From 6b229b2d85552d78fcbce805248f87559f7f6df8 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 25 Mar 2010 18:00:49 +0000 Subject: [PATCH] Z.ma updated to reflect changes in the logical Not operator From: ricciott --- .../software/matita/nlibrary/arithmetics/Z.ma | 39 ++++++++++--------- 1 file changed, 21 insertions(+), 18 deletions(-) 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. -- 2.39.2