]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/compare.ma
...
[helm.git] / helm / software / matita / library / nat / compare.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "datatypes/bool.ma".
16 include "datatypes/compare.ma".
17 include "nat/orders.ma".
18
19 let rec eqb n m \def 
20 match n with 
21   [ O \Rightarrow 
22      match m with 
23      [ O \Rightarrow true
24            | (S q) \Rightarrow false] 
25   | (S p) \Rightarrow
26            match m with 
27      [ O \Rightarrow false
28            | (S q) \Rightarrow eqb p q]].
29            
30 theorem eqb_to_Prop: \forall n,m:nat. 
31 match (eqb n m) with
32 [ true  \Rightarrow n = m 
33 | false \Rightarrow n \neq m].
34 intros.
35 apply (nat_elim2
36 (\lambda n,m:nat.match (eqb n m) with
37 [ true  \Rightarrow n = m 
38 | false \Rightarrow n \neq m])).
39 intro.elim n1.
40 simplify.reflexivity.
41 simplify.apply not_eq_O_S.
42 intro.
43 simplify.unfold Not.
44 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
45 intros.simplify.
46 generalize in match H.
47 elim ((eqb n1 m1)).
48 simplify.apply eq_f.apply H1.
49 simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
50 qed.
51
52 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
53 (n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)). 
54 intros.
55 cut 
56 (match (eqb n m) with
57 [ true  \Rightarrow n = m
58 | false \Rightarrow n \neq m] \to (P (eqb n m))).
59 apply Hcut.apply eqb_to_Prop.
60 elim (eqb n m).
61 apply ((H H2)).
62 apply ((H1 H2)).
63 qed.
64
65 theorem eqb_n_n: \forall n. eqb n n = true.
66 intro.elim n.simplify.reflexivity.
67 simplify.assumption.
68 qed.
69
70 theorem eqb_true_to_eq: \forall n,m:nat.
71 eqb n m = true \to n = m.
72 intros.
73 change with 
74 match true with
75 [ true  \Rightarrow n = m 
76 | false \Rightarrow n \neq m].
77 rewrite < H.
78 apply eqb_to_Prop. 
79 qed.
80
81 theorem eqb_false_to_not_eq: \forall n,m:nat.
82 eqb n m = false \to n \neq m.
83 intros.
84 change with 
85 match false with
86 [ true  \Rightarrow n = m 
87 | false \Rightarrow n \neq m].
88 rewrite < H.
89 apply eqb_to_Prop. 
90 qed.
91
92 theorem eq_to_eqb_true: \forall n,m:nat.
93 n = m \to eqb n m = true.
94 intros.apply (eqb_elim n m).
95 intros. reflexivity.
96 intros.apply False_ind.apply (H1 H).
97 qed.
98
99 theorem not_eq_to_eqb_false: \forall n,m:nat.
100 \lnot (n = m) \to eqb n m = false.
101 intros.apply (eqb_elim n m).
102 intros. apply False_ind.apply (H H1).
103 intros.reflexivity.
104 qed.
105
106 let rec leb n m \def 
107 match n with 
108     [ O \Rightarrow true
109     | (S p) \Rightarrow
110         match m with 
111         [ O \Rightarrow false
112         | (S q) \Rightarrow leb p q]].
113
114 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
115 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
116 P (leb n m).
117 apply nat_elim2; intros; simplify
118   [apply H.apply le_O_n
119   |apply H1.apply not_le_Sn_O.
120   |apply H;intros
121     [apply H1.apply le_S_S.assumption.
122     |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption
123     ]
124   ]
125 qed.
126
127 theorem leb_true_to_le:\forall n,m.
128 leb n m = true \to (n \le m).
129 intros 2.
130 apply leb_elim
131   [intros.assumption
132   |intros.destruct H1.
133   ]
134 qed.
135
136 theorem leb_false_to_not_le:\forall n,m.
137 leb n m = false \to \lnot (n \le m).
138 intros 2.
139 apply leb_elim
140   [intros.destruct H1
141   |intros.assumption
142   ]
143 qed.
144 (*
145 theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. 
146 intros.
147 apply (leb_elim n m)
148   [intro.left.assumption
149   |intro.right.assumption
150   ]
151 qed.
152 *)
153
154 theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true.
155 intros.apply leb_elim;intros
156   [reflexivity
157   |apply False_ind.apply H1.apply H.
158   ]
159 qed.
160
161 theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false.
162 intros.apply leb_elim;intros
163   [apply False_ind.apply (le_to_not_lt ? ? H1). assumption
164   |reflexivity
165   ]
166 qed.
167
168 theorem leb_to_Prop: \forall n,m:nat. 
169 match (leb n m) with
170 [ true  \Rightarrow n \leq m 
171 | false \Rightarrow n \nleq m].
172 apply nat_elim2;simplify
173   [exact le_O_n
174   |exact not_le_Sn_O
175   |intros 2.simplify.
176    elim ((leb n m));simplify
177     [apply le_S_S.apply H
178     |unfold Not.intros.apply H.apply le_S_S_to_le.assumption
179     ]
180   ]
181 qed.
182
183 (*
184 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
185 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
186 P (leb n m).
187 intros.
188 cut 
189 (match (leb n m) with
190 [ true  \Rightarrow n \leq m
191 | false \Rightarrow n \nleq m] \to (P (leb n m))).
192 apply Hcut.apply leb_to_Prop.
193 elim (leb n m).
194 apply ((H H2)).
195 apply ((H1 H2)).
196 qed.
197 *)
198
199 definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
200
201 theorem ltb_to_Prop :
202  ∀n,m.
203   match ltb n m with
204   [ true ⇒ n < m
205   | false ⇒ n ≮ m
206   ].
207 intros;
208 unfold ltb;
209 apply leb_elim;
210 apply eqb_elim;
211 intros;
212 simplify;
213 [ rewrite < H;
214   apply le_to_not_lt;
215   constructor 1
216 | apply (not_eq_to_le_to_lt ? ? H H1)
217 | rewrite < H;
218   apply le_to_not_lt;
219   constructor 1
220 | apply le_to_not_lt;
221   generalize in match (not_le_to_lt ? ? H1);
222   clear H1;
223   intro;
224   apply lt_to_le;
225   assumption
226 ].
227 qed.
228
229 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
230 (n < m → (P true)) → (n ≮ m → (P false)) →
231 P (ltb n m).
232 intros.
233 cut
234 (match (ltb n m) with
235 [ true  ⇒ n < m
236 | false ⇒ n ≮ m] → (P (ltb n m))).
237 apply Hcut.apply ltb_to_Prop.
238 elim (ltb n m).
239 apply ((H H2)).
240 apply ((H1 H2)).
241 qed.
242
243 let rec nat_compare n m: compare \def
244 match n with
245 [ O \Rightarrow 
246     match m with 
247       [ O \Rightarrow EQ
248       | (S q) \Rightarrow LT ]
249 | (S p) \Rightarrow 
250     match m with 
251       [ O \Rightarrow GT
252       | (S q) \Rightarrow nat_compare p q]].
253
254 theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
255 intro.elim n.
256 simplify.reflexivity.
257 simplify.assumption.
258 qed.
259
260 theorem nat_compare_S_S: \forall n,m:nat. 
261 nat_compare n m = nat_compare (S n) (S m).
262 intros.simplify.reflexivity.
263 qed.
264
265 theorem nat_compare_pred_pred: 
266 \forall n,m:nat.lt O n \to lt O m \to 
267 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
268 intros.
269 apply (lt_O_n_elim n H).
270 apply (lt_O_n_elim m H1).
271 intros.
272 simplify.reflexivity.
273 qed.
274
275 theorem nat_compare_to_Prop: \forall n,m:nat. 
276 match (nat_compare n m) with
277   [ LT \Rightarrow n < m
278   | EQ \Rightarrow n=m
279   | GT \Rightarrow m < n ].
280 intros.
281 apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
282   [ LT \Rightarrow n < m
283   | EQ \Rightarrow n=m
284   | GT \Rightarrow m < n ])).
285 intro.elim n1.simplify.reflexivity.
286 simplify.unfold lt.apply le_S_S.apply le_O_n.
287 intro.simplify.unfold lt.apply le_S_S. apply le_O_n.
288 intros 2.simplify.elim ((nat_compare n1 m1)).
289 simplify. unfold lt. apply le_S_S.apply H.
290 simplify. apply eq_f. apply H.
291 simplify. unfold lt.apply le_S_S.apply H.
292 qed.
293
294 theorem nat_compare_n_m_m_n: \forall n,m:nat. 
295 nat_compare n m = compare_invert (nat_compare m n).
296 intros. 
297 apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))).
298 intros.elim n1.simplify.reflexivity.
299 simplify.reflexivity.
300 intro.elim n1.simplify.reflexivity.
301 simplify.reflexivity.
302 intros.simplify.elim H.reflexivity.
303 qed.
304      
305 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
306 (n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to 
307 (P (nat_compare n m)).
308 intros.
309 cut (match (nat_compare n m) with
310 [ LT \Rightarrow n < m
311 | EQ \Rightarrow n=m
312 | GT \Rightarrow m < n] \to
313 (P (nat_compare n m))).
314 apply Hcut.apply nat_compare_to_Prop.
315 elim ((nat_compare n m)).
316 apply ((H H3)).
317 apply ((H1 H3)).
318 apply ((H2 H3)).
319 qed.
320
321 inductive cmp_cases (n,m:nat) : CProp ≝
322   | cmp_le : n ≤ m → cmp_cases n m
323   | cmp_gt : m < n → cmp_cases n m.
324
325 lemma cmp_nat: ∀n,m.cmp_cases n m.
326 intros; generalize in match (nat_compare_to_Prop n m);
327 cases (nat_compare n m); intros;
328 [constructor 1;apply lt_to_le|constructor 1;rewrite > H|constructor 2]
329 try assumption; apply le_n;
330 qed.