1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* *) |
---|
7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
9 | (* under the terms of the GNU General Public License as published by *) |
---|
10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
11 | (* (at your option) any later version. This file is also distributed *) |
---|
12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
13 | (* *) |
---|
14 | (* *********************************************************************) |
---|
15 | |
---|
16 | (* * This file collects a number of definitions and theorems that are |
---|
17 | used throughout the development. It complements the Coq standard |
---|
18 | library. *) |
---|
19 | |
---|
20 | include "basics/types.ma". |
---|
21 | include "basics/lists/list.ma". |
---|
22 | |
---|
23 | include "ASM/Util.ma". |
---|
24 | |
---|
25 | (* |
---|
26 | (** * Logical axioms *) |
---|
27 | |
---|
28 | (** We use two logical axioms that are not provable in Coq but consistent |
---|
29 | with the logic: function extensionality and proof irrelevance. |
---|
30 | These are used in the memory model to show that two memory states |
---|
31 | that have identical contents are equal. *) |
---|
32 | |
---|
33 | Axiom extensionality: |
---|
34 | forall (A B: Type) (f g : A -> B), |
---|
35 | (forall x, f x = g x) -> f = g. |
---|
36 | |
---|
37 | Axiom proof_irrelevance: |
---|
38 | forall (P: Prop) (p1 p2: P), p1 = p2. |
---|
39 | |
---|
40 | (** * Useful tactics *) |
---|
41 | |
---|
42 | Ltac inv H := inversion H; clear H; subst. |
---|
43 | |
---|
44 | Ltac predSpec pred predspec x y := |
---|
45 | generalize (predspec x y); case (pred x y); intro. |
---|
46 | |
---|
47 | Ltac caseEq name := |
---|
48 | generalize (refl_equal name); pattern name at -1 in |- *; case name. |
---|
49 | |
---|
50 | Ltac destructEq name := |
---|
51 | generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro. |
---|
52 | |
---|
53 | Ltac decEq := |
---|
54 | match goal with |
---|
55 | | [ |- _ = _ ] => f_equal |
---|
56 | | [ |- (?X ?A <> ?X ?B) ] => |
---|
57 | cut (A <> B); [intro; congruence | try discriminate] |
---|
58 | end. |
---|
59 | |
---|
60 | Ltac byContradiction := |
---|
61 | cut False; [contradiction|idtac]. |
---|
62 | |
---|
63 | Ltac omegaContradiction := |
---|
64 | cut False; [contradiction|omega]. |
---|
65 | |
---|
66 | Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q. |
---|
67 | Proof. auto. Qed. |
---|
68 | |
---|
69 | Ltac exploit x := |
---|
70 | refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
71 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
72 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
73 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
74 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
75 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
76 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
77 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
78 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
79 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
80 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
81 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
82 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
83 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
84 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
85 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
86 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
87 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
88 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
89 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
90 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
91 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
92 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
93 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _) |
---|
94 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _) |
---|
95 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _) |
---|
96 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _) |
---|
97 | || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _) |
---|
98 | || refine (modusponens _ _ (x _ _ _ _ _ _ _) _) |
---|
99 | || refine (modusponens _ _ (x _ _ _ _ _ _) _) |
---|
100 | || refine (modusponens _ _ (x _ _ _ _ _) _) |
---|
101 | || refine (modusponens _ _ (x _ _ _ _) _) |
---|
102 | || refine (modusponens _ _ (x _ _ _) _) |
---|
103 | || refine (modusponens _ _ (x _ _) _) |
---|
104 | || refine (modusponens _ _ (x _) _). |
---|
105 | |
---|
106 | (** * Definitions and theorems over the type [positive] *) |
---|
107 | |
---|
108 | Definition peq (x y: positive): {x = y} + {x <> y}. |
---|
109 | Proof. |
---|
110 | intros. caseEq (Pcompare x y Eq). |
---|
111 | intro. left. apply Pcompare_Eq_eq; auto. |
---|
112 | intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. |
---|
113 | intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. |
---|
114 | Qed. |
---|
115 | |
---|
116 | Lemma peq_true: |
---|
117 | forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a. |
---|
118 | Proof. |
---|
119 | intros. case (peq x x); intros. |
---|
120 | auto. |
---|
121 | elim n; auto. |
---|
122 | Qed. |
---|
123 | |
---|
124 | Lemma peq_false: |
---|
125 | forall (A: Type) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b. |
---|
126 | Proof. |
---|
127 | intros. case (peq x y); intros. |
---|
128 | elim H; auto. |
---|
129 | auto. |
---|
130 | Qed. |
---|
131 | |
---|
132 | Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y). |
---|
133 | |
---|
134 | Lemma Plt_ne: |
---|
135 | forall (x y: positive), Plt x y -> x <> y. |
---|
136 | Proof. |
---|
137 | unfold Plt; intros. red; intro. subst y. omega. |
---|
138 | Qed. |
---|
139 | Hint Resolve Plt_ne: coqlib. |
---|
140 | |
---|
141 | Lemma Plt_trans: |
---|
142 | forall (x y z: positive), Plt x y -> Plt y z -> Plt x z. |
---|
143 | Proof. |
---|
144 | unfold Plt; intros; omega. |
---|
145 | Qed. |
---|
146 | |
---|
147 | Remark Psucc_Zsucc: |
---|
148 | forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x). |
---|
149 | Proof. |
---|
150 | intros. rewrite Pplus_one_succ_r. |
---|
151 | reflexivity. |
---|
152 | Qed. |
---|
153 | |
---|
154 | Lemma Plt_succ: |
---|
155 | forall (x: positive), Plt x (Psucc x). |
---|
156 | Proof. |
---|
157 | intro. unfold Plt. rewrite Psucc_Zsucc. omega. |
---|
158 | Qed. |
---|
159 | Hint Resolve Plt_succ: coqlib. |
---|
160 | |
---|
161 | Lemma Plt_trans_succ: |
---|
162 | forall (x y: positive), Plt x y -> Plt x (Psucc y). |
---|
163 | Proof. |
---|
164 | intros. apply Plt_trans with y. assumption. apply Plt_succ. |
---|
165 | Qed. |
---|
166 | Hint Resolve Plt_succ: coqlib. |
---|
167 | |
---|
168 | Lemma Plt_succ_inv: |
---|
169 | forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y. |
---|
170 | Proof. |
---|
171 | intros x y. unfold Plt. rewrite Psucc_Zsucc. |
---|
172 | intro. assert (A: (Zpos x < Zpos y)%Z \/ Zpos x = Zpos y). omega. |
---|
173 | elim A; intro. left; auto. right; injection H0; auto. |
---|
174 | Qed. |
---|
175 | |
---|
176 | Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}. |
---|
177 | Proof. |
---|
178 | intros. unfold Plt. apply Z_lt_dec. |
---|
179 | Qed. |
---|
180 | |
---|
181 | Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q). |
---|
182 | |
---|
183 | Lemma Ple_refl: forall (p: positive), Ple p p. |
---|
184 | Proof. |
---|
185 | unfold Ple; intros; omega. |
---|
186 | Qed. |
---|
187 | |
---|
188 | Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r. |
---|
189 | Proof. |
---|
190 | unfold Ple; intros; omega. |
---|
191 | Qed. |
---|
192 | |
---|
193 | Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q. |
---|
194 | Proof. |
---|
195 | unfold Plt, Ple; intros; omega. |
---|
196 | Qed. |
---|
197 | |
---|
198 | Lemma Ple_succ: forall (p: positive), Ple p (Psucc p). |
---|
199 | Proof. |
---|
200 | intros. apply Plt_Ple. apply Plt_succ. |
---|
201 | Qed. |
---|
202 | |
---|
203 | Lemma Plt_Ple_trans: |
---|
204 | forall (p q r: positive), Plt p q -> Ple q r -> Plt p r. |
---|
205 | Proof. |
---|
206 | unfold Plt, Ple; intros; omega. |
---|
207 | Qed. |
---|
208 | |
---|
209 | Lemma Plt_strict: forall p, ~ Plt p p. |
---|
210 | Proof. |
---|
211 | unfold Plt; intros. omega. |
---|
212 | Qed. |
---|
213 | |
---|
214 | Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. |
---|
215 | |
---|
216 | (** Peano recursion over positive numbers. *) |
---|
217 | |
---|
218 | Section POSITIVE_ITERATION. |
---|
219 | |
---|
220 | Lemma Plt_wf: well_founded Plt. |
---|
221 | Proof. |
---|
222 | apply well_founded_lt_compat with nat_of_P. |
---|
223 | intros. apply nat_of_P_lt_Lt_compare_morphism. exact H. |
---|
224 | Qed. |
---|
225 | |
---|
226 | Variable A: Type. |
---|
227 | Variable v1: A. |
---|
228 | Variable f: positive -> A -> A. |
---|
229 | |
---|
230 | Lemma Ppred_Plt: |
---|
231 | forall x, x <> xH -> Plt (Ppred x) x. |
---|
232 | Proof. |
---|
233 | intros. elim (Psucc_pred x); intro. contradiction. |
---|
234 | set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ. |
---|
235 | Qed. |
---|
236 | |
---|
237 | Let iter (x: positive) (P: forall y, Plt y x -> A) : A := |
---|
238 | match peq x xH with |
---|
239 | | left EQ => v1 |
---|
240 | | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ)) |
---|
241 | end. |
---|
242 | |
---|
243 | Definition positive_rec : positive -> A := |
---|
244 | Fix Plt_wf (fun _ => A) iter. |
---|
245 | |
---|
246 | Lemma unroll_positive_rec: |
---|
247 | forall x, |
---|
248 | positive_rec x = iter x (fun y _ => positive_rec y). |
---|
249 | Proof. |
---|
250 | unfold positive_rec. apply (Fix_eq Plt_wf (fun _ => A) iter). |
---|
251 | intros. unfold iter. case (peq x 1); intro. auto. decEq. apply H. |
---|
252 | Qed. |
---|
253 | |
---|
254 | Lemma positive_rec_base: |
---|
255 | positive_rec 1%positive = v1. |
---|
256 | Proof. |
---|
257 | rewrite unroll_positive_rec. unfold iter. case (peq 1 1); intro. |
---|
258 | auto. elim n; auto. |
---|
259 | Qed. |
---|
260 | |
---|
261 | Lemma positive_rec_succ: |
---|
262 | forall x, positive_rec (Psucc x) = f x (positive_rec x). |
---|
263 | Proof. |
---|
264 | intro. rewrite unroll_positive_rec. unfold iter. |
---|
265 | case (peq (Psucc x) 1); intro. |
---|
266 | destruct x; simpl in e; discriminate. |
---|
267 | rewrite Ppred_succ. auto. |
---|
268 | Qed. |
---|
269 | |
---|
270 | Lemma positive_Peano_ind: |
---|
271 | forall (P: positive -> Prop), |
---|
272 | P xH -> |
---|
273 | (forall x, P x -> P (Psucc x)) -> |
---|
274 | forall x, P x. |
---|
275 | Proof. |
---|
276 | intros. |
---|
277 | apply (well_founded_ind Plt_wf P). |
---|
278 | intros. |
---|
279 | case (peq x0 xH); intro. |
---|
280 | subst x0; auto. |
---|
281 | elim (Psucc_pred x0); intro. contradiction. rewrite <- H2. |
---|
282 | apply H0. apply H1. apply Ppred_Plt. auto. |
---|
283 | Qed. |
---|
284 | |
---|
285 | End POSITIVE_ITERATION. |
---|
286 | |
---|
287 | (** * Definitions and theorems over the type [Z] *) |
---|
288 | |
---|
289 | Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec. |
---|
290 | |
---|
291 | Lemma zeq_true: |
---|
292 | forall (A: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a. |
---|
293 | Proof. |
---|
294 | intros. case (zeq x x); intros. |
---|
295 | auto. |
---|
296 | elim n; auto. |
---|
297 | Qed. |
---|
298 | |
---|
299 | Lemma zeq_false: |
---|
300 | forall (A: Type) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b. |
---|
301 | Proof. |
---|
302 | intros. case (zeq x y); intros. |
---|
303 | elim H; auto. |
---|
304 | auto. |
---|
305 | Qed. |
---|
306 | |
---|
307 | Open Scope Z_scope. |
---|
308 | |
---|
309 | Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec. |
---|
310 | |
---|
311 | Lemma zlt_true: |
---|
312 | forall (A: Type) (x y: Z) (a b: A), |
---|
313 | x < y -> (if zlt x y then a else b) = a. |
---|
314 | Proof. |
---|
315 | intros. case (zlt x y); intros. |
---|
316 | auto. |
---|
317 | omegaContradiction. |
---|
318 | Qed. |
---|
319 | |
---|
320 | Lemma zlt_false: |
---|
321 | forall (A: Type) (x y: Z) (a b: A), |
---|
322 | x >= y -> (if zlt x y then a else b) = b. |
---|
323 | Proof. |
---|
324 | intros. case (zlt x y); intros. |
---|
325 | omegaContradiction. |
---|
326 | auto. |
---|
327 | Qed. |
---|
328 | |
---|
329 | Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec. |
---|
330 | |
---|
331 | Lemma zle_true: |
---|
332 | forall (A: Type) (x y: Z) (a b: A), |
---|
333 | x <= y -> (if zle x y then a else b) = a. |
---|
334 | Proof. |
---|
335 | intros. case (zle x y); intros. |
---|
336 | auto. |
---|
337 | omegaContradiction. |
---|
338 | Qed. |
---|
339 | |
---|
340 | Lemma zle_false: |
---|
341 | forall (A: Type) (x y: Z) (a b: A), |
---|
342 | x > y -> (if zle x y then a else b) = b. |
---|
343 | Proof. |
---|
344 | intros. case (zle x y); intros. |
---|
345 | omegaContradiction. |
---|
346 | auto. |
---|
347 | Qed. |
---|
348 | *) |
---|
349 | (* * Properties of powers of two. *) |
---|
350 | (* |
---|
351 | lemma two_power_nat_O : two_power_nat O = one. |
---|
352 | // qed. |
---|
353 | |
---|
354 | lemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0. |
---|
355 | // qed. |
---|
356 | |
---|
357 | lemma two_power_nat_two_p: |
---|
358 | ∀x. Z_two_power_nat x = two_p (Z_of_nat x). |
---|
359 | #x cases x |
---|
360 | [ // |
---|
361 | | normalize #p elim p // #p' #H >(nat_succ_pos …) // |
---|
362 | ] qed.*) |
---|
363 | (* |
---|
364 | Lemma two_p_monotone: |
---|
365 | forall x y, 0 <= x <= y -> two_p x <= two_p y. |
---|
366 | Proof. |
---|
367 | intros. |
---|
368 | replace (two_p x) with (two_p x * 1) by omega. |
---|
369 | replace y with (x + (y - x)) by omega. |
---|
370 | rewrite two_p_is_exp; try omega. |
---|
371 | apply Zmult_le_compat_l. |
---|
372 | assert (two_p (y - x) > 0). apply two_p_gt_ZERO. omega. omega. |
---|
373 | assert (two_p x > 0). apply two_p_gt_ZERO. omega. omega. |
---|
374 | Qed. |
---|
375 | |
---|
376 | Lemma two_p_monotone_strict: |
---|
377 | forall x y, 0 <= x < y -> two_p x < two_p y. |
---|
378 | Proof. |
---|
379 | intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; omega. |
---|
380 | assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. omega. |
---|
381 | replace y with (Zsucc (y - 1)) by omega. rewrite two_p_S. omega. omega. |
---|
382 | Qed. |
---|
383 | |
---|
384 | Lemma two_p_strict: |
---|
385 | forall x, x >= 0 -> x < two_p x. |
---|
386 | Proof. |
---|
387 | intros x0 GT. pattern x0. apply natlike_ind. |
---|
388 | simpl. omega. |
---|
389 | intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). omega. |
---|
390 | omega. |
---|
391 | Qed. |
---|
392 | |
---|
393 | Lemma two_p_strict_2: |
---|
394 | forall x, x >= 0 -> 2 * x - 1 < two_p x. |
---|
395 | Proof. |
---|
396 | intros. assert (x = 0 \/ x - 1 >= 0) by omega. destruct H0. |
---|
397 | subst. vm_compute. auto. |
---|
398 | replace (two_p x) with (2 * two_p (x - 1)). |
---|
399 | generalize (two_p_strict _ H0). omega. |
---|
400 | rewrite <- two_p_S. decEq. omega. omega. |
---|
401 | Qed. |
---|
402 | |
---|
403 | (** Properties of [Zmin] and [Zmax] *) |
---|
404 | |
---|
405 | Lemma Zmin_spec: |
---|
406 | forall x y, Zmin x y = if zlt x y then x else y. |
---|
407 | Proof. |
---|
408 | intros. case (zlt x y); unfold Zlt, Zge; intros. |
---|
409 | unfold Zmin. rewrite z. auto. |
---|
410 | unfold Zmin. caseEq (x ?= y); intro. |
---|
411 | apply Zcompare_Eq_eq. auto. |
---|
412 | contradiction. |
---|
413 | reflexivity. |
---|
414 | Qed. |
---|
415 | |
---|
416 | Lemma Zmax_spec: |
---|
417 | forall x y, Zmax x y = if zlt y x then x else y. |
---|
418 | Proof. |
---|
419 | intros. case (zlt y x); unfold Zlt, Zge; intros. |
---|
420 | unfold Zmax. rewrite <- (Zcompare_antisym y x). |
---|
421 | rewrite z. simpl. auto. |
---|
422 | unfold Zmax. rewrite <- (Zcompare_antisym y x). |
---|
423 | caseEq (y ?= x); intro; simpl. |
---|
424 | symmetry. apply Zcompare_Eq_eq. auto. |
---|
425 | contradiction. reflexivity. |
---|
426 | Qed. |
---|
427 | |
---|
428 | Lemma Zmax_bound_l: |
---|
429 | forall x y z, x <= y -> x <= Zmax y z. |
---|
430 | Proof. |
---|
431 | intros. generalize (Zmax1 y z). omega. |
---|
432 | Qed. |
---|
433 | Lemma Zmax_bound_r: |
---|
434 | forall x y z, x <= z -> x <= Zmax y z. |
---|
435 | Proof. |
---|
436 | intros. generalize (Zmax2 y z). omega. |
---|
437 | Qed. |
---|
438 | |
---|
439 | (** Properties of Euclidean division and modulus. *) |
---|
440 | |
---|
441 | Lemma Zdiv_small: |
---|
442 | forall x y, 0 <= x < y -> x / y = 0. |
---|
443 | Proof. |
---|
444 | intros. assert (y > 0). omega. |
---|
445 | assert (forall a b, |
---|
446 | 0 <= a < y -> |
---|
447 | 0 <= y * b + a < y -> |
---|
448 | b = 0). |
---|
449 | intros. |
---|
450 | assert (b = 0 \/ b > 0 \/ (-b) > 0). omega. |
---|
451 | elim H3; intro. |
---|
452 | auto. |
---|
453 | elim H4; intro. |
---|
454 | assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. |
---|
455 | omegaContradiction. |
---|
456 | assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega. |
---|
457 | rewrite <- Zopp_mult_distr_r in H6. omegaContradiction. |
---|
458 | apply H1 with (x mod y). |
---|
459 | apply Z_mod_lt. auto. |
---|
460 | rewrite <- Z_div_mod_eq. auto. auto. |
---|
461 | Qed. |
---|
462 | |
---|
463 | Lemma Zmod_small: |
---|
464 | forall x y, 0 <= x < y -> x mod y = x. |
---|
465 | Proof. |
---|
466 | intros. assert (y > 0). omega. |
---|
467 | generalize (Z_div_mod_eq x y H0). |
---|
468 | rewrite (Zdiv_small x y H). omega. |
---|
469 | Qed. |
---|
470 | |
---|
471 | Lemma Zmod_unique: |
---|
472 | forall x y a b, |
---|
473 | x = a * y + b -> 0 <= b < y -> x mod y = b. |
---|
474 | Proof. |
---|
475 | intros. subst x. rewrite Zplus_comm. |
---|
476 | rewrite Z_mod_plus. apply Zmod_small. auto. omega. |
---|
477 | Qed. |
---|
478 | |
---|
479 | Lemma Zdiv_unique: |
---|
480 | forall x y a b, |
---|
481 | x = a * y + b -> 0 <= b < y -> x / y = a. |
---|
482 | Proof. |
---|
483 | intros. subst x. rewrite Zplus_comm. |
---|
484 | rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega. |
---|
485 | Qed. |
---|
486 | |
---|
487 | Lemma Zdiv_Zdiv: |
---|
488 | forall a b c, |
---|
489 | b > 0 -> c > 0 -> (a / b) / c = a / (b * c). |
---|
490 | Proof. |
---|
491 | intros. |
---|
492 | generalize (Z_div_mod_eq a b H). generalize (Z_mod_lt a b H). intros. |
---|
493 | generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros. |
---|
494 | set (q1 := a / b) in *. set (r1 := a mod b) in *. |
---|
495 | set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *. |
---|
496 | symmetry. apply Zdiv_unique with (r2 * b + r1). |
---|
497 | rewrite H2. rewrite H4. ring. |
---|
498 | split. |
---|
499 | assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega. |
---|
500 | assert ((r2 + 1) * b <= c * b). |
---|
501 | apply Zmult_le_compat_r. omega. omega. |
---|
502 | replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring. |
---|
503 | replace (c * b) with (b * c) in H5 by ring. |
---|
504 | omega. |
---|
505 | Qed. |
---|
506 | |
---|
507 | Lemma Zmult_le_compat_l_neg : |
---|
508 | forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m. |
---|
509 | Proof. |
---|
510 | intros. |
---|
511 | assert ((-p) * n >= (-p) * m). apply Zmult_ge_compat_l. auto. omega. |
---|
512 | replace (p * n) with (- ((-p) * n)) by ring. |
---|
513 | replace (p * m) with (- ((-p) * m)) by ring. |
---|
514 | omega. |
---|
515 | Qed. |
---|
516 | |
---|
517 | Lemma Zdiv_interval_1: |
---|
518 | forall lo hi a b, |
---|
519 | lo <= 0 -> hi > 0 -> b > 0 -> |
---|
520 | lo * b <= a < hi * b -> |
---|
521 | lo <= a/b < hi. |
---|
522 | Proof. |
---|
523 | intros. |
---|
524 | generalize (Z_div_mod_eq a b H1). generalize (Z_mod_lt a b H1). intros. |
---|
525 | set (q := a/b) in *. set (r := a mod b) in *. |
---|
526 | split. |
---|
527 | assert (lo < (q + 1)). |
---|
528 | apply Zmult_lt_reg_r with b. omega. |
---|
529 | apply Zle_lt_trans with a. omega. |
---|
530 | replace ((q + 1) * b) with (b * q + b) by ring. |
---|
531 | omega. |
---|
532 | omega. |
---|
533 | apply Zmult_lt_reg_r with b. omega. |
---|
534 | replace (q * b) with (b * q) by ring. |
---|
535 | omega. |
---|
536 | Qed. |
---|
537 | |
---|
538 | Lemma Zdiv_interval_2: |
---|
539 | forall lo hi a b, |
---|
540 | lo <= a <= hi -> lo <= 0 -> hi >= 0 -> b > 0 -> |
---|
541 | lo <= a/b <= hi. |
---|
542 | Proof. |
---|
543 | intros. |
---|
544 | assert (lo <= a / b < hi+1). |
---|
545 | apply Zdiv_interval_1. omega. omega. auto. |
---|
546 | assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega. |
---|
547 | replace (lo * 1) with lo in H3 by ring. |
---|
548 | assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega. |
---|
549 | replace ((hi + 1) * 1) with (hi + 1) in H4 by ring. |
---|
550 | omega. |
---|
551 | omega. |
---|
552 | Qed. |
---|
553 | |
---|
554 | (** Properties of divisibility. *) |
---|
555 | |
---|
556 | Lemma Zdivides_trans: |
---|
557 | forall x y z, (x | y) -> (y | z) -> (x | z). |
---|
558 | Proof. |
---|
559 | intros. inv H. inv H0. exists (q0 * q). ring. |
---|
560 | Qed. |
---|
561 | |
---|
562 | Definition Zdivide_dec: |
---|
563 | forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }. |
---|
564 | Proof. |
---|
565 | intros. destruct (zeq (Zmod q p) 0). |
---|
566 | left. exists (q / p). |
---|
567 | transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto. |
---|
568 | transitivity (p * (q / p)). omega. ring. |
---|
569 | right; red; intros. elim n. apply Z_div_exact_1; auto. |
---|
570 | inv H0. rewrite Z_div_mult; auto. ring. |
---|
571 | Defined. |
---|
572 | *) |
---|
573 | (* * Alignment: [align n amount] returns the smallest multiple of [amount] |
---|
574 | greater than or equal to [n]. *) |
---|
575 | (*naxiom align : Z → Z → Z.*) |
---|
576 | |
---|
577 | definition align : nat → nat → nat ≝ λn: nat. λamount: nat. |
---|
578 | ((minus (n + amount) 1) ÷ amount) * amount. |
---|
579 | (* |
---|
580 | Lemma align_le: forall x y, y > 0 -> x <= align x y. |
---|
581 | Proof. |
---|
582 | intros. unfold align. |
---|
583 | generalize (Z_div_mod_eq (x + y - 1) y H). intro. |
---|
584 | replace ((x + y - 1) / y * y) |
---|
585 | with ((x + y - 1) - (x + y - 1) mod y). |
---|
586 | generalize (Z_mod_lt (x + y - 1) y H). omega. |
---|
587 | rewrite Zmult_comm. omega. |
---|
588 | Qed. |
---|
589 | |
---|
590 | Lemma align_divides: forall x y, y > 0 -> (y | align x y). |
---|
591 | Proof. |
---|
592 | intros. unfold align. apply Zdivide_factor_l. |
---|
593 | Qed. |
---|
594 | |
---|
595 | (** * Definitions and theorems on the data types [option], [sum] and [list] *) |
---|
596 | |
---|
597 | Set Implicit Arguments. |
---|
598 | *) |
---|
599 | (* * Mapping a function over an option type. *) |
---|
600 | |
---|
601 | (* |
---|
602 | (** Mapping a function over a sum type. *) |
---|
603 | |
---|
604 | Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C := |
---|
605 | match x with |
---|
606 | | inl y => inl C (f y) |
---|
607 | | inr z => inr B z |
---|
608 | end. |
---|
609 | |
---|
610 | (** Properties of [List.nth] (n-th element of a list). *) |
---|
611 | |
---|
612 | Hint Resolve in_eq in_cons: coqlib. |
---|
613 | |
---|
614 | Lemma nth_error_in: |
---|
615 | forall (A: Type) (n: nat) (l: list A) (x: A), |
---|
616 | List.nth_error l n = Some x -> In x l. |
---|
617 | Proof. |
---|
618 | induction n; simpl. |
---|
619 | destruct l; intros. |
---|
620 | discriminate. |
---|
621 | injection H; intro; subst a. apply in_eq. |
---|
622 | destruct l; intros. |
---|
623 | discriminate. |
---|
624 | apply in_cons. auto. |
---|
625 | Qed. |
---|
626 | Hint Resolve nth_error_in: coqlib. |
---|
627 | |
---|
628 | Lemma nth_error_nil: |
---|
629 | forall (A: Type) (idx: nat), nth_error (@nil A) idx = None. |
---|
630 | Proof. |
---|
631 | induction idx; simpl; intros; reflexivity. |
---|
632 | Qed. |
---|
633 | Hint Resolve nth_error_nil: coqlib. |
---|
634 | |
---|
635 | (** Compute the length of a list, with result in [Z]. *) |
---|
636 | |
---|
637 | Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z := |
---|
638 | match l with |
---|
639 | | nil => acc |
---|
640 | | hd :: tl => list_length_z_aux tl (Zsucc acc) |
---|
641 | end. |
---|
642 | |
---|
643 | Remark list_length_z_aux_shift: |
---|
644 | forall (A: Type) (l: list A) n m, |
---|
645 | list_length_z_aux l n = list_length_z_aux l m + (n - m). |
---|
646 | Proof. |
---|
647 | induction l; intros; simpl. |
---|
648 | omega. |
---|
649 | replace (n - m) with (Zsucc n - Zsucc m) by omega. auto. |
---|
650 | Qed. |
---|
651 | |
---|
652 | Definition list_length_z (A: Type) (l: list A) : Z := |
---|
653 | list_length_z_aux l 0. |
---|
654 | |
---|
655 | Lemma list_length_z_cons: |
---|
656 | forall (A: Type) (hd: A) (tl: list A), |
---|
657 | list_length_z (hd :: tl) = list_length_z tl + 1. |
---|
658 | Proof. |
---|
659 | intros. unfold list_length_z. simpl. |
---|
660 | rewrite (list_length_z_aux_shift tl 1 0). omega. |
---|
661 | Qed. |
---|
662 | |
---|
663 | Lemma list_length_z_pos: |
---|
664 | forall (A: Type) (l: list A), |
---|
665 | list_length_z l >= 0. |
---|
666 | Proof. |
---|
667 | induction l; simpl. unfold list_length_z; simpl. omega. |
---|
668 | rewrite list_length_z_cons. omega. |
---|
669 | Qed. |
---|
670 | |
---|
671 | Lemma list_length_z_map: |
---|
672 | forall (A B: Type) (f: A -> B) (l: list A), |
---|
673 | list_length_z (map f l) = list_length_z l. |
---|
674 | Proof. |
---|
675 | induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence. |
---|
676 | Qed. |
---|
677 | |
---|
678 | (** Extract the n-th element of a list, as [List.nth_error] does, |
---|
679 | but the index [n] is of type [Z]. *) |
---|
680 | |
---|
681 | Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A := |
---|
682 | match l with |
---|
683 | | nil => None |
---|
684 | | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n) |
---|
685 | end. |
---|
686 | |
---|
687 | Lemma list_nth_z_in: |
---|
688 | forall (A: Type) (l: list A) n x, |
---|
689 | list_nth_z l n = Some x -> In x l. |
---|
690 | Proof. |
---|
691 | induction l; simpl; intros. |
---|
692 | congruence. |
---|
693 | destruct (zeq n 0). left; congruence. right; eauto. |
---|
694 | Qed. |
---|
695 | |
---|
696 | Lemma list_nth_z_map: |
---|
697 | forall (A B: Type) (f: A -> B) (l: list A) n, |
---|
698 | list_nth_z (List.map f l) n = option_map f (list_nth_z l n). |
---|
699 | Proof. |
---|
700 | induction l; simpl; intros. |
---|
701 | auto. |
---|
702 | destruct (zeq n 0). auto. eauto. |
---|
703 | Qed. |
---|
704 | |
---|
705 | Lemma list_nth_z_range: |
---|
706 | forall (A: Type) (l: list A) n x, |
---|
707 | list_nth_z l n = Some x -> 0 <= n < list_length_z l. |
---|
708 | Proof. |
---|
709 | induction l; simpl; intros. |
---|
710 | discriminate. |
---|
711 | rewrite list_length_z_cons. destruct (zeq n 0). |
---|
712 | generalize (list_length_z_pos l); omega. |
---|
713 | exploit IHl; eauto. unfold Zpred. omega. |
---|
714 | Qed. |
---|
715 | |
---|
716 | (** Properties of [List.incl] (list inclusion). *) |
---|
717 | |
---|
718 | Lemma incl_cons_inv: |
---|
719 | forall (A: Type) (a: A) (b c: list A), |
---|
720 | incl (a :: b) c -> incl b c. |
---|
721 | Proof. |
---|
722 | unfold incl; intros. apply H. apply in_cons. auto. |
---|
723 | Qed. |
---|
724 | Hint Resolve incl_cons_inv: coqlib. |
---|
725 | |
---|
726 | Lemma incl_app_inv_l: |
---|
727 | forall (A: Type) (l1 l2 m: list A), |
---|
728 | incl (l1 ++ l2) m -> incl l1 m. |
---|
729 | Proof. |
---|
730 | unfold incl; intros. apply H. apply in_or_app. left; assumption. |
---|
731 | Qed. |
---|
732 | |
---|
733 | Lemma incl_app_inv_r: |
---|
734 | forall (A: Type) (l1 l2 m: list A), |
---|
735 | incl (l1 ++ l2) m -> incl l2 m. |
---|
736 | Proof. |
---|
737 | unfold incl; intros. apply H. apply in_or_app. right; assumption. |
---|
738 | Qed. |
---|
739 | |
---|
740 | Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. |
---|
741 | |
---|
742 | Lemma incl_same_head: |
---|
743 | forall (A: Type) (x: A) (l1 l2: list A), |
---|
744 | incl l1 l2 -> incl (x::l1) (x::l2). |
---|
745 | Proof. |
---|
746 | intros; red; simpl; intros. intuition. |
---|
747 | Qed. |
---|
748 | |
---|
749 | (** Properties of [List.map] (mapping a function over a list). *) |
---|
750 | |
---|
751 | Lemma list_map_exten: |
---|
752 | forall (A B: Type) (f f': A -> B) (l: list A), |
---|
753 | (forall x, In x l -> f x = f' x) -> |
---|
754 | List.map f' l = List.map f l. |
---|
755 | Proof. |
---|
756 | induction l; simpl; intros. |
---|
757 | reflexivity. |
---|
758 | rewrite <- H. rewrite IHl. reflexivity. |
---|
759 | intros. apply H. tauto. |
---|
760 | tauto. |
---|
761 | Qed. |
---|
762 | |
---|
763 | Lemma list_map_compose: |
---|
764 | forall (A B C: Type) (f: A -> B) (g: B -> C) (l: list A), |
---|
765 | List.map g (List.map f l) = List.map (fun x => g(f x)) l. |
---|
766 | Proof. |
---|
767 | induction l; simpl. reflexivity. rewrite IHl; reflexivity. |
---|
768 | Qed. |
---|
769 | |
---|
770 | Lemma list_map_identity: |
---|
771 | forall (A: Type) (l: list A), |
---|
772 | List.map (fun (x:A) => x) l = l. |
---|
773 | Proof. |
---|
774 | induction l; simpl; congruence. |
---|
775 | Qed. |
---|
776 | |
---|
777 | Lemma list_map_nth: |
---|
778 | forall (A B: Type) (f: A -> B) (l: list A) (n: nat), |
---|
779 | nth_error (List.map f l) n = option_map f (nth_error l n). |
---|
780 | Proof. |
---|
781 | induction l; simpl; intros. |
---|
782 | repeat rewrite nth_error_nil. reflexivity. |
---|
783 | destruct n; simpl. reflexivity. auto. |
---|
784 | Qed. |
---|
785 | |
---|
786 | Lemma list_length_map: |
---|
787 | forall (A B: Type) (f: A -> B) (l: list A), |
---|
788 | List.length (List.map f l) = List.length l. |
---|
789 | Proof. |
---|
790 | induction l; simpl; congruence. |
---|
791 | Qed. |
---|
792 | *) (* |
---|
793 | lemma list_in_map_inv: |
---|
794 | ∀A,B: Type[0]. ∀f: A -> B. ∀l: list A. ∀y: B. |
---|
795 | in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l. |
---|
796 | #A B f l; nelim l; |
---|
797 | ##[ nnormalize; #y H; ninversion H; |
---|
798 | ##[ #x l' e1 e2; ndestruct; |
---|
799 | ##| #x z l' H1 H2 H3 H4; ndestruct; |
---|
800 | ##] |
---|
801 | ##| #x l' IH y H; ninversion H; |
---|
802 | ##[ nnormalize; #y' l'' e1 e2; ndestruct; @x; @; //; |
---|
803 | ##| nnormalize; #h h' t H1 H2 H3 H4; ndestruct; |
---|
804 | nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/; |
---|
805 | ##] |
---|
806 | ##] nqed.*) |
---|
807 | (* |
---|
808 | Lemma list_append_map: |
---|
809 | forall (A B: Type) (f: A -> B) (l1 l2: list A), |
---|
810 | List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2. |
---|
811 | Proof. |
---|
812 | induction l1; simpl; intros. |
---|
813 | auto. rewrite IHl1. auto. |
---|
814 | Qed. |
---|
815 | |
---|
816 | (** Properties of list membership. *) |
---|
817 | |
---|
818 | Lemma in_cns: |
---|
819 | forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l. |
---|
820 | Proof. |
---|
821 | intros. simpl. tauto. |
---|
822 | Qed. |
---|
823 | |
---|
824 | Lemma in_app: |
---|
825 | forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2. |
---|
826 | Proof. |
---|
827 | intros. split; intro. apply in_app_or. auto. apply in_or_app. auto. |
---|
828 | Qed. |
---|
829 | |
---|
830 | Lemma list_in_insert: |
---|
831 | forall (A: Type) (x: A) (l1 l2: list A) (y: A), |
---|
832 | In x (l1 ++ l2) -> In x (l1 ++ y :: l2). |
---|
833 | Proof. |
---|
834 | intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto. |
---|
835 | Qed. |
---|
836 | *) |
---|
837 | (* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements |
---|
838 | in common. *) |
---|
839 | (* |
---|
840 | definition list_disjoint : ∀A:Type[0]. list A → list A → Prop ≝ |
---|
841 | λA,l1,l2. |
---|
842 | ∀x,y: A. in_list A x l1 → in_list A y l2 → x ≠ y. |
---|
843 | |
---|
844 | lemma list_disjoint_cons_left: |
---|
845 | ∀A: Type[0]. ∀a: A. ∀l1,l2: list A. |
---|
846 | list_disjoint A (a :: l1) l2 → list_disjoint A l1 l2. |
---|
847 | #A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H; |
---|
848 | #x;#y;#in1;#in2; napply H; /2/; |
---|
849 | nqed. |
---|
850 | |
---|
851 | nlemma list_disjoint_cons_right: |
---|
852 | ∀A: Type. ∀a: A. ∀l1,l2: list A. |
---|
853 | list_disjoint A l1 (a :: l2) → list_disjoint A l1 l2. |
---|
854 | #A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H; |
---|
855 | #x;#y;#in1;#in2; napply H; /2/; |
---|
856 | nqed. |
---|
857 | |
---|
858 | nlemma list_disjoint_notin: |
---|
859 | ∀A: Type. ∀l1,l2: list A. ∀a: A. |
---|
860 | list_disjoint A l1 l2 → in_list A a l1 → ¬(in_list A a l2). |
---|
861 | #A;#l1;#l2;#a;nwhd in ⊢ (% → ?); #H; #H1; |
---|
862 | napply nmk; #H2; |
---|
863 | napply (absurd ?? (H … H1 H2)); //; |
---|
864 | nqed. |
---|
865 | |
---|
866 | nlemma list_disjoint_sym: |
---|
867 | ∀A: Type. ∀l1,l2: list A. |
---|
868 | list_disjoint A l1 l2 → list_disjoint A l2 l1. |
---|
869 | #A;#l1;#l2; |
---|
870 | nwhd in ⊢ (% → %); |
---|
871 | #H;#x;#y;#H1;#H2; napply sym_neq; /2/; |
---|
872 | nqed.*) |
---|
873 | |
---|
874 | (* |
---|
875 | Lemma list_disjoint_dec: |
---|
876 | forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A), |
---|
877 | {list_disjoint l1 l2} + {~list_disjoint l1 l2}. |
---|
878 | Proof. |
---|
879 | induction l1; intros. |
---|
880 | left; red; intros. elim H. |
---|
881 | case (In_dec eqA_dec a l2); intro. |
---|
882 | right; red; intro. apply (H a a); auto with coqlib. |
---|
883 | case (IHl1 l2); intro. |
---|
884 | left; red; intros. elim H; intro. |
---|
885 | red; intro; subst a y. contradiction. |
---|
886 | apply l; auto. |
---|
887 | right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto. |
---|
888 | Defined. |
---|
889 | |
---|
890 | (** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *) |
---|
891 | |
---|
892 | Definition list_equiv (A : Type) (l1 l2: list A) : Prop := |
---|
893 | forall x, In x l1 <-> In x l2. |
---|
894 | *) |
---|
895 | (* * [list_norepet l] holds iff the list [l] contains no repetitions, |
---|
896 | i.e. no element occurs twice. *) |
---|
897 | (* |
---|
898 | inductive list_norepet (A: Type[0]) : list A → Prop ≝ |
---|
899 | | list_norepet_nil: |
---|
900 | list_norepet A (nil A) |
---|
901 | | list_norepet_cons: |
---|
902 | ∀hd,tl. |
---|
903 | ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl).*) |
---|
904 | (* |
---|
905 | Lemma list_norepet_dec: |
---|
906 | forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A), |
---|
907 | {list_norepet l} + {~list_norepet l}. |
---|
908 | Proof. |
---|
909 | induction l. |
---|
910 | left; constructor. |
---|
911 | destruct IHl. |
---|
912 | case (In_dec eqA_dec a l); intro. |
---|
913 | right. red; intro. inversion H. contradiction. |
---|
914 | left. constructor; auto. |
---|
915 | right. red; intro. inversion H. contradiction. |
---|
916 | Defined. |
---|
917 | |
---|
918 | Lemma list_map_norepet: |
---|
919 | forall (A B: Type) (f: A -> B) (l: list A), |
---|
920 | list_norepet l -> |
---|
921 | (forall x y, In x l -> In y l -> x <> y -> f x <> f y) -> |
---|
922 | list_norepet (List.map f l). |
---|
923 | Proof. |
---|
924 | induction 1; simpl; intros. |
---|
925 | constructor. |
---|
926 | constructor. |
---|
927 | red; intro. generalize (list_in_map_inv f _ _ H2). |
---|
928 | intros [x [EQ IN]]. generalize EQ. change (f hd <> f x). |
---|
929 | apply H1. tauto. tauto. |
---|
930 | red; intro; subst x. contradiction. |
---|
931 | apply IHlist_norepet. intros. apply H1. tauto. tauto. auto. |
---|
932 | Qed. |
---|
933 | |
---|
934 | Remark list_norepet_append_commut: |
---|
935 | forall (A: Type) (a b: list A), |
---|
936 | list_norepet (a ++ b) -> list_norepet (b ++ a). |
---|
937 | Proof. |
---|
938 | intro A. |
---|
939 | assert (forall (x: A) (b: list A) (a: list A), |
---|
940 | list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) -> |
---|
941 | list_norepet (a ++ x :: b)). |
---|
942 | induction a; simpl; intros. |
---|
943 | constructor; auto. |
---|
944 | inversion H. constructor. red; intro. |
---|
945 | elim (in_app_or _ _ _ H6); intro. |
---|
946 | elim H4. apply in_or_app. tauto. |
---|
947 | elim H7; intro. subst a. elim H0. left. auto. |
---|
948 | elim H4. apply in_or_app. tauto. |
---|
949 | auto. |
---|
950 | induction a; simpl; intros. |
---|
951 | rewrite <- app_nil_end. auto. |
---|
952 | inversion H0. apply H. auto. |
---|
953 | red; intro; elim H3. apply in_or_app. tauto. |
---|
954 | red; intro; elim H3. apply in_or_app. tauto. |
---|
955 | Qed. |
---|
956 | |
---|
957 | Lemma list_norepet_app: |
---|
958 | forall (A: Type) (l1 l2: list A), |
---|
959 | list_norepet (l1 ++ l2) <-> |
---|
960 | list_norepet l1 /\ list_norepet l2 /\ list_disjoint l1 l2. |
---|
961 | Proof. |
---|
962 | induction l1; simpl; intros; split; intros. |
---|
963 | intuition. constructor. red;simpl;auto. |
---|
964 | tauto. |
---|
965 | inversion H; subst. rewrite IHl1 in H3. rewrite in_app in H2. |
---|
966 | intuition. |
---|
967 | constructor; auto. red; intros. elim H2; intro. congruence. auto. |
---|
968 | destruct H as [B [C D]]. inversion B; subst. |
---|
969 | constructor. rewrite in_app. intuition. elim (D a a); auto. apply in_eq. |
---|
970 | rewrite IHl1. intuition. red; intros. apply D; auto. apply in_cons; auto. |
---|
971 | Qed. |
---|
972 | |
---|
973 | Lemma list_norepet_append: |
---|
974 | forall (A: Type) (l1 l2: list A), |
---|
975 | list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 -> |
---|
976 | list_norepet (l1 ++ l2). |
---|
977 | Proof. |
---|
978 | generalize list_norepet_app; firstorder. |
---|
979 | Qed. |
---|
980 | |
---|
981 | Lemma list_norepet_append_right: |
---|
982 | forall (A: Type) (l1 l2: list A), |
---|
983 | list_norepet (l1 ++ l2) -> list_norepet l2. |
---|
984 | Proof. |
---|
985 | generalize list_norepet_app; firstorder. |
---|
986 | Qed. |
---|
987 | |
---|
988 | Lemma list_norepet_append_left: |
---|
989 | forall (A: Type) (l1 l2: list A), |
---|
990 | list_norepet (l1 ++ l2) -> list_norepet l1. |
---|
991 | Proof. |
---|
992 | generalize list_norepet_app; firstorder. |
---|
993 | Qed. |
---|
994 | |
---|
995 | (** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *) |
---|
996 | |
---|
997 | Inductive is_tail (A: Type): list A -> list A -> Prop := |
---|
998 | | is_tail_refl: |
---|
999 | forall c, is_tail c c |
---|
1000 | | is_tail_cons: |
---|
1001 | forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2). |
---|
1002 | |
---|
1003 | Lemma is_tail_in: |
---|
1004 | forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2. |
---|
1005 | Proof. |
---|
1006 | induction c2; simpl; intros. |
---|
1007 | inversion H. |
---|
1008 | inversion H. tauto. right; auto. |
---|
1009 | Qed. |
---|
1010 | |
---|
1011 | Lemma is_tail_cons_left: |
---|
1012 | forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2. |
---|
1013 | Proof. |
---|
1014 | induction c2; intros; inversion H. |
---|
1015 | constructor. constructor. constructor. auto. |
---|
1016 | Qed. |
---|
1017 | |
---|
1018 | Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. |
---|
1019 | |
---|
1020 | Lemma is_tail_incl: |
---|
1021 | forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2. |
---|
1022 | Proof. |
---|
1023 | induction 1; eauto with coqlib. |
---|
1024 | Qed. |
---|
1025 | |
---|
1026 | Lemma is_tail_trans: |
---|
1027 | forall (A: Type) (l1 l2: list A), |
---|
1028 | is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3. |
---|
1029 | Proof. |
---|
1030 | induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto. |
---|
1031 | Qed. |
---|
1032 | |
---|
1033 | (** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and |
---|
1034 | [P xi yi] holds for all [i]. *) |
---|
1035 | |
---|
1036 | Section FORALL2. |
---|
1037 | |
---|
1038 | Variable A: Type. |
---|
1039 | Variable B: Type. |
---|
1040 | Variable P: A -> B -> Prop. |
---|
1041 | |
---|
1042 | Inductive list_forall2: list A -> list B -> Prop := |
---|
1043 | | list_forall2_nil: |
---|
1044 | list_forall2 nil nil |
---|
1045 | | list_forall2_cons: |
---|
1046 | forall a1 al b1 bl, |
---|
1047 | P a1 b1 -> |
---|
1048 | list_forall2 al bl -> |
---|
1049 | list_forall2 (a1 :: al) (b1 :: bl). |
---|
1050 | |
---|
1051 | End FORALL2. |
---|
1052 | |
---|
1053 | Lemma list_forall2_imply: |
---|
1054 | forall (A B: Type) (P1: A -> B -> Prop) (l1: list A) (l2: list B), |
---|
1055 | list_forall2 P1 l1 l2 -> |
---|
1056 | forall (P2: A -> B -> Prop), |
---|
1057 | (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) -> |
---|
1058 | list_forall2 P2 l1 l2. |
---|
1059 | Proof. |
---|
1060 | induction 1; intros. |
---|
1061 | constructor. |
---|
1062 | constructor. auto with coqlib. apply IHlist_forall2; auto. |
---|
1063 | intros. auto with coqlib. |
---|
1064 | Qed. |
---|
1065 | |
---|
1066 | (** Dropping the first N elements of a list. *) |
---|
1067 | |
---|
1068 | Fixpoint list_drop (A: Type) (n: nat) (x: list A) {struct n} : list A := |
---|
1069 | match n with |
---|
1070 | | O => x |
---|
1071 | | S n' => match x with nil => nil | hd :: tl => list_drop n' tl end |
---|
1072 | end. |
---|
1073 | |
---|
1074 | Lemma list_drop_incl: |
---|
1075 | forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l. |
---|
1076 | Proof. |
---|
1077 | induction n; simpl; intros. auto. |
---|
1078 | destruct l; auto with coqlib. |
---|
1079 | Qed. |
---|
1080 | |
---|
1081 | Lemma list_drop_norepet: |
---|
1082 | forall (A: Type) n (l: list A), list_norepet l -> list_norepet (list_drop n l). |
---|
1083 | Proof. |
---|
1084 | induction n; simpl; intros. auto. |
---|
1085 | inv H. constructor. auto. |
---|
1086 | Qed. |
---|
1087 | |
---|
1088 | Lemma list_map_drop: |
---|
1089 | forall (A B: Type) (f: A -> B) n (l: list A), |
---|
1090 | list_drop n (map f l) = map f (list_drop n l). |
---|
1091 | Proof. |
---|
1092 | induction n; simpl; intros. auto. |
---|
1093 | destruct l; simpl; auto. |
---|
1094 | Qed. |
---|
1095 | |
---|
1096 | (** * Definitions and theorems over boolean types *) |
---|
1097 | |
---|
1098 | Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := |
---|
1099 | if a then true else false. |
---|
1100 | |
---|
1101 | Implicit Arguments proj_sumbool [P Q]. |
---|
1102 | |
---|
1103 | Coercion proj_sumbool: sumbool >-> bool. |
---|
1104 | |
---|
1105 | Lemma proj_sumbool_true: |
---|
1106 | forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P. |
---|
1107 | Proof. |
---|
1108 | intros P Q a. destruct a; simpl. auto. congruence. |
---|
1109 | Qed. |
---|
1110 | |
---|
1111 | Section DECIDABLE_EQUALITY. |
---|
1112 | |
---|
1113 | Variable A: Type. |
---|
1114 | Variable dec_eq: forall (x y: A), {x=y} + {x<>y}. |
---|
1115 | Variable B: Type. |
---|
1116 | |
---|
1117 | Lemma dec_eq_true: |
---|
1118 | forall (x: A) (ifso ifnot: B), |
---|
1119 | (if dec_eq x x then ifso else ifnot) = ifso. |
---|
1120 | Proof. |
---|
1121 | intros. destruct (dec_eq x x). auto. congruence. |
---|
1122 | Qed. |
---|
1123 | |
---|
1124 | Lemma dec_eq_false: |
---|
1125 | forall (x y: A) (ifso ifnot: B), |
---|
1126 | x <> y -> (if dec_eq x y then ifso else ifnot) = ifnot. |
---|
1127 | Proof. |
---|
1128 | intros. destruct (dec_eq x y). congruence. auto. |
---|
1129 | Qed. |
---|
1130 | |
---|
1131 | Lemma dec_eq_sym: |
---|
1132 | forall (x y: A) (ifso ifnot: B), |
---|
1133 | (if dec_eq x y then ifso else ifnot) = |
---|
1134 | (if dec_eq y x then ifso else ifnot). |
---|
1135 | Proof. |
---|
1136 | intros. destruct (dec_eq x y). |
---|
1137 | subst y. rewrite dec_eq_true. auto. |
---|
1138 | rewrite dec_eq_false; auto. |
---|
1139 | Qed. |
---|
1140 | |
---|
1141 | End DECIDABLE_EQUALITY. |
---|
1142 | *) |
---|