Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 336 insertions, 0 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
new file mode 100644
index 00000000..4a719f38
--- /dev/null
+++ b/contrib/cc/cctac.ml
@@ -0,0 +1,336 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: cctac.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
+
+(* This file is the interface between the c-c algorithm and Coq *)
+
+open Evd
+open Proof_type
+open Names
+open Libnames
+open Nameops
+open Inductiveops
+open Declarations
+open Term
+open Termops
+open Tacmach
+open Tactics
+open Tacticals
+open Ccalgo
+open Tacinterp
+open Ccproof
+open Pp
+open Util
+open Format
+
+let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
+
+let _f_equal = constant ["Init";"Logic"] "f_equal"
+
+let _eq_rect = constant ["Init";"Logic"] "eq_rect"
+
+let _eq = constant ["Init";"Logic"] "eq"
+
+let _False = constant ["Init";"Logic"] "False"
+
+(* decompose member of equality in an applicative format *)
+
+let whd env=
+  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let whd_delta env=
+   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let rec decompose_term env t=
+    match kind_of_term (whd env t) with
+      App (f,args)->
+	let tf=decompose_term env f in
+	let targs=Array.map (decompose_term env) args in
+	  Array.fold_left (fun s t->Appli (s,t)) tf targs
+    | Construct c->
+	let (oib,_)=Global.lookup_inductive (fst c) in
+	let nargs=mis_constructor_nargs_env env c in
+	  Constructor {ci_constr=c;
+		       ci_arity=nargs;
+		       ci_nhyps=nargs-oib.mind_nparams}
+    | _ ->(Symb t)
+	
+(* decompose equality in members and type *)
+	
+let atom_of_constr env term =
+  let wh =  (whd_delta env term) in
+  let kot = kind_of_term wh in 
+    match kot with
+      App (f,args)->
+	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3 
+	  then `Eq (args.(0),
+		   decompose_term env args.(1), 
+		   decompose_term env args.(2)) 
+	  else `Other (decompose_term env term)
+    | _ -> `Other (decompose_term env term)
+
+let rec litteral_of_constr env term=
+  match kind_of_term (whd_delta env term) with
+      Prod (_,atom,ff) -> 
+	if eq_constr ff (Lazy.force _False) then
+	  match (atom_of_constr env atom) with
+	      `Eq(t,a,b) -> `Neq(t,a,b)
+	    | `Other(p) -> `Nother(p)
+	else 
+	  `Other (decompose_term env term)
+    | _ -> atom_of_constr env term
+	
+(* rebuild a term from applicative format *)
+    
+let rec make_term = function
+    Symb s->s
+  | Eps -> anomaly "epsilon constant has no value" 
+  | Constructor cinfo -> mkConstruct cinfo.ci_constr 
+  | Appli (s1,s2)->
+      make_app [(make_term s2)] s1
+and make_app l=function
+    Appli (s1,s2)->make_app ((make_term s2)::l) s1    
+  | other -> applistc (make_term other) l 
+
+(* store all equalities from the context *)
+	
+let rec make_prb gls additionnal_terms =
+  let env=pf_env gls in
+  let state = empty () in
+  let pos_hyps = ref [] in
+  let neg_hyps =ref [] in
+    List.iter
+      (fun c ->
+	 let t = decompose_term env c in
+	   ignore (add_term state t)) additionnal_terms; 
+    List.iter 
+      (fun (id,_,e) ->
+	 begin
+	   match litteral_of_constr env e with
+	       `Eq (t,a,b) -> add_equality state id a b
+	     | `Neq (t,a,b) -> add_disequality state (Hyp id) a b
+	     | `Other ph ->
+		 List.iter 
+		   (fun (idn,nh) -> 
+		      add_disequality state (HeqnH (id,idn)) ph nh) 
+		   !neg_hyps;
+		 pos_hyps:=(id,ph):: !pos_hyps
+	     | `Nother nh ->
+		 List.iter 
+		   (fun (idp,ph) -> 
+		      add_disequality state (HeqnH (idp,id)) ph nh) 
+		   !pos_hyps;
+		 neg_hyps:=(id,nh):: !neg_hyps
+	 end) (Environ.named_context_of_val gls.it.evar_hyps);
+    begin
+      match atom_of_constr env gls.it.evar_concl with
+	  `Eq (t,a,b) -> add_disequality state Goal a b
+	|	`Other g ->  
+		  List.iter 
+	      (fun (idp,ph) -> 
+		 add_disequality state (HeqG idp) ph g) !pos_hyps
+    end;
+    state
+
+(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
+
+let build_projection intype outtype (cstr:constructor) special default gls=
+  let env=pf_env gls in 
+  let (h,argv) = 
+    try destApp intype with 
+	Invalid_argument _ -> (intype,[||])  in
+  let ind=destInd h in 
+  let types=Inductiveops.arities_of_constructors env ind in
+  let lp=Array.length types in
+  let ci=(snd cstr)-1 in
+  let branch i=
+    let ti=Term.prod_appvect types.(i) argv in
+    let rc=fst (Sign.decompose_prod_assum ti) in
+    let head=
+      if i=ci then special else default in  
+      Sign.it_mkLambda_or_LetIn head rc in
+  let branches=Array.init lp branch in
+  let casee=mkRel 1 in
+  let pred=mkLambda(Anonymous,intype,outtype) in
+  let case_info=make_default_case_info (pf_env gls) RegularStyle ind in
+  let body= mkCase(case_info, pred, casee, branches) in
+  let id=pf_get_new_id (id_of_string "t") gls in     
+    mkLambda(Name id,intype,body)
+  
+(* generate an adhoc tactic following the proof tree  *)
+
+let rec proof_tac axioms=function
+    Ax id->exact_check (mkVar id)
+  | SymAx id->tclTHEN symmetry (exact_check (mkVar id))
+  | Refl t->reflexivity
+  | Trans (p1,p2)->let t=(make_term (snd (type_proof axioms p1))) in
+      (tclTHENS (transitivity t) 
+	 [(proof_tac axioms p1);(proof_tac axioms p2)])
+  | Congr (p1,p2)->
+      fun gls->
+	let (f1,f2)=(type_proof axioms p1) 
+	and (x1,x2)=(type_proof axioms p2) in
+        let tf1=make_term f1 and tx1=make_term x1 
+	and tf2=make_term f2 and tx2=make_term x2 in
+	let typf=pf_type_of gls tf1 and typx=pf_type_of gls tx1
+	and typfx=pf_type_of gls (mkApp(tf1,[|tx1|])) in
+	let id=pf_get_new_id (id_of_string "f") gls in
+	let appx1=mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
+	let lemma1=
+	  mkApp(Lazy.force _f_equal,[|typf;typfx;appx1;tf1;tf2|])
+	and lemma2=
+	  mkApp(Lazy.force _f_equal,[|typx;typfx;tf2;tx1;tx2|]) in
+	  (tclTHENS (transitivity (mkApp(tf2,[|tx1|])))
+	     [tclTHEN (apply lemma1) (proof_tac axioms p1);
+  	      tclFIRST
+		[tclTHEN (apply lemma2) (proof_tac axioms p2);
+		 reflexivity;
+		 fun gls ->
+		   errorlabstrm  "Congruence" 
+		   (Pp.str 
+		      "I don't know how to handle dependent equality")]]
+	     gls)
+  | Inject (prf,cstr,nargs,argind)  as gprf->
+      (fun gls ->
+	 let ti,tj=type_proof axioms prf in
+	 let ai,aj=type_proof axioms gprf in
+	 let cti=make_term ti in
+	 let ctj=make_term tj in
+	 let cai=make_term ai in
+	 let intype=pf_type_of gls cti in
+	 let outtype=pf_type_of gls cai in
+	 let special=mkRel (1+nargs-argind) in
+	 let default=make_term ai in
+	 let proj=build_projection intype outtype cstr special default gls in
+	 let injt=
+	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;cti;ctj|]) in 
+	   tclTHEN (apply injt) (proof_tac axioms prf) gls)
+
+let refute_tac axioms id t1 t2 p gls =      
+  let tt1=make_term t1 and tt2=make_term t2 in
+  let intype=pf_type_of gls tt1 in
+  let neweq=
+    mkApp(Lazy.force _eq,
+	  [|intype;tt1;tt2|]) in
+  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let false_t=mkApp (mkVar id,[|mkVar hid|]) in
+    tclTHENS (true_cut (Name hid) neweq)
+      [proof_tac axioms p; simplest_elim false_t] gls
+
+let convert_to_goal_tac axioms id t1 t2 p gls =
+  let tt1=make_term t1 and tt2=make_term t2 in
+  let sort=pf_type_of gls tt2 in
+  let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in 
+  let e=pf_get_new_id (id_of_string "e") gls in
+  let x=pf_get_new_id (id_of_string "X") gls in
+  let identity=mkLambda (Name x,sort,mkRel 1) in 
+  let endt=mkApp (Lazy.force _eq_rect,
+		  [|sort;tt1;identity;mkVar id;tt2;mkVar e|]) in
+    tclTHENS (true_cut (Name e) neweq) 
+      [proof_tac axioms p;exact_check endt] gls
+
+let convert_to_hyp_tac axioms id1 t1 id2 t2 p gls =
+  let tt2=make_term t2 in
+  let h=pf_get_new_id (id_of_string "H") gls in
+  let false_t=mkApp (mkVar id2,[|mkVar h|]) in
+    tclTHENS (true_cut (Name h) tt2)
+      [convert_to_goal_tac axioms id1 t1 t2 p;
+       simplest_elim false_t] gls
+  
+let discriminate_tac axioms cstr p gls =
+  let t1,t2=type_proof axioms p in 
+  let tt1=make_term t1 and tt2=make_term t2 in
+  let intype=pf_type_of gls tt1 in
+  let concl=pf_concl gls in
+  let outsort=mkType (new_univ ()) in
+  let xid=pf_get_new_id (id_of_string "X") gls in
+  let tid=pf_get_new_id (id_of_string "t") gls in
+  let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
+  let trivial=pf_type_of gls identity in
+  let outtype=mkType (new_univ ()) in
+  let pred=mkLambda(Name xid,outtype,mkRel 1) in
+  let hid=pf_get_new_id (id_of_string "Heq") gls in     
+  let proj=build_projection intype outtype cstr trivial concl gls in
+  let injt=mkApp (Lazy.force _f_equal,
+		  [|intype;outtype;proj;tt1;tt2;mkVar hid|]) in   
+  let endt=mkApp (Lazy.force _eq_rect,
+		  [|outtype;trivial;pred;identity;concl;injt|]) in
+  let neweq=mkApp(Lazy.force _eq,[|intype;tt1;tt2|]) in
+    tclTHENS (true_cut (Name hid) neweq) 
+      [proof_tac axioms p;exact_check endt] gls
+      
+(* wrap everything *)
+	
+let build_term_to_complete uf meta pac =
+  let cinfo = get_constructor_info uf pac.cnode in
+  let real_args = List.map (fun i -> make_term (term uf i)) pac.args in
+  let dummy_args = List.rev (list_tabulate meta pac.arity) in
+  let all_args = List.rev_append real_args dummy_args in
+    applistc (mkConstruct cinfo.ci_constr) all_args
+      
+let cc_tactic additionnal_terms gls=
+  Coqlib.check_required_library ["Coq";"Init";"Logic"];
+  let _ = debug Pp.msgnl (Pp.str "Reading subgoal ...") in
+  let state = make_prb gls additionnal_terms in
+  let _ = debug Pp.msgnl (Pp.str "Problem built, solving ...") in
+  let sol = execute true state in
+  let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
+  let uf=forest state in
+    match sol with
+	None -> tclFAIL 0 (str "congruence failed") gls  
+      | Some reason ->
+	  debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
+	  match reason with
+	      Discrimination (i,ipac,j,jpac) ->
+		let p=build_proof uf (`Discr (i,ipac,j,jpac)) in	  
+		let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+		  discriminate_tac (axioms uf) cstr p gls
+	    | Incomplete ->
+		let metacnt = ref 0 in
+		let newmeta _ = incr metacnt; mkMeta !metacnt in
+		let terms_to_complete = 
+		  List.map 
+		    (build_term_to_complete uf newmeta) 
+		    (epsilons uf) in 
+		  Pp.msgnl
+		    (Pp.str "Goal is solvable by congruence but \
+ some arguments are missing.");
+		  Pp.msgnl
+		    (Pp.str "  Try " ++
+		     hov 8
+		       begin 
+			 str "\"congruence with (" ++  
+			 prlist_with_sep 
+			   (fun () -> str ")" ++ pr_spc () ++ str "(")
+			   (print_constr_env (pf_env gls))
+			   terms_to_complete ++ 
+			 str ")\","
+		       end);
+		  Pp.msgnl
+		    (Pp.str "  replacing metavariables by arbitrary terms.");
+		  tclFAIL 0 (str "Incomplete") gls
+	    | Contradiction dis ->
+		let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+		let ta=term uf dis.lhs and tb=term uf dis.rhs in
+		let axioms = axioms uf in 
+		  match dis.rule with
+		      Goal -> proof_tac axioms p gls
+		    | Hyp id -> refute_tac axioms id ta tb p gls
+		    | HeqG id -> 
+			convert_to_goal_tac axioms id ta tb p gls
+		    | HeqnH (ida,idb) -> 
+			convert_to_hyp_tac axioms ida ta idb tb p gls
+		    
+
+let cc_fail gls =
+  errorlabstrm  "Congruence" (Pp.str "congruence failed.")