diff options
author | 2003-11-26 14:33:04 +0000 | |
---|---|---|
committer | 2003-11-26 14:33:04 +0000 | |
commit | cdb1422b199d1966fb2276c197a3d2ed516a735f (patch) | |
tree | fbded1c9006c68b2bba57202b16d722ccc5c5adc /contrib | |
parent | 4cc4a78c44a2d156fe55acec58195d89e08df9ac (diff) |
removal of CC.v lemata in cc (deprecated)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4994 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/cc/CC.v | 29 | ||||
-rw-r--r-- | contrib/cc/cctac.ml4 | 56 |
2 files changed, 36 insertions, 49 deletions
diff --git a/contrib/cc/CC.v b/contrib/cc/CC.v index da7292084..86f24b1cb 100644 --- a/contrib/cc/CC.v +++ b/contrib/cc/CC.v @@ -6,32 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $id$ *) +(* $id:$ *) -Require Export Eqdep_dec. - -(* Congruence lemma *) - -Theorem Congr_nodep: (A,B:Type)(f,g:A->B)(x,y:A)f==g->x==y->(f x)==(g y). -Intros A B f g x y eq1 eq2;Rewrite eq1;Rewrite eq2;Reflexivity. -Defined. - -Theorem Congr_dep: - (A:Type; P:(A->Type); f,g:((a:A)(P a)); x:A)f==g->(f x)==(g x). -Intros A P f g x e;Rewrite e;Reflexivity. -Defined. - -(* Basic application : try to prove that goal is equal to one hypothesis *) - -Lemma convert_goal : (A,B:Prop)B->(A==B)->A. -Intros A B H E;Rewrite E;Assumption. -Save. +(* Here were some now deprecated lemmata *) Tactic Definition CCsolve := Repeat (Match Context With [ H: ?1 |- ?2] -> - (Assert Heq____:(?2==?1);[CC|(Rewrite Heq____;Exact H)]) + Let Heq = FreshId "Heq" In + (Assert Heq:(?2==?1);[CC|(Rewrite Heq;Exact H)]) |[ H: ?1; G: ?2 -> ?3 |- ?] -> - (Assert Heq____:(?2==?1) ;[CC| - (Rewrite Heq____ in G;Generalize (G H);Clear G;Intro G)])). + Let Heq = FreshId "Heq" In + (Assert Heq:(?2==?1) ;[CC| + (Rewrite Heq in G;Generalize (G H);Clear G;Intro G)])). diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 index 85e8c9ae8..2bc225b66 100644 --- a/contrib/cc/cctac.ml4 +++ b/contrib/cc/cctac.ml4 @@ -121,7 +121,7 @@ let build_projection (cstr:constructor) nargs argind ttype default atype gls= let env=pf_env gls 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 "C") gls in + let id=pf_get_new_id (id_of_string "t") gls in mkLambda(Name id,ttype,body) (* generate an adhoc tactic following the proof tree *) @@ -134,23 +134,29 @@ let rec proof_tac uf axioms=function (tclTHENS (transitivity t) [(proof_tac uf axioms p1);(proof_tac uf axioms p2)]) | Congr (p1,p2)-> - (fun gls-> - let (s1,t1)=(type_proof axioms p1) and - (s2,t2)=(type_proof axioms p2) in - let ts1=(make_term s1) and tt1=(make_term t1) - and ts2=(make_term s2) and tt2=(make_term t2) in - let typ1=pf_type_of gls ts1 and typ2=pf_type_of gls ts2 in - let (typb,_,_)=(eq_type_of_term gls.it.evar_concl) in - let act=mkApp ((Lazy.force congr_theo),[|typ2;typb;ts1;tt1;ts2;tt2|]) in - tclORELSE - (tclTHENS - (apply act) - [(proof_tac uf axioms p1);(proof_tac uf axioms p2)]) - (tclTHEN - (let p=mkLambda(destProd typ1) in - let acdt=mkApp((Lazy.force congr_dep_theo), - [|typ2;p;ts1;tt1;ts2|]) in - apply acdt) (proof_tac uf axioms p1)) gls) + 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_theo,[|typf;typfx;appx1;tf1;tf2|]) + 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); + tclFIRST + [tclTHEN (apply lemma2) (proof_tac uf axioms p2); + reflexivity; + fun gls -> + errorlabstrm "CC" + (Pp.str + "CC doesn'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 @@ -168,19 +174,15 @@ let rec proof_tac uf axioms=function (* wrap everything *) let cc_tactic gls= - Library.check_required_library ["Coq";"cc";"CC"]; + Library.check_required_library ["Coq";"Init";"Logic"]; let prb= try make_prb gls with Not_an_eq -> - errorlabstrm "CC" [< str "Goal is not an equality" >] in + 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)-> - tclORELSE (proof_tac uf axioms p) - (fun _->errorlabstrm "CC" - [< str "CC doesn't know how to handle dependent equality." >]) - gls - + None->errorlabstrm "CC" (str "CC couldn't solve goal") + | Some (p,uf,axioms)->proof_tac uf axioms p gls + (* Tactic registration *) TACTIC EXTEND CC |