X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnat.ma;h=a75032d7123b7018f40af65285712d5c3c4da9c1;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=ff41ba62e25e2844b18240ddf80ba36a0bc52cdf;hpb=244d65f63ca6a736b871f9f91328fe8c5524ff05;p=helm.git

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index ff41ba62e..a75032d71 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -1,5 +1,5 @@
 (**************************************************************************)
-(*       ___	                                                            *)
+(*       ___	                                                          *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
 (*      ||T||                                                             *)
@@ -14,8 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/nat".
 
-include "logic/equality.ma".
-include "logic/connectives.ma".
 include "higher_order_defs/functions.ma".
 
 inductive nat : Set \def
@@ -27,26 +25,24 @@ definition pred: nat \to nat \def
 [ O \Rightarrow  O
 | (S p) \Rightarrow p ].
 
-theorem pred_Sn : \forall n:nat.
-(eq nat n (pred (S n))).
-intros; reflexivity.
+theorem pred_Sn : \forall n:nat.n=(pred (S n)).
+intros. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.
-simplify.
+unfold injective.
 intros.
 rewrite > pred_Sn.
-rewrite > pred_Sn y.
+rewrite > (pred_Sn y).
 apply eq_f. assumption.
 qed.
 
-theorem inj_S : \forall n,m:nat. 
-(eq nat (S n) (S m)) \to (eq nat n m)
+theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 \def injective_S.
 
 theorem not_eq_S  : \forall n,m:nat. 
-Not (eq nat n m) \to Not (eq nat (S n) (S m)).
-intros. simplify. intros.
+\lnot n=m \to S n \neq S m.
+intros. unfold Not. intros.
 apply H. apply injective_S. assumption.
 qed.
 
@@ -56,14 +52,14 @@ definition not_zero : nat \to Prop \def
   [ O \Rightarrow False
   | (S p) \Rightarrow True ].
 
-theorem not_eq_O_S : \forall n:nat. Not (eq nat O (S n)).
-intros. simplify. intros.
+theorem not_eq_O_S : \forall n:nat. O \neq S n.
+intros. unfold Not. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
 qed.
 
-theorem not_eq_n_Sn : \forall n:nat. Not (eq nat n (S n)).
+theorem not_eq_n_Sn : \forall n:nat. n \neq S n.
 intros.elim n.
 apply not_eq_O_S.
 apply not_eq_S.assumption.
@@ -75,6 +71,14 @@ P O \to  (\forall m:nat. P (S m)) \to P n.
 intros.elim n.assumption.apply H1.
 qed.
 
+theorem nat_case1:
+\forall n:nat.\forall P:nat \to Prop. 
+(n=O \to P O) \to  (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
+intros 2.elim n.
+apply H.reflexivity.
+apply H2.reflexivity.
+qed.
+
 theorem nat_elim2 :
 \forall R:nat \to nat \to Prop.
 (\forall n:nat. R O n) \to 
@@ -82,7 +86,21 @@ theorem nat_elim2 :
 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 intros 5.elim n.
 apply H.
-apply nat_case m.apply H1.
+apply (nat_case m).apply H1.
 intros.apply H2. apply H3.
 qed.
 
+theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
+intros.unfold decidable.
+apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
+intro.elim n1.
+left.reflexivity.
+right.apply not_eq_O_S.
+intro.right.intro.
+apply (not_eq_O_S n1).
+apply sym_eq.assumption.
+intros.elim H.
+left.apply eq_f. assumption.
+right.intro.apply H1.apply inj_S.assumption.
+qed.
+