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