From f0e24c6a8b66e86a22370fcc45d1f3e7543496fd Mon Sep 17 00:00:00 2001 From: corbinea Date: Sat, 29 Nov 2003 12:19:35 +0000 Subject: ground->firstorder, cc-> congruence, CC final commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5022 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/cc/cctac.ml4 | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) (limited to 'contrib/cc/cctac.ml4') diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 index 2bc225b66..2089d5997 100644 --- a/contrib/cc/cctac.ml4 +++ b/contrib/cc/cctac.ml4 @@ -37,8 +37,6 @@ let fail()=raise Not_an_eq let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) let f_equal_theo = constant ["Init";"Logic"] "f_equal" -let congr_theo = constant ["cc";"CC"] "Congr_nodep" -let congr_dep_theo = constant ["cc";"CC"] "Congr_dep" (* decompose member of equality in an applicative format *) @@ -96,7 +94,10 @@ let rec read_hyps env=function let make_prb gl= let env=pf_env gl in - (read_hyps env gl.it.evar_hyps,read_eq env gl.it.evar_concl) + let hyps=read_hyps env gl.it.evar_hyps in + try (hyps,Some (read_eq env gl.it.evar_concl)) with + Not_an_eq -> (hyps,None) + (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) @@ -126,13 +127,13 @@ let build_projection (cstr:constructor) nargs argind ttype default atype gls= (* generate an adhoc tactic following the proof tree *) -let rec proof_tac uf axioms=function +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 uf axioms p1);(proof_tac uf axioms p2)]) + [(proof_tac axioms p1);(proof_tac axioms p2)]) | Congr (p1,p2)-> fun gls-> let (f1,f2)=(type_proof axioms p1) @@ -148,9 +149,9 @@ let rec proof_tac uf axioms=function and lemma2= mkApp(Lazy.force f_equal_theo,[|typx;typfx;tf2;tx1;tx2|]) in (tclTHENS (transitivity (mkApp(tf2,[|tx1|]))) - [tclTHEN (apply lemma1) (proof_tac uf axioms p1); + [tclTHEN (apply lemma1) (proof_tac axioms p1); tclFIRST - [tclTHEN (apply lemma2) (proof_tac uf axioms p2); + [tclTHEN (apply lemma2) (proof_tac axioms p2); reflexivity; fun gls -> errorlabstrm "CC" @@ -169,7 +170,7 @@ let rec proof_tac uf axioms=function let proj=build_projection cstr nargs argind ttype cai atype gls in let injt= mkApp (Lazy.force f_equal_theo,[|ttype;atype;proj;cti;ctj|]) in - tclTHEN (apply injt) (proof_tac uf axioms prf) gls) + tclTHEN (apply injt) (proof_tac axioms prf) gls) (* wrap everything *) @@ -180,13 +181,20 @@ let cc_tactic gls= Not_an_eq -> errorlabstrm "CC" (str "Goal is not an equality") in match (cc_proof prb) with - None->errorlabstrm "CC" (str "CC couldn't solve goal") - | Some (p,uf,axioms)->proof_tac uf axioms p gls - + Prove (p,axioms)-> proof_tac axioms p gls + | Refute (t1,t2,p,axioms) -> + let tt1=make_term t1 and tt2=make_term t2 in + let typ=pf_type_of gls tt1 in + let id=pf_get_new_id (id_of_string "Heq") gls in + let neweq= + mkApp(constr_of_reference Coqlib.glob_eq,[|typ;tt1;tt2|]) in + tclTHENS (true_cut (Some id) neweq) + [proof_tac axioms p;Equality.discr id] gls + (* Tactic registration *) TACTIC EXTEND CC - [ "CC" ] -> [ cc_tactic ] + [ "Congruence" ] -> [ cc_tactic ] END -- cgit v1.2.3