From: Ferruccio Guidi Date: Tue, 29 Aug 2006 13:57:23 +0000 (+0000) Subject: - new tactic subst removes simple non recursive equalities from the context X-Git-Tag: 0.4.95@7852~1102 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=45d71beffd253ffd767a9afbfcec5c4f44afd8a8;p=helm.git - new tactic subst removes simple non recursive equalities from the context - RELATIONAL updated to use the new tactic --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index efcd21071..54924ff4c 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -83,7 +83,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Right of loc | Ring of loc | Split of loc - | Subst of loc * string + | Subst of loc | Symmetry of loc | Transitivity of loc * 'term (* Costruttori Aggiunti *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 425751b72..e1855014d 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -152,7 +152,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Right _ -> "right" | Ring _ -> "ring" | Split _ -> "split" - | Subst (_, s) -> "subst " ^ s + | Subst _ -> "subst" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ term_pp term (* Tattiche Aggiunte *) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index ac6381246..4a9254845 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -152,7 +152,7 @@ let tactic_of_ast ast = | GrafiteAst.Right _ -> Tactics.right | GrafiteAst.Ring _ -> Tactics.ring | GrafiteAst.Split _ -> Tactics.split - | GrafiteAst.Subst (_, hyp) -> Tactics.subst ~hyp + | GrafiteAst.Subst _ -> Tactics.subst | GrafiteAst.Symmetry _ -> Tactics.symmetry | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term (* Implementazioni Aggiunte *) diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 151d8cebd..cdf01febd 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -246,8 +246,8 @@ let disambiguate_tactic metasenv,GrafiteAst.Ring loc | GrafiteAst.Split loc -> metasenv,GrafiteAst.Split loc - | GrafiteAst.Subst (loc, hyp) -> - metasenv, GrafiteAst.Subst (loc, hyp) + | GrafiteAst.Subst loc -> + metasenv, GrafiteAst.Subst loc | GrafiteAst.Symmetry loc -> metasenv,GrafiteAst.Symmetry loc | GrafiteAst.Transitivity (loc, term) -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 9e9be81e2..16f7998d1 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -233,8 +233,8 @@ EXTEND GrafiteAst.Ring loc | IDENT "split" -> GrafiteAst.Split loc - | IDENT "subst"; id = IDENT -> - GrafiteAst.Subst (loc, id) + | IDENT "subst" -> + GrafiteAst.Subst loc | IDENT "symmetry" -> GrafiteAst.Symmetry loc | IDENT "transitivity"; t = tactic_term -> diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index c697acaed..fd6e7c59f 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -191,7 +191,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit in (proof',goals) with (* FG: this should be PET.Fail _ *) - TC.TypeCheckerFailure _ -> PET.apply_tactic (P.letout_tac ()) status + TC.TypeCheckerFailure _ -> PET.apply_tactic P.letout_tac status in ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality) @@ -362,7 +362,7 @@ let transitivity_tac ~term = ProofEngineTypes.mk_tactic (transitivity_tac ~term) ;; -(* FG *) +(* FG: subst tactic *********************************************************) let msg0 = lazy "Subst: not found in context" let msg1 = lazy "Subst: not a simple equality" @@ -402,3 +402,26 @@ let subst_tac ~hyp = PET.apply_tactic tac status in PET.mk_tactic subst_tac + +(* FG: This should be replaced by T.try_tactic *) +let try_tactic ~tactic = + let try_tactic status = + try PET.apply_tactic tactic status with + | PET.Fail _ -> PET.apply_tactic T.id_tac status + in + PET.mk_tactic try_tactic + +let subst_tac = + let subst hyp = try_tactic ~tactic:(subst_tac hyp) in + let map = function + | Some (C.Name s, _) -> Some (subst s) + | _ -> None + in + let subst_tac status = + let (proof, goal) = status in + let (_, metasenv, _, _) = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let tactics = PEH.list_rev_map_filter map context in + PET.apply_tactic (T.seq ~tactics) status + in + PET.mk_tactic subst_tac diff --git a/components/tactics/equalityTactics.mli b/components/tactics/equalityTactics.mli index 31ad7eedf..4edb5747a 100644 --- a/components/tactics/equalityTactics.mli +++ b/components/tactics/equalityTactics.mli @@ -41,4 +41,5 @@ val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic (* FG *) -val subst_tac: hyp:string -> ProofEngineTypes.tactic +(* rewrites and clears all simple equalities in the context *) +val subst_tac: ProofEngineTypes.tactic diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 5fb8d4ae1..9baf829ea 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -571,7 +571,7 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres module C = Cic -let letout_tac () = +let letout_tac = let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in let term = C.Sort C.Set in let letout_tac (proof, goal) = diff --git a/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli index 0f003bb4c..ce5194ad1 100644 --- a/components/tactics/primitiveTactics.mli +++ b/components/tactics/primitiveTactics.mli @@ -81,4 +81,4 @@ val elim_intros_tac: (* inserts a hole in the context *) val letout_tac: - unit -> ProofEngineTypes.tactic + ProofEngineTypes.tactic diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml index ceb2d2de8..88e2f4b9e 100644 --- a/components/tactics/tacticals.ml +++ b/components/tactics/tacticals.ml @@ -242,7 +242,7 @@ struct (* This applies tactic and catches its possible failure *) let try_tactic ~tactic = - let rec try_tactic ~tactic status = + let try_tactic status = info (lazy "in Tacticals.try_tactic"); try S.apply_tactic tactic status @@ -252,7 +252,7 @@ struct "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e)); S.apply_tactic S.id_tactic status in - S.mk_tactic (try_tactic ~tactic) + S.mk_tactic try_tactic (* This tries tactics until one of them doesn't _solve_ the goal *) (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index a77b3475f..4517db0b5 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Aug 28 17:29:50 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Aug 29 11:37:38 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic @@ -80,7 +80,7 @@ val ring : ProofEngineTypes.tactic val set_goal : int -> ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic -val subst : hyp:string -> ProofEngineTypes.tactic +val subst : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val unfold : diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma index 6bdb81946..436dc7e62 100644 --- a/matita/contribs/RELATIONAL/NLE/dec.ma +++ b/matita/contribs/RELATIONAL/NLE/dec.ma @@ -21,11 +21,9 @@ theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x. [ auto | decompose; [ lapply linear nle_gen_succ_1 to H1. decompose. - rewrite > H1. clear H1 n. auto + subst. auto | lapply linear nle_lt_or_eq to H1; decompose; - [ auto - | rewrite > H. clear H n. auto - ] + subst; auto ] ]. qed. diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma index 19ad50b9b..6a78e0aac 100644 --- a/matita/contribs/RELATIONAL/NLE/fwd.ma +++ b/matita/contribs/RELATIONAL/NLE/fwd.ma @@ -24,7 +24,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to intros. inversion H; clear H; intros; [ apply (eq_gen_succ_zero ? ? H) | lapply linear eq_gen_succ_succ to H2 as H0. - rewrite > H0. clear H0. + subst. apply ex_intro; [|auto] (**) ]. qed. @@ -34,8 +34,7 @@ theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y. [ apply (eq_gen_succ_zero ? ? H) | lapply linear eq_gen_succ_succ to H2 as H0. lapply linear eq_gen_succ_succ to H3 as H2. - rewrite > H0. rewrite > H2. clear H0 H2. - auto + subst. auto ]. qed. diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma index e961f5a9c..8745e160e 100644 --- a/matita/contribs/RELATIONAL/NLE/props.ma +++ b/matita/contribs/RELATIONAL/NLE/props.ma @@ -28,11 +28,9 @@ theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y. intros 1. elim y; clear y; intros; [ lapply linear nle_gen_zero_2 to H. auto | lapply linear nle_gen_succ_2 to H1. decompose; - [ rewrite > H1. clear H1. auto + [ subst. auto | lapply linear H to H3 as H0. decompose; - [ rewrite > H1. clear H1 x. auto - | rewrite < H. clear H n. auto - ] + subst; auto ] ]. qed. diff --git a/matita/contribs/RELATIONAL/NPlus/fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma index 350a53f62..b1f7f2ca3 100644 --- a/matita/contribs/RELATIONAL/NPlus/fwd.ma +++ b/matita/contribs/RELATIONAL/NPlus/fwd.ma @@ -32,7 +32,7 @@ theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to [ | clear H1. decompose. - rewrite > H1. clear H1 n2 + subst. ]; apply ex_intro; [| auto || auto ]. (**) qed. @@ -50,7 +50,7 @@ theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to [ lapply eq_gen_succ_zero to H as H0. apply H0 | clear H1 H3 r. lapply linear eq_gen_succ_succ to H2 as H0. - rewrite > H0. clear H0 q. + subst. apply ex_intro; [| auto ] (**) ]. qed. @@ -58,8 +58,7 @@ qed. theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to p = zero \land q = zero. intros. inversion H; clear H; intros; - [ rewrite < H1. clear H1 p. - auto + [ subst. auto | clear H H1. lapply eq_gen_zero_succ to H3 as H0. apply H0 ]. @@ -69,10 +68,10 @@ theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to \exists s. p = succ s \land (s + q == r) \lor q = succ s \land p + s == r. intros. inversion H; clear H; intros; - [ rewrite < H1. clear H1 p + [ subst. | clear H1. lapply linear eq_gen_succ_succ to H3 as H0. - rewrite > H0. clear H0 r. + subst. ]; apply ex_intro; [| auto || auto ] (**) qed. (* @@ -82,8 +81,7 @@ variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to p = zero \land q = zero. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p. - auto + subst. auto | clear H. lapply linear nplus_gen_succ_2 to H1 as H0. decompose. @@ -96,12 +94,12 @@ variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to q = succ s \land p + s == r. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p + subst | clear H. lapply linear nplus_gen_succ_2 to H1 as H0. decompose. lapply linear eq_gen_succ_succ to H1 as H0. - rewrite > H0. clear H0 r. + subst ]; apply ex_intro; [| auto || auto ]. (**) qed. *) @@ -110,21 +108,21 @@ qed. theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p + subst | lapply linear nplus_gen_succ_2 to H1 as H0. decompose. lapply linear eq_gen_succ_succ to H2 as H0. - rewrite < H0 in H3. clear H0 a + subst ]; auto. qed. theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero. intros 1. elim p; clear p; intros; [ lapply linear nplus_gen_zero_1 to H as H0. - rewrite > H0. clear H0 q + subst | lapply linear nplus_gen_succ_1 to H1 as H0. decompose. lapply linear eq_gen_succ_succ to H2 as H0. - rewrite < H0 in H3. clear H0 a + subst ]; auto. qed. diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma index a40187c65..5e7cc1b7f 100644 --- a/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/matita/contribs/RELATIONAL/NPlus/props.ma @@ -24,20 +24,20 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to (succ p) + q == (succ r). intros 2. elim q; clear q; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p + subst | lapply linear nplus_gen_succ_2 to H1 as H0. decompose. - rewrite > H2. clear H2 r + subst ]; auto. qed. theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r. intros 2. elim q; clear q; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p + subst | lapply linear nplus_gen_succ_2 to H1 as H0. decompose. - rewrite > H2. clear H2 r + subst ]; auto. qed. @@ -45,18 +45,14 @@ theorem nplus_shift_succ_sx: \forall p,q,r. (p + (succ q) == r) \to (succ p) + q == r. intros. lapply linear nplus_gen_succ_2 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. + decompose. subst. auto. qed. theorem nplus_shift_succ_dx: \forall p,q,r. ((succ p) + q == r) \to p + (succ q) == r. intros. lapply linear nplus_gen_succ_1 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. + decompose. subst. auto. qed. theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to @@ -64,13 +60,11 @@ theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to \exists q. (q1 + q2 == q) \land p + q == r2. intros 2; elim q1; clear q1; intros; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p + subst. | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. + decompose. subst. lapply linear nplus_gen_succ_1 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. + decompose. subst. lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto || auto ]. (**) @@ -81,13 +75,11 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to \exists p. (p1 + p2 == p) \land p + q == r2. intros 2; elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p1 + subst | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. + decompose. subst. lapply linear nplus_gen_succ_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. + decompose. subst. lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto || auto ]. (**) @@ -97,12 +89,10 @@ theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to \forall r2. (p + q == r2) \to r1 = r2. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0 in H1. clear H0 p + subst | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. clear H3 r1. + decompose. subst. lapply linear nplus_gen_succ_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. + decompose. subst. ]; auto. qed. diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma index 407db9b66..457899a8c 100644 --- a/matita/contribs/prova.ma +++ b/matita/contribs/prova.ma @@ -19,9 +19,9 @@ include "nat/nat.ma". theorem pippo: \forall (P,Q,R:nat \to Prop). \forall x,y. x=y \to P x \to Q x \to R x. intros. - try rewrite > P in Q. + rewrite > P in Q. (* -theorem pippo2: \forall (P,Q,R:nat \to Prop). - \forall x,y. x=y \to P x \to Q x \to R x. - intros. rewrite > H in y. -*) +theorem pippo: \forall (P,Q,R:nat \to Prop). + \forall x,y. x=y \to P x \to Q x \to R x. + intros. rewrite > H in y. +*) \ No newline at end of file diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index 53a20ac6a..cd26700ab 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -1578,6 +1578,46 @@ its constructor takes no arguments. + + + subst + subst + subst + + + + Synopsis: + + subst + + + + Pre-conditions: + + None. + + + + Action: + + For each premise of the form + H: x = t or H: t = x + where x is a local variable and + t does not depend on x, + the tactic rewrites H wherever + x appears clearing H and + x afterwards. + + + + New sequents to prove: + + The one opened by the applied tactics. + + + + + symmetry symmetry diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index e44a53068..2709769ba 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -270,6 +270,15 @@ + + + | + + + subst + + + | diff --git a/matita/matita.lang b/matita/matita.lang index b7198579c..13c88e480 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -123,6 +123,7 @@ symmetry simplify split + subst to transitivity unfold