Moved compare in a different file.

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

diff --git a/helm/software/matita/nlibrary/arithmetics/compare.ma b/helm/software/matita/nlibrary/arithmetics/compare.ma
new file mode 100644 (file)
index 0000000..68e1411
--- /dev/null
+++ b/helm/software/matita/nlibrary/arithmetics/compare.ma
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(*       ___                                                             *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+
+ninductive compare : Type[0] ≝
+| LT : compare
+| EQ : compare
+| GT : compare.
+
+ndefinition compare_invert: compare → compare ≝
+  λc.match c with
+      [ LT ⇒ GT
+      | EQ ⇒ EQ
+      | GT ⇒ LT ].
+
+nlet rec nat_compare n m: compare ≝
+match n with
+[ O ⇒ match m with 
+      [ O ⇒ EQ
+      | (S q) ⇒ LT ]
+| S p ⇒ match m with 
+      [ O ⇒ GT
+      | S q ⇒ nat_compare p q]].
+
+ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ.
+#n;nelim n
+##[//
+##|#m;#IH;nnormalize;//]
+nqed.
+
+ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m).
+//;
+nqed.
+
+ntheorem nat_compare_pred_pred: 
+  ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m).
+#n;#m;#Hn;#Hm;
+napply (lt_O_n_elim n Hn);
+napply (lt_O_n_elim m Hm);
+#p;#q;//;
+nqed.
+
+ntheorem nat_compare_to_Prop: 
+  ∀n,m.match (nat_compare n m) with
+    [ LT ⇒ n < m
+    | EQ ⇒ n = m
+    | GT ⇒ m < n ].
+#n;#m;
+napply (nat_elim2 (λn,m.match (nat_compare n m) with
+  [ LT ⇒ n < m
+  | EQ ⇒ n = m
+  | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
+##[##1,2:#n1;ncases n1;//;
+##|#n1;#m1;nnormalize;ncases (nat_compare n1 m1);
+   ##[##1,3:nnormalize;#IH;napply le_S_S;//;
+   ##|nnormalize;#IH;nrewrite > IH;//]
+nqed.
+
+ntheorem nat_compare_n_m_m_n: 
+  ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n).
+#n;#m;
+napply (nat_elim2 (λn,m. nat_compare n m = compare_invert (nat_compare m n)))
+##[##1,2:#n1;ncases n1;//;
+##|#n1;#m1;#IH;nnormalize;napply IH]
+nqed.
+     
+ntheorem nat_compare_elim : 
+  ∀n,m. ∀P:compare → Prop.
+    (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (nat_compare n m).
+#n;#m;#P;#Hlt;#Heq;#Hgt;
+ncut (match (nat_compare n m) with
+    [ LT ⇒ n < m
+    | EQ ⇒ n=m
+    | GT ⇒ m < n] →
+  P (nat_compare n m))
+##[ncases (nat_compare n m);
+   ##[napply Hlt
+   ##|napply Heq
+   ##|napply Hgt]
+##|#Hcut;napply Hcut;//;
+nqed.
+
+ninductive cmp_cases (n,m:nat) : CProp[0] ≝
+  | cmp_le : n ≤ m → cmp_cases n m
+  | cmp_gt : m < n → cmp_cases n m.
+
+ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m.
+(* sic 
+#n;#m;#H;nelim H
+##[//
+##|/2/] *)
+/2/; nqed.
+
+nlemma cmp_nat: ∀n,m.cmp_cases n m.
+#n;#m; nlapply (nat_compare_to_Prop n m);
+ncases (nat_compare n m);nnormalize; /3/; 
+nqed.

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index fe9ef8267ffc064e1d50f9e3283b6f0c5e0c3660..54ff253c22404a443b6a39879aebf9211f1873f4 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -17,11 +17,7 @@ include "hints_declaration.ma".
 include "basics/functions.ma".
 include "basics/eq.ma".
 
-ntheorem foo: ∀A:Type.∀a,b:A.∀f:A→A.∀g:A→A→A.
-(∀x,y.f (g x y) = x) → ∀x. g (f a) x = b → f a = f b.
-//; nqed.
-
-ninductive nat : Type[0] ≝
+ninductive nat : Type ≝
   | O : nat
   | S : nat → nat.
   
@@ -40,7 +36,7 @@ ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on
 *)
 
 ndefinition pred ≝
- λn. match n with [ O ⇒  O | (S p) ⇒ p].
+ λn. match n with [ O ⇒ O | S p ⇒ p].
 
 ntheorem pred_Sn : ∀n. n = pred (S n).
 //; nqed.
@@ -278,6 +274,7 @@ ntheorem monotonic_pred: monotonic ? le pred.
 
 ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
 (* XXX *) nletin hint ≝ monotonic. 
+#a; #b; #H; napplyS monotonic_pred;
 /2/; nqed.
 
 (* this are instances of the le versions 
@@ -566,7 +563,6 @@ ntheorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
 
 ntheorem monotonic_le_plus_l: 
 ∀m:nat.monotonic nat le (λn.n + m).
-#m; #x; #y; #H; napplyS monotonic_le_plus_r;
 /2/; nqed.
 
 (*
@@ -1156,98 +1152,3 @@ ntheorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
 #n; #m; #Hltb; napply lt_to_leb_false; /2/;
 nqed. *)
 
-ninductive compare : Type[0] ≝
-| LT : compare
-| EQ : compare
-| GT : compare.
-
-ndefinition compare_invert: compare → compare ≝
-  λc.match c with
-      [ LT ⇒ GT
-      | EQ ⇒ EQ
-      | GT ⇒ LT ].
-
-nlet rec nat_compare n m: compare ≝
-match n with
-[ O ⇒ match m with 
-      [ O ⇒ EQ
-      | (S q) ⇒ LT ]
-| S p ⇒ match m with 
-      [ O ⇒ GT
-      | S q ⇒ nat_compare p q]].
-
-ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ.
-#n;nelim n
-##[//
-##|#m;#IH;nnormalize;//]
-nqed.
-
-ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m).
-//;
-nqed.
-
-ntheorem nat_compare_pred_pred: 
-  ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m).
-#n;#m;#Hn;#Hm;
-napply (lt_O_n_elim n Hn);
-napply (lt_O_n_elim m Hm);
-#p;#q;//;
-nqed.
-
-ntheorem nat_compare_to_Prop: 
-  ∀n,m.match (nat_compare n m) with
-    [ LT ⇒ n < m
-    | EQ ⇒ n = m
-    | GT ⇒ m < n ].
-#n;#m;
-napply (nat_elim2 (λn,m.match (nat_compare n m) with
-  [ LT ⇒ n < m
-  | EQ ⇒ n = m
-  | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
-##[##1,2:#n1;ncases n1;//;
-##|#n1;#m1;nnormalize;ncases (nat_compare n1 m1);
-   ##[##1,3:nnormalize;#IH;napply le_S_S;//;
-   ##|nnormalize;#IH;nrewrite > IH;//]
-nqed.
-
-ntheorem nat_compare_n_m_m_n: 
-  ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n).
-#n;#m;
-napply (nat_elim2 (λn,m. nat_compare n m = compare_invert (nat_compare m n)))
-##[##1,2:#n1;ncases n1;//;
-##|#n1;#m1;#IH;nnormalize;napply IH]
-nqed.
-     
-ntheorem nat_compare_elim : 
-  ∀n,m. ∀P:compare → Prop.
-    (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (nat_compare n m).
-#n;#m;#P;#Hlt;#Heq;#Hgt;
-ncut (match (nat_compare n m) with
-    [ LT ⇒ n < m
-    | EQ ⇒ n=m
-    | GT ⇒ m < n] →
-  P (nat_compare n m))
-##[ncases (nat_compare n m);
-   ##[napply Hlt
-   ##|napply Heq
-   ##|napply Hgt]
-##|#Hcut;napply Hcut;//;
-nqed.
-
-ninductive cmp_cases (n,m:nat) : CProp[0] ≝
-  | cmp_le : n ≤ m → cmp_cases n m
-  | cmp_gt : m < n → cmp_cases n m.
-
-ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m.
-#n;#m;#H;nelim H
-##[//
-##|/2/]
-nqed.
-
-nlemma cmp_nat: ∀n,m.cmp_cases n m.
-#n;#m; nlapply (nat_compare_to_Prop n m);
-ncases (nat_compare n m);#H
-##[@;napply lt_to_le;//
-##|@;//
-##|@2;//]
-nqed.