From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 12:31:24 +0000 (+0000) Subject: 1. rewrite_* and rewrite_back_* merged into one function X-Git-Tag: PRE_GETTER_STORAGE~94 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=06ef12ecdaa09ed6e9c2b00554010e6b59f77744;p=helm.git 1. rewrite_* and rewrite_back_* merged into one function 2. signature of rewrite_* improved 3. concrete syntax for the rewrite direction fixed to ">" and "<" NOTE: rewrite_* is still no longer working. --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 354b18ae5..7239e98e3 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -84,11 +84,8 @@ let tactic_of_ast = function | TacticAst.Reflexivity _ -> Tactics.reflexivity | TacticAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what - | TacticAst.Rewrite (_, dir, t, pattern) -> - if dir = `Left then - EqualityTactics.rewrite_tac ~where:pattern ~term:t () - else - EqualityTactics.rewrite_back_tac ~where:pattern ~term:t () + | TacticAst.Rewrite (_, direction, t, pattern) -> + EqualityTactics.rewrite_tac ~direction ~pattern t | TacticAst.Right _ -> Tactics.right | TacticAst.Ring _ -> Tactics.ring | TacticAst.Split _ -> Tactics.split diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 11396b8bd..c0662e78f 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -102,5 +102,5 @@ qed. theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n). intros. lapply le_gen_S_x_2 to H using H0. elim H0. elim H1. -lapply eq_gen_S_S to H2 using H4. rewrite left H4. assumption. +lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption. qed. diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma index 888ec5abd..f5ad10c7f 100644 --- a/helm/matita/tests/inversion.ma +++ b/helm/matita/tests/inversion.ma @@ -20,7 +20,7 @@ theorem test_inversion: \forall n. le n O \to n=O. generalize Hcut. apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H). (* first goal (left open) *) - intro. rewrite right H1. + intro. rewrite < H1. clear Hcut. (* second goal (closed) *) goal 14. @@ -38,7 +38,7 @@ theorem test_inversion2: \forall n. le n O \to n=O. generalize (refl_equal nat O). apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H). (* first goal (left open) *) - intro. rewrite right H1. + intro. rewrite < H1. (* second goal (closed) *) goal 13. simplify. intros. diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index 67da01e89..ce1e216ad 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -10,13 +10,13 @@ theorem a: \forall a,b:nat. a = b \to b + a + b + a= (\lambda j.((\lambda w.((\lambda x.x + b + w + j) a)) b)) a. intros. -rewrite right H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)). +rewrite < H in \vdash (? ? ? ((\lambda j.((\lambda w.%) ?)) ?)). -rewrite right H in \vdash (? ? % ?). +rewrite < H in \vdash (? ? % ?). simplify in \vdash (? ? ? ((\lambda x.((\lambda y.%) ?)) ?)). -rewrite right H in \vdash (? ? ? (% ?)). +rewrite < H in \vdash (? ? ? (% ?)). simplify. reflexivity. qed.