source: C-semantics/Coqlib.ma @ 10

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

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File size: 31.7 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
797Lemma list_in_map_inv:
798  forall (A B: Type) (f: A -> B) (l: list A) (y: B),
799  In y (List.map f l) -> exists x:A, y = f x /\ In x l.
800Proof.
801  induction l; simpl; intros.
802  contradiction.
803  elim H; intro.
804  exists a; intuition auto.
805  generalize (IHl y H0). intros [x [EQ IN]].
806  exists x; tauto.
807Qed.
808
809Lemma list_append_map:
810  forall (A B: Type) (f: A -> B) (l1 l2: list A),
811  List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.
812Proof.
813  induction l1; simpl; intros.
814  auto. rewrite IHl1. auto.
815Qed.
816
817(** Properties of list membership. *)
818
819Lemma in_cns:
820  forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
821Proof.
822  intros. simpl. tauto.
823Qed.
824
825Lemma in_app:
826  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
827Proof.
828  intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
829Qed.
830
831Lemma list_in_insert:
832  forall (A: Type) (x: A) (l1 l2: list A) (y: A),
833  In x (l1 ++ l2) -> In x (l1 ++ y :: l2).
834Proof.
835  intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto.
836Qed.
837*)
838(* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements
839  in common. *)
840
841ndefinition list_disjoint : ∀A:Type. list A → list A → Prop ≝
842  λA,l1,l2.
843  ∀x,y: A. in_list A x l1 → in_list A y l2 → x ≠ y.
844
845nlemma list_disjoint_cons_left:
846  ∀A: Type. ∀a: A. ∀l1,l2: list A.
847  list_disjoint A (a :: l1) l2 → list_disjoint A l1 l2.
848#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
849#x;#y;#in1;#in2; napply H; /2/;
850nqed.
851
852nlemma list_disjoint_cons_right:
853  ∀A: Type. ∀a: A. ∀l1,l2: list A.
854  list_disjoint A l1 (a :: l2) → list_disjoint A l1 l2.
855#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
856#x;#y;#in1;#in2; napply H; /2/;
857nqed.
858
859nlemma list_disjoint_notin:
860  ∀A: Type. ∀l1,l2: list A. ∀a: A.
861  list_disjoint A l1 l2 → in_list A a l1 → ¬(in_list A a l2).
862#A;#l1;#l2;#a;nwhd in ⊢ (% → ?); #H; #H1;
863napply nmk; #H2;
864napply (absurd ?? (H … H1 H2)); //;
865nqed.
866
867nlemma list_disjoint_sym:
868  ∀A: Type. ∀l1,l2: list A.
869  list_disjoint A l1 l2 → list_disjoint A l2 l1.
870#A;#l1;#l2;
871nwhd in ⊢ (% → %);
872#H;#x;#y;#H1;#H2; napply sym_neq; /2/;
873nqed.
874(*
875Lemma 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}.
878Proof.
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.
888Defined.
889
890(** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *)
891
892Definition 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
898ninductive list_norepet (A: Type) : 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(*
905Lemma 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}.
908Proof.
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.
916Defined.
917
918Lemma 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).
923Proof.
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.
932Qed.
933
934Remark list_norepet_append_commut:
935  forall (A: Type) (a b: list A),
936  list_norepet (a ++ b) -> list_norepet (b ++ a).
937Proof.
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.
955Qed.
956
957Lemma 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.
961Proof.
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.
971Qed.
972
973Lemma 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).
977Proof.
978  generalize list_norepet_app; firstorder.
979Qed.
980
981Lemma list_norepet_append_right:
982  forall (A: Type) (l1 l2: list A),
983  list_norepet (l1 ++ l2) -> list_norepet l2.
984Proof.
985  generalize list_norepet_app; firstorder.
986Qed.
987
988Lemma list_norepet_append_left:
989  forall (A: Type) (l1 l2: list A),
990  list_norepet (l1 ++ l2) -> list_norepet l1.
991Proof.
992  generalize list_norepet_app; firstorder.
993Qed.
994
995(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
996
997Inductive 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
1003Lemma is_tail_in:
1004  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
1005Proof.
1006  induction c2; simpl; intros.
1007  inversion H.
1008  inversion H. tauto. right; auto.
1009Qed.
1010
1011Lemma is_tail_cons_left:
1012  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
1013Proof.
1014  induction c2; intros; inversion H.
1015  constructor. constructor. constructor. auto.
1016Qed.
1017
1018Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
1019
1020Lemma is_tail_incl:
1021  forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
1022Proof.
1023  induction 1; eauto with coqlib.
1024Qed.
1025
1026Lemma 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.
1029Proof.
1030  induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
1031Qed.
1032
1033(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and
1034  [P xi yi] holds for all [i]. *)
1035
1036Section FORALL2.
1037
1038Variable A: Type.
1039Variable B: Type.
1040Variable P: A -> B -> Prop.
1041
1042Inductive 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
1051End FORALL2.
1052
1053Lemma 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.
1059Proof.
1060  induction 1; intros.
1061  constructor.
1062  constructor. auto with coqlib. apply IHlist_forall2; auto.
1063  intros. auto with coqlib.
1064Qed.
1065
1066(** Dropping the first N elements of a list. *)
1067
1068Fixpoint 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
1074Lemma list_drop_incl:
1075  forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l.
1076Proof.
1077  induction n; simpl; intros. auto.
1078  destruct l; auto with coqlib.
1079Qed.
1080
1081Lemma list_drop_norepet:
1082  forall (A: Type) n (l: list A), list_norepet l -> list_norepet (list_drop n l).
1083Proof.
1084  induction n; simpl; intros. auto.
1085  inv H. constructor. auto.
1086Qed.
1087
1088Lemma 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).
1091Proof.
1092  induction n; simpl; intros. auto.
1093  destruct l; simpl; auto.
1094Qed.
1095
1096(** * Definitions and theorems over boolean types *)
1097
1098Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
1099  if a then true else false.
1100
1101Implicit Arguments proj_sumbool [P Q].
1102
1103Coercion proj_sumbool: sumbool >-> bool.
1104
1105Lemma proj_sumbool_true:
1106  forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P.
1107Proof.
1108  intros P Q a. destruct a; simpl. auto. congruence.
1109Qed.
1110
1111Section DECIDABLE_EQUALITY.
1112
1113Variable A: Type.
1114Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.
1115Variable B: Type.
1116
1117Lemma dec_eq_true:
1118  forall (x: A) (ifso ifnot: B),
1119  (if dec_eq x x then ifso else ifnot) = ifso.
1120Proof.
1121  intros. destruct (dec_eq x x). auto. congruence.
1122Qed.
1123
1124Lemma dec_eq_false:
1125  forall (x y: A) (ifso ifnot: B),
1126  x <> y -> (if dec_eq x y then ifso else ifnot) = ifnot.
1127Proof.
1128  intros. destruct (dec_eq x y). congruence. auto.
1129Qed.
1130
1131Lemma 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).
1135Proof.
1136  intros. destruct (dec_eq x y).
1137  subst y. rewrite dec_eq_true. auto.
1138  rewrite dec_eq_false; auto.
1139Qed.
1140
1141End DECIDABLE_EQUALITY.
1142*)
Note: See TracBrowser for help on using the repository browser.