From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 25 Mar 2010 18:00:49 +0000 (+0000)
Subject: Z.ma updated to reflect changes in the logical Not operator
X-Git-Tag: make_still_working~2958
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b229b2d85552d78fcbce805248f87559f7f6df8;p=helm.git

Z.ma updated to reflect changes in the logical Not operator

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma
index 7a0f7f080..9045a6d8a 100644
--- a/helm/software/matita/nlibrary/arithmetics/Z.ma
+++ b/helm/software/matita/nlibrary/arithmetics/Z.ma
@@ -55,7 +55,7 @@ ntheorem OZ_test_to_Prop : ∀z:Z.
   |false ⇒ z ≠ OZ].
 #z;ncases z
 ##[napply refl
-##|##*:#z1;#H;ndestruct]
+##|##*:#z1;napply nmk;#H;ndestruct]
 nqed.
 
 (* discrimination *)
@@ -74,34 +74,37 @@ nqed.
 \def injective_neg. *)
 
 ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n.
-#n;#H;ndestruct;
+#n;napply nmk;#H;ndestruct;
 nqed.
 
 ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
-#n;#H;ndestruct;
+#n;napply nmk;#H;ndestruct;
 nqed.
 
 ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
-#n;#m;#H;ndestruct;
+#n;#m;napply nmk;#H;ndestruct;
 nqed.
 
 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
 #x;#y;ncases x;
 ##[ncases y;
    ##[@;//
-   ##|##*:#n;@2;#H;ndestruct]
+   ##|##*:#n;@2;napply nmk;#H;ndestruct]
 ##|#n;ncases y;
-   ##[@2;#H;ndestruct;
+   ##[@2;napply nmk;#H;ndestruct;
    ##|#m;ncases (decidable_eq_nat n m);#H;
       ##[nrewrite > H;@;//
-      ##|@2;#H2;napply H;ndestruct;//]
-   ##|#m;@2;#H;ndestruct]
+      ##|@2;napply nmk;#H2;nelim H;
+         (* bug if you don't introduce H3 *)#H3;ndestruct;
+         napply H3;@]
+   ##|#m;@2;napply nmk;#H;ndestruct]
 ##|#n;ncases y;
-   ##[@2;#H;ndestruct;
-   ##|#m;@2;#H;ndestruct
+   ##[@2;napply nmk;#H;ndestruct;
+   ##|#m;@2;napply nmk;#H;ndestruct
    ##|#m;ncases (decidable_eq_nat n m);#H;
       ##[nrewrite > H;@;//
-      ##|@2;#H2;napply H;ndestruct;//]##]##]
+      ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
+         napply H3;@]##]##]
 nqed.
 
 ndefinition Zsucc ≝
@@ -180,7 +183,7 @@ interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
 
 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
 #x;ncases x
-##[//
+##[napply nmk;//
 ##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
 nqed.
 
@@ -276,7 +279,7 @@ ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
 ##|#n;ncases y
    ##[##1,2:ncases n;//
    ##|#p;ncases n;nnormalize;
-      ##[napply not_le_Sn_O (* XXX: auto? *)
+      ##[#H;nelim (not_le_Sn_O p);#H2;napply H2;//; (* XXX: auto? *)
       ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
    ##]
 ##]
@@ -315,17 +318,17 @@ ntheorem eqZb_to_Prop:
    ##|napply not_eq_OZ_pos (* XXX: auto? *)
    ##|napply not_eq_OZ_neg (* XXX: auto? *)]
 ##|#n;ncases y;
-   ##[#H;napply not_eq_OZ_pos;//;
+   ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
    ##|#m;napply eqb_elim;
       ##[//
-      ##|#H;#H2;napply H;ndestruct;//]
+      ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
    ##|#m;napply not_eq_pos_neg]
 ##|#n;ncases y
-   ##[#H;napply not_eq_OZ_neg;//;
-   ##|#m;#H;ndestruct
+   ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
+   ##|#m;napply nmk;#H;ndestruct
    ##|#m;napply eqb_elim;
       ##[//
-      ##|#H;#H2;napply H;ndestruct;//]
+      ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
    ##]
 ##]
 nqed.