set "baseuri" "cic:/matita/nat/nat".
+include "datatypes/bool.ma".
include "logic/equality.ma".
include "logic/connectives.ma".
include "higher_order_defs/functions.ma".
[ 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.
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.
[ 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.
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
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.
+