From d7a329578a475af98aa5f2a16d9873a576dab599 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 11 Oct 2002 16:47:37 +0000 Subject: [PATCH] New tactic rewrite implemented. Not tested yet. --- helm/gTopLevel/fourierR.ml | 49 +++++++++++++++++++- helm/gTopLevel/fourierR.mli | 2 +- helm/gTopLevel/gTopLevel.ml | 11 ++++- helm/gTopLevel/proofEngine.ml | 2 +- helm/gTopLevel/proofEngine.mli | 1 + helm/gTopLevel/proofEngineReduction.ml | 59 +++++++++++++++++++++++++ helm/gTopLevel/proofEngineReduction.mli | 3 ++ 7 files changed, 123 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 1de87fdd9..b9e782330 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -24,6 +24,54 @@ *) +(******************** OTHER USEFUL TACTICS **********************) + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") -> + ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality:ProofEngineReduction.syntactic_equality + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("##### Atteso: " ^ CicPp.ppterm + (C.Lambda (C.Name "x", ty, + C.Appl + [C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind",0,0) ; + ty ; C.Rel 3 ; C.Rel 1])) +) ; +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + PrimitiveTactics.exact_tac + (C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ((curi,metasenv',pbo,pty),goal) +;; + +(******************** THE FOURIER TACTIC ***********************) (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients des inéquations et équations sont entiers. En attendant la tactique Field. @@ -1026,4 +1074,3 @@ let rec fourier ~status:(s_proof,s_goal)= ;; let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; - diff --git a/helm/gTopLevel/fourierR.mli b/helm/gTopLevel/fourierR.mli index 68bc34288..87d034909 100644 --- a/helm/gTopLevel/fourierR.mli +++ b/helm/gTopLevel/fourierR.mli @@ -1,2 +1,2 @@ +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic val fourier_tac: ProofEngineTypes.tactic - diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 48c178918..3c37b3ed2 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -681,8 +681,13 @@ let clearbody rendering_window = let clear rendering_window = call_tactic_with_hypothesis_input ProofEngine.clear rendering_window ;; +let fourier rendering_window = + call_tactic ProofEngine.fourier rendering_window +;; +let rewrite rendering_window = + call_tactic_with_input ProofEngine.rewrite rendering_window +;; -let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;; let whd_in_scratch scratch_window = @@ -1460,6 +1465,9 @@ class rendering_window output proofw (label : GMisc.label) = let fourierb = GButton.button ~label:"Fourier" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rewriteb = + GButton.button ~label:"Rewrite" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -1514,6 +1522,7 @@ object(self) ignore(clearbodyb#connect#clicked (clearbody self)) ; ignore(clearb#connect#clicked (clear self)) ; ignore(fourierb#connect#clicked (fourier self)) ; + ignore(rewriteb#connect#clicked (rewrite self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 0e4de4f3b..0885f3037 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -273,4 +273,4 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) let elim_type term = apply_tactic (Ring.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac - +let rewrite term = apply_tactic (FourierR.rewrite_tac ~term) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index fed8d04ad..a11914a9a 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -58,3 +58,4 @@ val clear : Cic.hypothesis -> unit val elim_type : Cic.term -> unit val ring : unit -> unit val fourier : unit -> unit +val rewrite : Cic.term -> unit diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 87cf24c21..265e5f99c 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -146,6 +146,65 @@ let replace ~equality ~what ~with_what ~where = aux where ;; +(* replaces in a term a term with another one. *) +(* Lifting are performed as usual. *) +let replace_lifting ~equality ~what ~with_what ~where = + let rec substaux k = + let module C = Cic in + function + t when (equality t what) -> CicSubstitution.lift (k-1) with_what + | C.Rel n as t -> t (*CSC: ??? BUG ? *) + | C.Var _ as t -> t + | C.Meta (i, l) as t -> + let l' = + List.map + (function + None -> None + | Some t -> Some (substaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k) tl in + begin + match substaux k he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false + | C.Const _ as t -> t + | C.MutInd _ as t -> t + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,substaux k outt, substaux k t, + List.map (substaux k) pl) + | C.Fix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, substaux k ty, substaux (k+len) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let len = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, substaux k ty, substaux (k+len) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + substaux 1 where +;; + (* Takes a well-typed term and fully reduces it. *) (*CSC: It does not perform reduction in a Case *) let reduce context = diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli index 06a7f2b9a..e2d96f40b 100644 --- a/helm/gTopLevel/proofEngineReduction.mli +++ b/helm/gTopLevel/proofEngineReduction.mli @@ -38,5 +38,8 @@ val syntactic_equality : Cic.term -> Cic.term -> bool val replace : equality:(Cic.term -> 'a -> bool) -> what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term +val replace_lifting : + equality:(Cic.term -> 'a -> bool) -> + what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term val reduce : Cic.context -> Cic.term -> Cic.term val simpl : Cic.context -> Cic.term -> Cic.term -- 2.39.2