From 43ed97bb09bf148dfda74b3266b44143640b9643 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 1 May 2007 16:15:58 +0000 Subject: [PATCH] SubstTactic: bug fix RELATIONAL : some improvements on integers --- components/tactics/substTactic.ml | 11 +++-- matita/contribs/RELATIONAL/NPlus/monoid.ma | 2 +- matita/contribs/RELATIONAL/ZEq/defs.ma | 28 +++++++++++ .../RELATIONAL/{Zah => ZEq}/setoid.ma | 49 +++++-------------- .../{Zah/defs.ma => datatypes/Zah.ma} | 18 +------ matita/contribs/RELATIONAL/preamble.ma | 1 + 6 files changed, 53 insertions(+), 56 deletions(-) create mode 100644 matita/contribs/RELATIONAL/ZEq/defs.ma rename matita/contribs/RELATIONAL/{Zah => ZEq}/setoid.ma (56%) rename matita/contribs/RELATIONAL/{Zah/defs.ma => datatypes/Zah.ma} (68%) diff --git a/components/tactics/substTactic.ml b/components/tactics/substTactic.ml index ef2a297e1..cc107451e 100644 --- a/components/tactics/substTactic.ml +++ b/components/tactics/substTactic.ml @@ -67,6 +67,11 @@ let msg3 = lazy "Subst: no progress" let rec subst_tac ~try_tactic ~hyp = let hole = C.Implicit (Some `Hole) in let meta = C.Implicit None in + let rec ind = function + | C.MutInd _ -> true + | C.Appl (t :: tl) -> ind t + | _ -> false + in let rec constr = function | C.MutConstruct _ -> true | C.Appl (t :: tl) -> constr t @@ -105,7 +110,7 @@ let rec subst_tac ~try_tactic ~hyp = [lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]] in let whd_g () = - let whd_pattern = C.Appl [meta; meta; hole; hole] in + let whd_pattern = C.Appl [meta; hole; hole; hole] in let pattern = None, [hyp, whd_pattern], None in [RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp] in @@ -114,8 +119,8 @@ let rec subst_tac ~try_tactic ~hyp = when LO.is_eq_URI uri -> subst_g `LeftToRight i t | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) when LO.is_eq_URI uri -> subst_g `RightToLeft i t - | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) - when LO.is_eq_URI uri && constr t1 && constr t2 -> destruct_g () + | (C.Appl [(C.MutInd (uri, 0, [])); t; t1; t2]) + when LO.is_eq_URI uri && ind t && constr t1 && constr t2 -> destruct_g () | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when LO.is_eq_URI uri -> whd_g () | _ -> raise (PET.Fail msg1) diff --git a/matita/contribs/RELATIONAL/NPlus/monoid.ma b/matita/contribs/RELATIONAL/NPlus/monoid.ma index a7d56eeb3..4d1705b90 100644 --- a/matita/contribs/RELATIONAL/NPlus/monoid.ma +++ b/matita/contribs/RELATIONAL/NPlus/monoid.ma @@ -22,7 +22,7 @@ theorem nplus_zero_1: \forall q. zero + q == q. intros. elim q; clear q; auto. qed. -theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to +theorem nplus_succ_1: \forall p,q,r. (p + q == r) \to (succ p) + q == (succ r). intros. elim H; clear H q r; auto. qed. diff --git a/matita/contribs/RELATIONAL/ZEq/defs.ma b/matita/contribs/RELATIONAL/ZEq/defs.ma new file mode 100644 index 000000000..6d270cab3 --- /dev/null +++ b/matita/contribs/RELATIONAL/ZEq/defs.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/RELATIONAL/ZEq/defs". + +include "datatypes/Zah.ma". +include "NPlus/defs.ma". + +inductive ZEq: Zah \to Zah \to Prop := + | zeq: \forall m1,m2,m3,m4,n. + (m1 + m4 == n) \to (m3 + m2 == n) \to + ZEq \langle m1, m2 \rangle \langle m3, m4 \rangle +. + +interpretation "integer equality" 'eq x y = + (cic:/matita/RELATIONAL/ZEq/defs/ZEq.ind#xpointer(1/1) x y). + diff --git a/matita/contribs/RELATIONAL/Zah/setoid.ma b/matita/contribs/RELATIONAL/ZEq/setoid.ma similarity index 56% rename from matita/contribs/RELATIONAL/Zah/setoid.ma rename to matita/contribs/RELATIONAL/ZEq/setoid.ma index 681d63385..1b6279fd1 100644 --- a/matita/contribs/RELATIONAL/Zah/setoid.ma +++ b/matita/contribs/RELATIONAL/ZEq/setoid.ma @@ -12,49 +12,26 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid". +set "baseuri" "cic:/matita/RELATIONAL/ZEq/setoid". -include "NPlus/monoid.ma". -include "Zah/defs.ma". - -theorem nplus_total: \forall p,q. \exists r. p + q == r. - intros 2. elim q; clear q; - decompose; auto. -qed. -(* -theorem zeq_intro: \forall z1,z2. - (\forall n.((\fst z1) + (\snd z2) == n) \to ((\fst z2) + (\snd z1) == n)) \to - (\forall n.((\fst z2) + (\snd z1) == n) \to ((\fst z1) + (\snd z2) == n)) \to - z1 = z2. - unfold ZEq. intros. apply iff_intro; intros; auto. -qed. +include "NPlus/fun.ma". +include "ZEq/defs.ma". theorem zeq_refl: \forall z. z = z. - unfold ZEq. intros. auto. + intros. elim z. clear z. + lapply (nplus_total t t1). decompose. + auto. qed. theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1. - unfold ZEq. intros. lapply linear (H n). auto. + intros. elim H. clear H z1 z2. auto. qed. -*)(* +(* theorem zeq_trans: \forall z1,z2. z1 = z2 \to \forall z3. z2 = z3 \to z1 = z3. - unfold ZEq. intros. - lapply (nplus_total (\snd z2) (\fst z2)). decompose. - - - - apply iff_intro; intros; - [ lapply (nplus_total (\fst z1) (\snd z3)). decompose - | - - - - - lapply (nplus_total (\snd z2) (\fst z2)). decompose. - lapply (nplus_total n a). decompose. - lapply linear (H a1). lapply linear (H1 a1). decompose. - - - + intros 3. elim H. clear H z1 z2. + inversion H3. clear H3. intros. subst. + lapply (nplus_total n5 n6). decompose. + lapply (nplus_total n4 n9). decompose. + apply zeq. *) diff --git a/matita/contribs/RELATIONAL/Zah/defs.ma b/matita/contribs/RELATIONAL/datatypes/Zah.ma similarity index 68% rename from matita/contribs/RELATIONAL/Zah/defs.ma rename to matita/contribs/RELATIONAL/datatypes/Zah.ma index 83c9ceeea..87f61d7d1 100644 --- a/matita/contribs/RELATIONAL/Zah/defs.ma +++ b/matita/contribs/RELATIONAL/datatypes/Zah.ma @@ -12,22 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/Zah/defs". +set "baseuri" "cic:/matita/RELATIONAL/datatypes/Zah". -include "datatypes/constructors.ma". -include "logic/coimplication.ma". -include "NPlusList/defs.ma". +include "datatypes/Nat.ma". definition Zah \def Nat \times Nat. -(* -definition ZEq: Zah \to Zah -> Prop := - \lambda z1,z2. - \forall n. ((\fst z1) + (\snd z2) == n) \liff (\fst z2) + (\snd z1) == n. - -interpretation "integer equality" 'zeq x y = - (cic:/matita/RELATIONAL/Zah/defs/ZEq.con x y). - -notation "hvbox(a break = b)" - non associative with precedence 45 -for @{ 'zeq $a $b }. -*) \ No newline at end of file diff --git a/matita/contribs/RELATIONAL/preamble.ma b/matita/contribs/RELATIONAL/preamble.ma index 050d9dece..d52da9701 100644 --- a/matita/contribs/RELATIONAL/preamble.ma +++ b/matita/contribs/RELATIONAL/preamble.ma @@ -16,3 +16,4 @@ set "baseuri" "cic:/matita/RELATIONAL/preamble". include "logic/equality.ma". include "logic/connectives.ma". +include "datatypes/constructors.ma". -- 2.39.2