1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/compare".
17 include "datatypes/bool.ma".
18 include "datatypes/compare.ma".
19 include "nat/orders.ma".
26 | (S q) \Rightarrow false]
30 | (S q) \Rightarrow eqb p q]].
32 theorem eqb_to_Prop: \forall n,m:nat.
34 [ true \Rightarrow n = m
35 | false \Rightarrow n \neq m].
38 (\lambda n,m:nat.match (eqb n m) with
39 [ true \Rightarrow n = m
40 | false \Rightarrow n \neq m])).
43 simplify.apply not_eq_O_S.
46 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
48 generalize in match H.
50 simplify.apply eq_f.apply H1.
51 simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
54 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
55 (n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)).
59 [ true \Rightarrow n = m
60 | false \Rightarrow n \neq m] \to (P (eqb n m))).
61 apply Hcut.apply eqb_to_Prop.
67 theorem eqb_n_n: \forall n. eqb n n = true.
68 intro.elim n.simplify.reflexivity.
72 theorem eqb_true_to_eq: \forall n,m:nat.
73 eqb n m = true \to n = m.
77 [ true \Rightarrow n = m
78 | false \Rightarrow n \neq m].
83 theorem eqb_false_to_not_eq: \forall n,m:nat.
84 eqb n m = false \to n \neq m.
88 [ true \Rightarrow n = m
89 | false \Rightarrow n \neq m].
94 theorem eq_to_eqb_true: \forall n,m:nat.
95 n = m \to eqb n m = true.
96 intros.apply (eqb_elim n m).
98 intros.apply False_ind.apply (H1 H).
101 theorem not_eq_to_eqb_false: \forall n,m:nat.
102 \lnot (n = m) \to eqb n m = false.
103 intros.apply (eqb_elim n m).
104 intros. apply False_ind.apply (H H1).
113 [ O \Rightarrow false
114 | (S q) \Rightarrow leb p q]].
116 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop.
117 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
119 apply nat_elim2; intros; simplify
120 [apply H.apply le_O_n
121 |apply H1.apply not_le_Sn_O.
123 [apply H1.apply le_S_S.assumption.
124 |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption
130 theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m.
133 [intro.left.assumption
134 |intro.right.assumption
139 theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true.
140 intros.apply leb_elim;intros
142 |apply False_ind.apply H1.apply H.
146 theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false.
147 intros.apply leb_elim;intros
148 [apply False_ind.apply (le_to_not_lt ? ? H1). assumption
153 theorem leb_to_Prop: \forall n,m:nat.
155 [ true \Rightarrow n \leq m
156 | false \Rightarrow n \nleq m].
157 apply nat_elim2;simplify
161 elim ((leb n m));simplify
162 [apply le_S_S.apply H
163 |unfold Not.intros.apply H.apply le_S_S_to_le.assumption
169 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop.
170 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
174 (match (leb n m) with
175 [ true \Rightarrow n \leq m
176 | false \Rightarrow n \nleq m] \to (P (leb n m))).
177 apply Hcut.apply leb_to_Prop.
184 definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
186 theorem ltb_to_Prop :
201 | apply (not_eq_to_le_to_lt ? ? H H1)
205 | apply le_to_not_lt;
206 generalize in match (not_le_to_lt ? ? H1);
214 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
215 (n < m → (P true)) → (n ≮ m → (P false)) →
219 (match (ltb n m) with
221 | false ⇒ n ≮ m] → (P (ltb n m))).
222 apply Hcut.apply ltb_to_Prop.
228 let rec nat_compare n m: compare \def
233 | (S q) \Rightarrow LT ]
237 | (S q) \Rightarrow nat_compare p q]].
239 theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
241 simplify.reflexivity.
245 theorem nat_compare_S_S: \forall n,m:nat.
246 nat_compare n m = nat_compare (S n) (S m).
247 intros.simplify.reflexivity.
250 theorem nat_compare_pred_pred:
251 \forall n,m:nat.lt O n \to lt O m \to
252 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
254 apply (lt_O_n_elim n H).
255 apply (lt_O_n_elim m H1).
257 simplify.reflexivity.
260 theorem nat_compare_to_Prop: \forall n,m:nat.
261 match (nat_compare n m) with
262 [ LT \Rightarrow n < m
264 | GT \Rightarrow m < n ].
266 apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
267 [ LT \Rightarrow n < m
269 | GT \Rightarrow m < n ])).
270 intro.elim n1.simplify.reflexivity.
271 simplify.unfold lt.apply le_S_S.apply le_O_n.
272 intro.simplify.unfold lt.apply le_S_S. apply le_O_n.
273 intros 2.simplify.elim ((nat_compare n1 m1)).
274 simplify. unfold lt. apply le_S_S.apply H.
275 simplify. apply eq_f. apply H.
276 simplify. unfold lt.apply le_S_S.apply H.
279 theorem nat_compare_n_m_m_n: \forall n,m:nat.
280 nat_compare n m = compare_invert (nat_compare m n).
282 apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))).
283 intros.elim n1.simplify.reflexivity.
284 simplify.reflexivity.
285 intro.elim n1.simplify.reflexivity.
286 simplify.reflexivity.
287 intros.simplify.elim H.reflexivity.
290 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
291 (n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to
292 (P (nat_compare n m)).
294 cut (match (nat_compare n m) with
295 [ LT \Rightarrow n < m
297 | GT \Rightarrow m < n] \to
298 (P (nat_compare n m))).
299 apply Hcut.apply nat_compare_to_Prop.
300 elim ((nat_compare n m)).