1 include "basics/relations.ma".
2 include "basics/bool.ma".
6 inductive nat : Type[0] ≝
10 interpretation "Natural numbers" 'N = nat.
12 alias num (instance 0) = "natural number".
15 λn. match n with [ O ⇒ O | S p ⇒ p].
17 definition not_zero: nat → Prop ≝
18 λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
22 inductive le (n:nat) : nat → Prop ≝
24 | le_S : ∀ m:nat. le n m → le n (S m).
26 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
28 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
30 definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
32 interpretation "natural 'less than'" 'lt x y = (lt x y).
34 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
36 (* abstract properties *)
38 definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
40 (* arithmetic operations *)
43 match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
45 interpretation "natural plus" 'plus x y = (plus x y).
47 (* Generic conclusion ******************************************************)
51 (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
52 #n #P (elim n) /2/ qed.
58 → (∀n,m:nat. R n m → R (S n) (S m))
60 #R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
62 lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
65 (* Equalities ***************************************************************)
67 theorem pred_Sn : ∀n. n = pred (S n).
70 theorem injective_S : injective nat nat S.
71 #a #b #H >(pred_Sn a) >(pred_Sn b) @eq_f // qed.
73 theorem S_pred: ∀n. O < n → S(pred n) = n.
74 #n #posn (cases posn) //
77 theorem plus_O_n: ∀n:nat. n = O + n.
80 theorem plus_n_O: ∀n:nat. n = n + O.
81 #n (elim n) normalize // qed.
83 theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
84 #n (elim n) normalize // qed.
86 theorem commutative_plus: commutative ? plus.
87 #n (elim n) normalize // qed.
89 theorem associative_plus : associative nat plus.
90 #n (elim n) normalize // qed.
92 theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
95 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
96 #n (elim n) normalize /3/ qed.
98 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
103 theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
104 #n #m #Hlt (elim Hlt) // qed.
108 theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
109 #n #m #lenm (elim lenm) /2/ qed.
111 theorem le_O_n : ∀n:nat. O ≤ n.
114 theorem le_n_Sn : ∀n:nat. n ≤ S n.
117 theorem transitive_le : transitive nat le.
118 #a #b #c #leab #lebc (elim lebc) /2/
121 theorem le_pred_n : ∀n:nat. pred n ≤ n.
124 theorem monotonic_pred: monotonic ? le pred.
125 #n #m #lenm (elim lenm) /2/ qed.
127 theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
131 theorem monotonic_le_plus_r:
132 ∀n:nat.monotonic nat le (λm.n + m).
133 #n #a #b (elim n) normalize //
134 #m #H #leab @le_S_S /2/ qed.
136 theorem monotonic_le_plus_l:
137 ∀m:nat.monotonic nat le (λn.n + m).
140 theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
142 #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
145 theorem le_plus_n :∀n,m:nat. m ≤ n + m.
148 lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
151 lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
154 theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
157 theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
160 theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
161 #a (elim a) normalize /3/ qed.
163 theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
168 theorem transitive_lt: transitive nat lt.
169 #a #b #c #ltab #ltbc (elim ltbc) /2/
172 theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
173 #n #m #p #H #H1 (elim H1) /2/ qed.
175 theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
176 #n #m #p #H (elim H) /3/ qed.
178 theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
181 theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
184 theorem lt_O_S : ∀n:nat. O < S n.
187 theorem monotonic_lt_plus_r:
188 ∀n:nat.monotonic nat lt (λm.n+m).
191 theorem monotonic_lt_plus_l:
192 ∀n:nat.monotonic nat lt (λm.m+n).
195 theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
196 #n #m #p #q #ltnm #ltpq
197 @(transitive_lt ? (n+q))/2/ qed.
199 theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
202 theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
205 theorem increasing_to_monotonic: ∀f:nat → nat.
206 increasing f → monotonic nat lt f.
207 #f #incr #n #m #ltnm (elim ltnm) /2/
212 theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
213 #n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
215 theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
218 theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
221 theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
224 theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
225 #n #m #Hltnm (elim Hltnm) /3/ qed.
227 theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
231 |#m #Hind #HnotleSS @le_S_S /3/
237 theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
240 theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
241 #n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
243 (*********************** boolean arithmetics ********************)
248 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
249 | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqbnat p q]
252 theorem eqbnat_elim : ∀ n,m:nat.∀ P:bool → Prop.
253 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqbnat n m)).
255 [#n (cases n) normalize /3/
261 theorem eqbnat_n_n: ∀n. eqbnat n n = true.
262 #n (elim n) normalize // qed.
264 theorem eqbnat_true_to_eq: ∀n,m:nat. eqbnat n m = true → n = m.
265 #n #m @(eqbnat_elim n m) // #_ #abs @False_ind /2/ qed.
267 (* theorem eqb_false_to_not_eq: ∀n,m:nat. eqbnat n m = false → n ≠ m.
268 #n #m @(eqbnat_elim n m) /2/ qed. *)
270 theorem eq_to_eqbnat_true: ∀n,m:nat.n = m → eqbnat n m = true.