X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2Fnat.ma;h=f15f8cbc858becfb524e6259b644cf6a7b841230;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=fe9ef8267ffc064e1d50f9e3283b6f0c5e0c3660;hpb=fb0a4ba033da3ea305e0add8c2ec4573e95fa3d2;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index fe9ef8267..f15f8cbc8 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -12,16 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* include "higher_order_defs/functions.ma". *)
 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 +35,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.
@@ -84,7 +79,7 @@ ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
 napply nat_elim2; #n;
  ##[ ncases n; /2/;
  ##| /3/;
- ##| #m; #Hind; ncases Hind; /3/;
+ ##| #m; #Hind; ncases Hind;/3/;
  ##]
 nqed. 
 
@@ -128,7 +123,7 @@ ntheorem associative_plus : associative nat plus.
 #n; nelim n; nnormalize; //; nqed.
 
 ntheorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
-//; nqed.
+//; nqed. 
 
 ntheorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 #n; nelim n; nnormalize; /3/; nqed.
@@ -262,6 +257,9 @@ ntheorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
 ntheorem le_O_n : ∀n:nat. O ≤ n.
 #n; nelim n; /2/; nqed.
 
+ntheorem nboh: 0 ≤ 0 + 0.
+//; nqed.
+
 ntheorem le_n_Sn : ∀n:nat. n ≤ S n.
 /2/; nqed.
 
@@ -277,7 +275,6 @@ ntheorem monotonic_pred: monotonic ? le pred.
 #n; #m; #lenm; nelim lenm; /2/;nqed.
 
 ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
-(* XXX *) nletin hint ≝ monotonic. 
 /2/; nqed.
 
 (* this are instances of the le versions 
@@ -453,7 +450,8 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 (* le and eq *)
 
 ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-napply nat_elim2; /4/; nqed. 
+napply nat_elim2; /4/;
+nqed. 
 
 ntheorem lt_O_S : ∀n:nat. O < S n.
 /2/; nqed.
@@ -566,7 +564,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.
 
 (*
@@ -890,7 +887,7 @@ ntheorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
 
 ntheorem plus_minus_m_m: ∀n,m:nat.
   m ≤ n → n = (n-m)+m.
-#n; #m; #lemn; napplyS symmetric_eq; 
+#n; #m; #lemn; napplyS sym_eq; 
 napplyS (plus_minus m n m); //; nqed.
 
 ntheorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
@@ -909,7 +906,7 @@ nqed.
 ntheorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
 (* /4/ done in 43.5 *)
 #n; #m; #p; #eqp; 
-napply symmetric_eq;
+napply sym_eq;
 napplyS (minus_plus_m_m p m);
 nqed.
 
@@ -1049,15 +1046,14 @@ simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
 qed.
 *)
 
-naxiom eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
+ntheorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
-(*
 napply nat_elim2; 
   ##[#n; ncases n; nnormalize; /3/; 
   ##|nnormalize; /3/;
   ##|nnormalize; /4/; 
   ##] 
-nqed.*)
+nqed.
 
 ntheorem eqb_n_n: ∀n. eqb n n = true.
 #n; nelim n; nnormalize; //.
@@ -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.