source: C-semantics/Coqlib.ma @ 82

Last change on this file since 82 was 24, checked in by campbell, 10 years ago

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

File size: 31.8 KB
Line 
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
20include "binary/Z.ma".
21include "datatypes/sums.ma".
22include "datatypes/list.ma".
23
24include "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
34Axiom extensionality:
35  forall (A B: Type) (f g : A -> B),
36  (forall x, f x = g x) -> f = g.
37
38Axiom proof_irrelevance:
39  forall (P: Prop) (p1 p2: P), p1 = p2.
40
41(** * Useful tactics *)
42
43Ltac inv H := inversion H; clear H; subst.
44
45Ltac predSpec pred predspec x y :=
46  generalize (predspec x y); case (pred x y); intro.
47
48Ltac caseEq name :=
49  generalize (refl_equal name); pattern name at -1 in |- *; case name.
50
51Ltac destructEq name :=
52  generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro.
53
54Ltac decEq :=
55  match goal with
56  | [ |- _ = _ ] => f_equal
57  | [ |- (?X ?A <> ?X ?B) ] =>
58      cut (A <> B); [intro; congruence | try discriminate]
59  end.
60
61Ltac byContradiction :=
62  cut False; [contradiction|idtac].
63
64Ltac omegaContradiction :=
65  cut False; [contradiction|omega].
66
67Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.
68Proof. auto. Qed.
69
70Ltac 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
109Definition peq (x y: positive): {x = y} + {x <> y}.
110Proof.
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.
115Qed.
116
117Lemma peq_true:
118  forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a.
119Proof.
120  intros. case (peq x x); intros.
121  auto.
122  elim n; auto.
123Qed.
124
125Lemma peq_false:
126  forall (A: Type) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
127Proof.
128  intros. case (peq x y); intros.
129  elim H; auto.
130  auto.
131Qed. 
132
133Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y).
134
135Lemma Plt_ne:
136  forall (x y: positive), Plt x y -> x <> y.
137Proof.
138  unfold Plt; intros. red; intro. subst y. omega.
139Qed.
140Hint Resolve Plt_ne: coqlib.
141
142Lemma Plt_trans:
143  forall (x y z: positive), Plt x y -> Plt y z -> Plt x z.
144Proof.
145  unfold Plt; intros; omega.
146Qed.
147
148Remark Psucc_Zsucc:
149  forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x).
150Proof.
151  intros. rewrite Pplus_one_succ_r.
152  reflexivity.
153Qed.
154
155Lemma Plt_succ:
156  forall (x: positive), Plt x (Psucc x).
157Proof.
158  intro. unfold Plt. rewrite Psucc_Zsucc. omega.
159Qed.
160Hint Resolve Plt_succ: coqlib.
161
162Lemma Plt_trans_succ:
163  forall (x y: positive), Plt x y -> Plt x (Psucc y).
164Proof.
165  intros. apply Plt_trans with y. assumption. apply Plt_succ.
166Qed.
167Hint Resolve Plt_succ: coqlib.
168
169Lemma Plt_succ_inv:
170  forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y.
171Proof.
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.
175Qed.
176
177Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}.
178Proof.
179 intros. unfold Plt. apply Z_lt_dec.
180Qed.
181
182Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q).
183
184Lemma Ple_refl: forall (p: positive), Ple p p.
185Proof.
186  unfold Ple; intros; omega.
187Qed.
188
189Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r.
190Proof.
191  unfold Ple; intros; omega.
192Qed.
193
194Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q.
195Proof.
196  unfold Plt, Ple; intros; omega.
197Qed.
198
199Lemma Ple_succ: forall (p: positive), Ple p (Psucc p).
200Proof.
201  intros. apply Plt_Ple. apply Plt_succ.
202Qed.
203
204Lemma Plt_Ple_trans:
205  forall (p q r: positive), Plt p q -> Ple q r -> Plt p r.
206Proof.
207  unfold Plt, Ple; intros; omega.
208Qed.
209
210Lemma Plt_strict: forall p, ~ Plt p p.
211Proof.
212  unfold Plt; intros. omega.
213Qed.
214
215Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib.
216
217(** Peano recursion over positive numbers. *)
218
219Section POSITIVE_ITERATION.
220
221Lemma Plt_wf: well_founded Plt.
222Proof.
223  apply well_founded_lt_compat with nat_of_P.
224  intros. apply nat_of_P_lt_Lt_compare_morphism. exact H.
225Qed.
226
227Variable A: Type.
228Variable v1: A.
229Variable f: positive -> A -> A.
230
231Lemma Ppred_Plt:
232  forall x, x <> xH -> Plt (Ppred x) x.
233Proof.
234  intros. elim (Psucc_pred x); intro. contradiction.
235  set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ.
236Qed.
237
238Let 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
244Definition positive_rec : positive -> A :=
245  Fix Plt_wf (fun _ => A) iter.
246
247Lemma unroll_positive_rec:
248  forall x,
249  positive_rec x = iter x (fun y _ => positive_rec y).
250Proof.
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.
253Qed.
254
255Lemma positive_rec_base:
256  positive_rec 1%positive = v1.
257Proof.
258  rewrite unroll_positive_rec. unfold iter. case (peq 1 1); intro.
259  auto. elim n; auto.
260Qed.
261
262Lemma positive_rec_succ:
263  forall x, positive_rec (Psucc x) = f x (positive_rec x).
264Proof.
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.
269Qed.
270
271Lemma positive_Peano_ind:
272  forall (P: positive -> Prop),
273  P xH ->
274  (forall x, P x -> P (Psucc x)) ->
275  forall x, P x.
276Proof.
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.
284Qed.
285
286End POSITIVE_ITERATION.
287
288(** * Definitions and theorems over the type [Z] *)
289
290Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec.
291
292Lemma zeq_true:
293  forall (A: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a.
294Proof.
295  intros. case (zeq x x); intros.
296  auto.
297  elim n; auto.
298Qed.
299
300Lemma zeq_false:
301  forall (A: Type) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
302Proof.
303  intros. case (zeq x y); intros.
304  elim H; auto.
305  auto.
306Qed. 
307
308Open Scope Z_scope.
309
310Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec.
311
312Lemma zlt_true:
313  forall (A: Type) (x y: Z) (a b: A),
314  x < y -> (if zlt x y then a else b) = a.
315Proof.
316  intros. case (zlt x y); intros.
317  auto.
318  omegaContradiction.
319Qed.
320
321Lemma zlt_false:
322  forall (A: Type) (x y: Z) (a b: A),
323  x >= y -> (if zlt x y then a else b) = b.
324Proof.
325  intros. case (zlt x y); intros.
326  omegaContradiction.
327  auto.
328Qed.
329
330Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec.
331
332Lemma zle_true:
333  forall (A: Type) (x y: Z) (a b: A),
334  x <= y -> (if zle x y then a else b) = a.
335Proof.
336  intros. case (zle x y); intros.
337  auto.
338  omegaContradiction.
339Qed.
340
341Lemma zle_false:
342  forall (A: Type) (x y: Z) (a b: A),
343  x > y -> (if zle x y then a else b) = b.
344Proof.
345  intros. case (zle x y); intros.
346  omegaContradiction.
347  auto.
348Qed.
349*)
350(* * Properties of powers of two. *)
351
352nlemma two_power_nat_O : two_power_nat O = one.
353//; nqed.
354
355nlemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
356//; nqed.
357
358nlemma two_power_nat_two_p:
359  ∀x. Z_two_power_nat x = two_p (Z_of_nat x).
360#x; ncases x;
361##[ //;
362##| nnormalize; #p; nelim p; //; #p' H; nrewrite > (nat_succ_pos …); //;
363##] nqed.
364(*
365Lemma two_p_monotone:
366  forall x y, 0 <= x <= y -> two_p x <= two_p y.
367Proof.
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.
375Qed.
376
377Lemma two_p_monotone_strict:
378  forall x y, 0 <= x < y -> two_p x < two_p y.
379Proof.
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.
383Qed.
384
385Lemma two_p_strict:
386  forall x, x >= 0 -> x < two_p x.
387Proof.
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.
392Qed.
393
394Lemma two_p_strict_2:
395  forall x, x >= 0 -> 2 * x - 1 < two_p x.
396Proof.
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.
402Qed.
403
404(** Properties of [Zmin] and [Zmax] *)
405
406Lemma Zmin_spec:
407  forall x y, Zmin x y = if zlt x y then x else y.
408Proof.
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.
415Qed.
416
417Lemma Zmax_spec:
418  forall x y, Zmax x y = if zlt y x then x else y.
419Proof.
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.
427Qed.
428
429Lemma Zmax_bound_l:
430  forall x y z, x <= y -> x <= Zmax y z.
431Proof.
432  intros. generalize (Zmax1 y z). omega.
433Qed.
434Lemma Zmax_bound_r:
435  forall x y z, x <= z -> x <= Zmax y z.
436Proof.
437  intros. generalize (Zmax2 y z). omega.
438Qed.
439
440(** Properties of Euclidean division and modulus. *)
441
442Lemma Zdiv_small:
443  forall x y, 0 <= x < y -> x / y = 0.
444Proof.
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.
462Qed.
463
464Lemma Zmod_small:
465  forall x y, 0 <= x < y -> x mod y = x.
466Proof.
467  intros. assert (y > 0). omega.
468  generalize (Z_div_mod_eq x y H0).
469  rewrite (Zdiv_small x y H). omega.
470Qed.
471
472Lemma Zmod_unique:
473  forall x y a b,
474  x = a * y + b -> 0 <= b < y -> x mod y = b.
475Proof.
476  intros. subst x. rewrite Zplus_comm.
477  rewrite Z_mod_plus. apply Zmod_small. auto. omega.
478Qed.
479
480Lemma Zdiv_unique:
481  forall x y a b,
482  x = a * y + b -> 0 <= b < y -> x / y = a.
483Proof.
484  intros. subst x. rewrite Zplus_comm.
485  rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega.
486Qed.
487
488Lemma Zdiv_Zdiv:
489  forall a b c,
490  b > 0 -> c > 0 -> (a / b) / c = a / (b * c).
491Proof.
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.
506Qed.
507
508Lemma Zmult_le_compat_l_neg :
509  forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m.
510Proof.
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.
516Qed.
517
518Lemma 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.
523Proof.
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.
537Qed.
538
539Lemma Zdiv_interval_2:
540  forall lo hi a b,
541  lo <= a <= hi -> lo <= 0 -> hi >= 0 -> b > 0 ->
542  lo <= a/b <= hi.
543Proof.
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.
553Qed.
554
555(** Properties of divisibility. *)
556
557Lemma Zdivides_trans:
558  forall x y z, (x | y) -> (y | z) -> (x | z).
559Proof.
560  intros. inv H. inv H0. exists (q0 * q). ring.
561Qed.
562
563Definition Zdivide_dec:
564  forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.
565Proof.
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.
572Defined.
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
578ndefinition align ≝ λn: Z. λamount: Z.
579  ((n + amount - 1) / amount) * amount.
580(*
581Lemma align_le: forall x y, y > 0 -> x <= align x y.
582Proof.
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.
589Qed.
590
591Lemma align_divides: forall x y, y > 0 -> (y | align x y).
592Proof.
593  intros. unfold align. apply Zdivide_factor_l.
594Qed.
595
596(** * Definitions and theorems on the data types [option], [sum] and [list] *)
597
598Set Implicit Arguments.
599*)
600(* * Mapping a function over an option type. *)
601
602ndefinition 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
608Definition 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
616Hint Resolve in_eq in_cons: coqlib.
617
618Lemma 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.
621Proof.
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.
629Qed.
630Hint Resolve nth_error_in: coqlib.
631
632Lemma nth_error_nil:
633  forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.
634Proof.
635  induction idx; simpl; intros; reflexivity.
636Qed.
637Hint Resolve nth_error_nil: coqlib.
638
639(** Compute the length of a list, with result in [Z]. *)
640
641Fixpoint 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
647Remark 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).
650Proof.
651  induction l; intros; simpl.
652  omega.
653  replace (n - m) with (Zsucc n - Zsucc m) by omega. auto.
654Qed.
655
656Definition list_length_z (A: Type) (l: list A) : Z :=
657  list_length_z_aux l 0.
658
659Lemma list_length_z_cons:
660  forall (A: Type) (hd: A) (tl: list A),
661  list_length_z (hd :: tl) = list_length_z tl + 1.
662Proof.
663  intros. unfold list_length_z. simpl.
664  rewrite (list_length_z_aux_shift tl 1 0). omega.
665Qed.
666
667Lemma list_length_z_pos:
668  forall (A: Type) (l: list A),
669  list_length_z l >= 0.
670Proof.
671  induction l; simpl. unfold list_length_z; simpl. omega.
672  rewrite list_length_z_cons. omega.
673Qed.
674
675Lemma 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.
678Proof.
679  induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence.
680Qed.
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
685Fixpoint 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
691Lemma list_nth_z_in:
692  forall (A: Type) (l: list A) n x,
693  list_nth_z l n = Some x -> In x l.
694Proof.
695  induction l; simpl; intros.
696  congruence.
697  destruct (zeq n 0). left; congruence. right; eauto.
698Qed.
699
700Lemma 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).
703Proof.
704  induction l; simpl; intros.
705  auto.
706  destruct (zeq n 0). auto. eauto.
707Qed.
708
709Lemma 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.
712Proof.
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.
718Qed.
719
720(** Properties of [List.incl] (list inclusion). *)
721
722Lemma incl_cons_inv:
723  forall (A: Type) (a: A) (b c: list A),
724  incl (a :: b) c -> incl b c.
725Proof.
726  unfold incl; intros. apply H. apply in_cons. auto.
727Qed.
728Hint Resolve incl_cons_inv: coqlib.
729
730Lemma incl_app_inv_l:
731  forall (A: Type) (l1 l2 m: list A),
732  incl (l1 ++ l2) m -> incl l1 m.
733Proof.
734  unfold incl; intros. apply H. apply in_or_app. left; assumption.
735Qed.
736
737Lemma incl_app_inv_r:
738  forall (A: Type) (l1 l2 m: list A),
739  incl (l1 ++ l2) m -> incl l2 m.
740Proof.
741  unfold incl; intros. apply H. apply in_or_app. right; assumption.
742Qed.
743
744Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
745
746Lemma incl_same_head:
747  forall (A: Type) (x: A) (l1 l2: list A),
748  incl l1 l2 -> incl (x::l1) (x::l2).
749Proof.
750  intros; red; simpl; intros. intuition.
751Qed.
752
753(** Properties of [List.map] (mapping a function over a list). *)
754
755Lemma 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.
759Proof.
760  induction l; simpl; intros.
761  reflexivity.
762  rewrite <- H. rewrite IHl. reflexivity.
763  intros. apply H. tauto.
764  tauto.
765Qed.
766
767Lemma 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.
770Proof.
771  induction l; simpl. reflexivity. rewrite IHl; reflexivity.
772Qed.
773
774Lemma list_map_identity:
775  forall (A: Type) (l: list A),
776  List.map (fun (x:A) => x) l = l.
777Proof.
778  induction l; simpl; congruence.
779Qed.
780
781Lemma 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).
784Proof.
785  induction l; simpl; intros.
786  repeat rewrite nth_error_nil. reflexivity.
787  destruct n; simpl. reflexivity. auto.
788Qed.
789
790Lemma list_length_map:
791  forall (A B: Type) (f: A -> B) (l: list A),
792  List.length (List.map f l) = List.length l.
793Proof.
794  induction l; simpl; congruence.
795Qed.
796*)
797nlemma list_in_map_inv:
798  ∀A,B: Type. ∀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(*
812Lemma 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.
815Proof.
816  induction l1; simpl; intros.
817  auto. rewrite IHl1. auto.
818Qed.
819
820(** Properties of list membership. *)
821
822Lemma in_cns:
823  forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
824Proof.
825  intros. simpl. tauto.
826Qed.
827
828Lemma in_app:
829  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
830Proof.
831  intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
832Qed.
833
834Lemma 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).
837Proof.
838  intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto.
839Qed.
840*)
841(* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements
842  in common. *)
843
844ndefinition list_disjoint : ∀A:Type. 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
848nlemma list_disjoint_cons_left:
849  ∀A: Type. ∀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/;
853nqed.
854
855nlemma 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/;
860nqed.
861
862nlemma 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;
866napply nmk; #H2;
867napply (absurd ?? (H … H1 H2)); //;
868nqed.
869
870nlemma 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;
874nwhd in ⊢ (% → %);
875#H;#x;#y;#H1;#H2; napply sym_neq; /2/;
876nqed.
877(*
878Lemma list_disjoint_dec:
879  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
880  {list_disjoint l1 l2} + {~list_disjoint l1 l2}.
881Proof.
882  induction l1; intros.
883  left; red; intros. elim H.
884  case (In_dec eqA_dec a l2); intro.
885  right; red; intro. apply (H a a); auto with coqlib.
886  case (IHl1 l2); intro.
887  left; red; intros. elim H; intro.
888    red; intro; subst a y. contradiction.
889    apply l; auto.
890  right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto.
891Defined.
892
893(** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *)
894
895Definition list_equiv (A : Type) (l1 l2: list A) : Prop :=
896  forall x, In x l1 <-> In x l2.
897*)
898(* * [list_norepet l] holds iff the list [l] contains no repetitions,
899  i.e. no element occurs twice. *)
900
901ninductive list_norepet (A: Type) : list A → Prop ≝
902  | list_norepet_nil:
903      list_norepet A (nil A)
904  | list_norepet_cons:
905      ∀hd,tl.
906      ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl).
907(*
908Lemma list_norepet_dec:
909  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
910  {list_norepet l} + {~list_norepet l}.
911Proof.
912  induction l.
913  left; constructor.
914  destruct IHl.
915  case (In_dec eqA_dec a l); intro.
916  right. red; intro. inversion H. contradiction.
917  left. constructor; auto.
918  right. red; intro. inversion H. contradiction.
919Defined.
920
921Lemma list_map_norepet:
922  forall (A B: Type) (f: A -> B) (l: list A),
923  list_norepet l ->
924  (forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
925  list_norepet (List.map f l).
926Proof.
927  induction 1; simpl; intros.
928  constructor.
929  constructor.
930  red; intro. generalize (list_in_map_inv f _ _ H2).
931  intros [x [EQ IN]]. generalize EQ. change (f hd <> f x).
932  apply H1. tauto. tauto.
933  red; intro; subst x. contradiction.
934  apply IHlist_norepet. intros. apply H1. tauto. tauto. auto.
935Qed.
936
937Remark list_norepet_append_commut:
938  forall (A: Type) (a b: list A),
939  list_norepet (a ++ b) -> list_norepet (b ++ a).
940Proof.
941  intro A.
942  assert (forall (x: A) (b: list A) (a: list A),
943           list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) ->
944           list_norepet (a ++ x :: b)).
945    induction a; simpl; intros.
946    constructor; auto.
947    inversion H. constructor. red; intro.
948    elim (in_app_or _ _ _ H6); intro.
949    elim H4. apply in_or_app. tauto.
950    elim H7; intro. subst a. elim H0. left. auto.
951    elim H4. apply in_or_app. tauto.
952    auto.
953  induction a; simpl; intros.
954  rewrite <- app_nil_end. auto.
955  inversion H0. apply H. auto.
956  red; intro; elim H3. apply in_or_app. tauto.
957  red; intro; elim H3. apply in_or_app. tauto.
958Qed.
959
960Lemma list_norepet_app:
961  forall (A: Type) (l1 l2: list A),
962  list_norepet (l1 ++ l2) <->
963  list_norepet l1 /\ list_norepet l2 /\ list_disjoint l1 l2.
964Proof.
965  induction l1; simpl; intros; split; intros.
966  intuition. constructor. red;simpl;auto.
967  tauto.
968  inversion H; subst. rewrite IHl1 in H3. rewrite in_app in H2.
969  intuition.
970  constructor; auto. red; intros. elim H2; intro. congruence. auto.
971  destruct H as [B [C D]]. inversion B; subst.
972  constructor. rewrite in_app. intuition. elim (D a a); auto. apply in_eq.
973  rewrite IHl1. intuition. red; intros. apply D; auto. apply in_cons; auto.
974Qed.
975
976Lemma list_norepet_append:
977  forall (A: Type) (l1 l2: list A),
978  list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
979  list_norepet (l1 ++ l2).
980Proof.
981  generalize list_norepet_app; firstorder.
982Qed.
983
984Lemma list_norepet_append_right:
985  forall (A: Type) (l1 l2: list A),
986  list_norepet (l1 ++ l2) -> list_norepet l2.
987Proof.
988  generalize list_norepet_app; firstorder.
989Qed.
990
991Lemma list_norepet_append_left:
992  forall (A: Type) (l1 l2: list A),
993  list_norepet (l1 ++ l2) -> list_norepet l1.
994Proof.
995  generalize list_norepet_app; firstorder.
996Qed.
997
998(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
999
1000Inductive is_tail (A: Type): list A -> list A -> Prop :=
1001  | is_tail_refl:
1002      forall c, is_tail c c
1003  | is_tail_cons:
1004      forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).
1005
1006Lemma is_tail_in:
1007  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
1008Proof.
1009  induction c2; simpl; intros.
1010  inversion H.
1011  inversion H. tauto. right; auto.
1012Qed.
1013
1014Lemma is_tail_cons_left:
1015  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
1016Proof.
1017  induction c2; intros; inversion H.
1018  constructor. constructor. constructor. auto.
1019Qed.
1020
1021Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
1022
1023Lemma is_tail_incl:
1024  forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
1025Proof.
1026  induction 1; eauto with coqlib.
1027Qed.
1028
1029Lemma is_tail_trans:
1030  forall (A: Type) (l1 l2: list A),
1031  is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3.
1032Proof.
1033  induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
1034Qed.
1035
1036(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and
1037  [P xi yi] holds for all [i]. *)
1038
1039Section FORALL2.
1040
1041Variable A: Type.
1042Variable B: Type.
1043Variable P: A -> B -> Prop.
1044
1045Inductive list_forall2: list A -> list B -> Prop :=
1046  | list_forall2_nil:
1047      list_forall2 nil nil
1048  | list_forall2_cons:
1049      forall a1 al b1 bl,
1050      P a1 b1 ->
1051      list_forall2 al bl ->
1052      list_forall2 (a1 :: al) (b1 :: bl).
1053
1054End FORALL2.
1055
1056Lemma list_forall2_imply:
1057  forall (A B: Type) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
1058  list_forall2 P1 l1 l2 ->
1059  forall (P2: A -> B -> Prop),
1060  (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) ->
1061  list_forall2 P2 l1 l2.
1062Proof.
1063  induction 1; intros.
1064  constructor.
1065  constructor. auto with coqlib. apply IHlist_forall2; auto.
1066  intros. auto with coqlib.
1067Qed.
1068
1069(** Dropping the first N elements of a list. *)
1070
1071Fixpoint list_drop (A: Type) (n: nat) (x: list A) {struct n} : list A :=
1072  match n with
1073  | O => x
1074  | S n' => match x with nil => nil | hd :: tl => list_drop n' tl end
1075  end.
1076
1077Lemma list_drop_incl:
1078  forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l.
1079Proof.
1080  induction n; simpl; intros. auto.
1081  destruct l; auto with coqlib.
1082Qed.
1083
1084Lemma list_drop_norepet:
1085  forall (A: Type) n (l: list A), list_norepet l -> list_norepet (list_drop n l).
1086Proof.
1087  induction n; simpl; intros. auto.
1088  inv H. constructor. auto.
1089Qed.
1090
1091Lemma list_map_drop:
1092  forall (A B: Type) (f: A -> B) n (l: list A),
1093  list_drop n (map f l) = map f (list_drop n l).
1094Proof.
1095  induction n; simpl; intros. auto.
1096  destruct l; simpl; auto.
1097Qed.
1098
1099(** * Definitions and theorems over boolean types *)
1100
1101Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
1102  if a then true else false.
1103
1104Implicit Arguments proj_sumbool [P Q].
1105
1106Coercion proj_sumbool: sumbool >-> bool.
1107
1108Lemma proj_sumbool_true:
1109  forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P.
1110Proof.
1111  intros P Q a. destruct a; simpl. auto. congruence.
1112Qed.
1113
1114Section DECIDABLE_EQUALITY.
1115
1116Variable A: Type.
1117Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.
1118Variable B: Type.
1119
1120Lemma dec_eq_true:
1121  forall (x: A) (ifso ifnot: B),
1122  (if dec_eq x x then ifso else ifnot) = ifso.
1123Proof.
1124  intros. destruct (dec_eq x x). auto. congruence.
1125Qed.
1126
1127Lemma dec_eq_false:
1128  forall (x y: A) (ifso ifnot: B),
1129  x <> y -> (if dec_eq x y then ifso else ifnot) = ifnot.
1130Proof.
1131  intros. destruct (dec_eq x y). congruence. auto.
1132Qed.
1133
1134Lemma dec_eq_sym:
1135  forall (x y: A) (ifso ifnot: B),
1136  (if dec_eq x y then ifso else ifnot) =
1137  (if dec_eq y x then ifso else ifnot).
1138Proof.
1139  intros. destruct (dec_eq x y).
1140  subst y. rewrite dec_eq_true. auto.
1141  rewrite dec_eq_false; auto.
1142Qed.
1143
1144End DECIDABLE_EQUALITY.
1145*)
Note: See TracBrowser for help on using the repository browser.