commit by user lroversi

[helm.git] / weblib / lroversi / nat.ma

diff --git a/weblib/lroversi/nat.ma b/weblib/lroversi/nat.ma
new file mode 100644 (file)
index 0000000..aad1828
--- /dev/null
+++ b/weblib/lroversi/nat.ma
@@ -0,0 +1,70 @@
+include "hints_declaration.ma".
+include "basics/eq.ma".
+
+ninductive nat : Type ≝
+  | O : nat
+  | S : nat → nat.
+  
+interpretation "Natural numbers" 'N = nat.
+
+alias num (instance 0) = "nnatural number".
+
+(*
+nrecord pos : Type ≝
+ {n:>nat; is_pos: n ≠ 0}.
+
+ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on 
+*)
+
+(* default "natural numbers" cic:/matita/ng/arithmetics/nat/nat.ind.
+*)
+
+ndefinition pred ≝
+ λn. match n with [ O ⇒ O | S p ⇒ p].
+
+ntheorem pred_Sn : ∀n. n = pred (S n).
+//; nqed.
+
+ntheorem injective_S : injective nat nat S.
+//; nqed.
+
+(*
+ntheorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
+//. nqed. *)
+
+ntheorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/3/; nqed.
+
+ndefinition not_zero: nat → Prop ≝
+ λn: nat. match n with
+  [ O ⇒ False | (S p) ⇒ True ].
+  
+ntheorem not_eq_O_S : ∀n:nat. O ≠ S n.
+#n; napply nmk; #eqOS; nchange with (not_zero O); 
+nrewrite > eqOS; //.
+nqed.
+
+ntheorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
+#n; nelim n;/2/; nqed.
+
+ntheorem nat_case:
+ ∀n:nat.∀P:nat → Prop. 
+  (n=O → P O) → (∀m:nat. (n=(S m) → P (S m))) → P n.
+#n; #P; nelim n; /2/; nqed.
+
+ntheorem nat_elim2 :
+ ∀R:nat → nat → Prop.
+  (∀n:nat. R O n) 
+  → (∀n:nat. R (S n) O)
+  → (∀n,m:nat. R n m → R (S n) (S m))
+  → ∀n,m:nat. R n m.
+#R; #ROn; #RSO; #RSS; #n; nelim n;//;
+#n0; #Rn0m; #m; ncases m;/2/; nqed.
+
+ntheorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
+napply nat_elim2; #n;
+ ##[ ncases n; /2/;
+ ##| /3/;
+ ##| #m; #Hind; ncases Hind;/3/;
+ ##]
+nqed.