branch for universe

[helm.git] / matita / contribs / library_auto / auto / nat / nat.ma

diff --git a/matita/contribs/library_auto/auto/nat/nat.ma b/matita/contribs/library_auto/auto/nat/nat.ma
new file mode 100644 (file)
index 0000000..f915759
--- /dev/null
+++ b/matita/contribs/library_auto/auto/nat/nat.ma
@@ -0,0 +1,151 @@
+(**************************************************************************)
+(*       ___                                                                 *)
+(*      ||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         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/library_autobatch/nat/nat".
+
+include "higher_order_defs/functions.ma".
+
+inductive nat : Set \def
+  | O : nat
+  | S : nat \to nat.
+
+definition pred: nat \to nat \def
+ \lambda n:nat. match n with
+ [ O \Rightarrow  O
+ | (S p) \Rightarrow p ].
+
+theorem pred_Sn : \forall n:nat.n=(pred (S n)).
+  autobatch.
+ (*intros. reflexivity.*)
+qed.
+
+theorem injective_S : injective nat nat S.
+ unfold injective.
+ intros.
+ rewrite > pred_Sn.
+ rewrite > (pred_Sn y).
+ autobatch.
+ (*apply eq_f. 
+ assumption.*)
+qed.
+
+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. 
+ \lnot n=m \to S n \neq S m.
+ intros.
+ unfold Not. 
+ intros.
+ autobatch.
+ (*apply H. 
+ apply injective_S.
+ assumption.*)
+qed.
+
+definition not_zero : nat \to Prop \def
+ \lambda n: nat.
+  match n with
+  [ O \Rightarrow False
+  | (S p) \Rightarrow True ].
+
+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. n \neq S n.
+ intros.
+ elim n
+ [apply not_eq_O_S
+ |apply not_eq_S.assumption]
+qed.
+
+theorem nat_case:
+ \forall n:nat.\forall P:nat \to Prop. 
+  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
+  [ autobatch
+    (*apply H;
+    reflexivity*)
+  | autobatch
+    (*apply H2;
+    reflexivity*) ]
+qed.
+
+theorem nat_elim2 :
+ \forall R:nat \to nat \to Prop.
+  (\forall n:nat. R O n) 
+  \to (\forall n:nat. R (S n) O) 
+  \to (\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
+    |intro;
+     autobatch
+     (*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
+   [autobatch
+    (*left; 
+    reflexivity*)
+   |autobatch 
+   (*right; 
+   apply not_eq_O_S*) ]
+ | intro;
+   right; 
+   intro; 
+   apply (not_eq_O_S n1);
+   autobatch 
+   (*apply sym_eq; 
+   assumption*)
+ | intros; elim H
+   [  autobatch
+      (*left; 
+      apply eq_f; 
+      assumption*)
+   | right;
+     intro;
+     autobatch 
+     (*apply H1; 
+     apply inj_S; 
+     assumption*) 
+   ] 
+ ]
+qed.