diff options
Diffstat (limited to 'contrib/cc/cctac.ml')
| -rw-r--r-- | contrib/cc/cctac.ml | 336 |
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.") |