]> matita.cs.unibo.it Git - helm.git/commitdiff
SubstTactic: bug fix
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 1 May 2007 16:15:58 +0000 (16:15 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 1 May 2007 16:15:58 +0000 (16:15 +0000)
RELATIONAL : some improvements on integers

helm/software/components/tactics/substTactic.ml
helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma
helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma [new file with mode: 0644]
helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma [new file with mode: 0644]
helm/software/matita/contribs/RELATIONAL/Zah/defs.ma [deleted file]
helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma [deleted file]
helm/software/matita/contribs/RELATIONAL/datatypes/Zah.ma [new file with mode: 0644]
helm/software/matita/contribs/RELATIONAL/preamble.ma

index ef2a297e1cfc81e32d9b42e84d294421eb4fd73e..cc107451ee70182c1bbabbb4b8f557534bb87ef7 100644 (file)
@@ -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)
index a7d56eeb3e2f1e4ddf9bdd1672747bc6641eb0de..4d1705b90da0d1eba00f5e98cd5958c2fc639344 100644 (file)
@@ -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/helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/defs.ma
new file mode 100644 (file)
index 0000000..6d270ca
--- /dev/null
@@ -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/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
new file mode 100644 (file)
index 0000000..1b6279f
--- /dev/null
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/setoid".
+
+include "NPlus/fun.ma".
+include "ZEq/defs.ma".
+
+theorem zeq_refl: \forall z. z = z.
+ intros. elim z. clear z.
+ lapply (nplus_total t t1). decompose.
+ auto.
+qed.
+
+theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
+ 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.
+ 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/helm/software/matita/contribs/RELATIONAL/Zah/defs.ma b/helm/software/matita/contribs/RELATIONAL/Zah/defs.ma
deleted file mode 100644 (file)
index 83c9cee..0000000
+++ /dev/null
@@ -1,33 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/Zah/defs".
-
-include "datatypes/constructors.ma".
-include "logic/coimplication.ma".
-include "NPlusList/defs.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/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma b/helm/software/matita/contribs/RELATIONAL/Zah/setoid.ma
deleted file mode 100644 (file)
index 681d633..0000000
+++ /dev/null
@@ -1,60 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/Zah/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.
-
-theorem zeq_refl: \forall z. z = z.
- unfold ZEq. intros. auto.
-qed.
-
-theorem zeq_sym: \forall z1,z2. z1 = z2 \to z2 = z1.
- unfold ZEq. intros. lapply linear (H n). 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.
-
-*)
diff --git a/helm/software/matita/contribs/RELATIONAL/datatypes/Zah.ma b/helm/software/matita/contribs/RELATIONAL/datatypes/Zah.ma
new file mode 100644 (file)
index 0000000..87f61d7
--- /dev/null
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/datatypes/Zah".
+
+include "datatypes/Nat.ma".
+
+definition Zah \def Nat \times Nat.
index 050d9deced0d08130996f06eb30c2ef133b0e56a..d52da97017d54775de591a7d91acb3ecebac11c4 100644 (file)
@@ -16,3 +16,4 @@ set "baseuri" "cic:/matita/RELATIONAL/preamble".
 
 include "logic/equality.ma".
 include "logic/connectives.ma".
+include "datatypes/constructors.ma".