changed default parameter values...

[helm.git] / helm / matita / library / nat / nat.ma

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index f84ffef44cd44bb8da092f5011c48b483cb8e8e0..df045daa732e5310d93245c2164610c74d350ae8 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/nat/nat".
 
 include "logic/equality.ma".
 include "logic/connectives.ma".
+include "datatypes/bool.ma".
 include "higher_order_defs/functions.ma".
 
 inductive nat : Set \def
@@ -27,8 +28,7 @@ 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))).
+theorem pred_Sn : \forall n:nat.n=(pred (S n)).
 intros; reflexivity.
 qed.
 
@@ -40,12 +40,11 @@ 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)).
+\lnot n=m \to \lnot (S n = S m).
 intros. simplify. intros.
 apply H. apply injective_S. assumption.
 qed.
@@ -56,14 +55,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)).
+theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
 intros. simplify. 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. \lnot n=S n.
 intros.elim n.
 apply not_eq_O_S.
 apply not_eq_S.assumption.
@@ -86,3 +85,17 @@ apply nat_case m.apply H1.
 intros.apply H2. apply H3.
 qed.
 
+theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
+intros.simplify.
+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.
+