source: src/utilities/Coqlib.ma @ 753

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

Merge the two AST files together (although some definitions still need to be
harmonised).

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 "basics/types.ma".
21include "basics/list.ma".
22
23include "ASM/Util.ma".
24
25(*
26(** * Logical axioms *)
27
28(** We use two logical axioms that are not provable in Coq but consistent
29  with the logic: function extensionality and proof irrelevance.
30  These are used in the memory model to show that two memory states
31  that have identical contents are equal. *)
32
33Axiom extensionality:
34  forall (A B: Type) (f g : A -> B),
35  (forall x, f x = g x) -> f = g.
36
37Axiom proof_irrelevance:
38  forall (P: Prop) (p1 p2: P), p1 = p2.
39
40(** * Useful tactics *)
41
42Ltac inv H := inversion H; clear H; subst.
43
44Ltac predSpec pred predspec x y :=
45  generalize (predspec x y); case (pred x y); intro.
46
47Ltac caseEq name :=
48  generalize (refl_equal name); pattern name at -1 in |- *; case name.
49
50Ltac destructEq name :=
51  generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro.
52
53Ltac decEq :=
54  match goal with
55  | [ |- _ = _ ] => f_equal
56  | [ |- (?X ?A <> ?X ?B) ] =>
57      cut (A <> B); [intro; congruence | try discriminate]
58  end.
59
60Ltac byContradiction :=
61  cut False; [contradiction|idtac].
62
63Ltac omegaContradiction :=
64  cut False; [contradiction|omega].
65
66Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.
67Proof. auto. Qed.
68
69Ltac exploit x :=
70    refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
71 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
72 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
73 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
74 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
75 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
76 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
77 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
78 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
79 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
80 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
81 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
82 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
83 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
84 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
85 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
86 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
87 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
88 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
89 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
90 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
91 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
92 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
93 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)
94 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)
95 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)
96 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)
97 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)
98 || refine (modusponens _ _ (x _ _ _ _ _ _ _) _)
99 || refine (modusponens _ _ (x _ _ _ _ _ _) _)
100 || refine (modusponens _ _ (x _ _ _ _ _) _)
101 || refine (modusponens _ _ (x _ _ _ _) _)
102 || refine (modusponens _ _ (x _ _ _) _)
103 || refine (modusponens _ _ (x _ _) _)
104 || refine (modusponens _ _ (x _) _).
105
106(** * Definitions and theorems over the type [positive] *)
107
108Definition peq (x y: positive): {x = y} + {x <> y}.
109Proof.
110  intros. caseEq (Pcompare x y Eq).
111  intro. left. apply Pcompare_Eq_eq; auto.
112  intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
113  intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
114Qed.
115
116Lemma peq_true:
117  forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a.
118Proof.
119  intros. case (peq x x); intros.
120  auto.
121  elim n; auto.
122Qed.
123
124Lemma peq_false:
125  forall (A: Type) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.
126Proof.
127  intros. case (peq x y); intros.
128  elim H; auto.
129  auto.
130Qed. 
131
132Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y).
133
134Lemma Plt_ne:
135  forall (x y: positive), Plt x y -> x <> y.
136Proof.
137  unfold Plt; intros. red; intro. subst y. omega.
138Qed.
139Hint Resolve Plt_ne: coqlib.
140
141Lemma Plt_trans:
142  forall (x y z: positive), Plt x y -> Plt y z -> Plt x z.
143Proof.
144  unfold Plt; intros; omega.
145Qed.
146
147Remark Psucc_Zsucc:
148  forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x).
149Proof.
150  intros. rewrite Pplus_one_succ_r.
151  reflexivity.
152Qed.
153
154Lemma Plt_succ:
155  forall (x: positive), Plt x (Psucc x).
156Proof.
157  intro. unfold Plt. rewrite Psucc_Zsucc. omega.
158Qed.
159Hint Resolve Plt_succ: coqlib.
160
161Lemma Plt_trans_succ:
162  forall (x y: positive), Plt x y -> Plt x (Psucc y).
163Proof.
164  intros. apply Plt_trans with y. assumption. apply Plt_succ.
165Qed.
166Hint Resolve Plt_succ: coqlib.
167
168Lemma Plt_succ_inv:
169  forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y.
170Proof.
171  intros x y. unfold Plt. rewrite Psucc_Zsucc.
172  intro. assert (A: (Zpos x < Zpos y)%Z \/ Zpos x = Zpos y). omega.
173  elim A; intro. left; auto. right; injection H0; auto.
174Qed.
175
176Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}.
177Proof.
178 intros. unfold Plt. apply Z_lt_dec.
179Qed.
180
181Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q).
182
183Lemma Ple_refl: forall (p: positive), Ple p p.
184Proof.
185  unfold Ple; intros; omega.
186Qed.
187
188Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r.
189Proof.
190  unfold Ple; intros; omega.
191Qed.
192
193Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q.
194Proof.
195  unfold Plt, Ple; intros; omega.
196Qed.
197
198Lemma Ple_succ: forall (p: positive), Ple p (Psucc p).
199Proof.
200  intros. apply Plt_Ple. apply Plt_succ.
201Qed.
202
203Lemma Plt_Ple_trans:
204  forall (p q r: positive), Plt p q -> Ple q r -> Plt p r.
205Proof.
206  unfold Plt, Ple; intros; omega.
207Qed.
208
209Lemma Plt_strict: forall p, ~ Plt p p.
210Proof.
211  unfold Plt; intros. omega.
212Qed.
213
214Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib.
215
216(** Peano recursion over positive numbers. *)
217
218Section POSITIVE_ITERATION.
219
220Lemma Plt_wf: well_founded Plt.
221Proof.
222  apply well_founded_lt_compat with nat_of_P.
223  intros. apply nat_of_P_lt_Lt_compare_morphism. exact H.
224Qed.
225
226Variable A: Type.
227Variable v1: A.
228Variable f: positive -> A -> A.
229
230Lemma Ppred_Plt:
231  forall x, x <> xH -> Plt (Ppred x) x.
232Proof.
233  intros. elim (Psucc_pred x); intro. contradiction.
234  set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ.
235Qed.
236
237Let iter (x: positive) (P: forall y, Plt y x -> A) : A :=
238  match peq x xH with
239  | left EQ => v1
240  | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ))
241  end.
242
243Definition positive_rec : positive -> A :=
244  Fix Plt_wf (fun _ => A) iter.
245
246Lemma unroll_positive_rec:
247  forall x,
248  positive_rec x = iter x (fun y _ => positive_rec y).
249Proof.
250  unfold positive_rec. apply (Fix_eq Plt_wf (fun _ => A) iter).
251  intros. unfold iter. case (peq x 1); intro. auto. decEq. apply H.
252Qed.
253
254Lemma positive_rec_base:
255  positive_rec 1%positive = v1.
256Proof.
257  rewrite unroll_positive_rec. unfold iter. case (peq 1 1); intro.
258  auto. elim n; auto.
259Qed.
260
261Lemma positive_rec_succ:
262  forall x, positive_rec (Psucc x) = f x (positive_rec x).
263Proof.
264  intro. rewrite unroll_positive_rec. unfold iter.
265  case (peq (Psucc x) 1); intro.
266  destruct x; simpl in e; discriminate.
267  rewrite Ppred_succ. auto.
268Qed.
269
270Lemma positive_Peano_ind:
271  forall (P: positive -> Prop),
272  P xH ->
273  (forall x, P x -> P (Psucc x)) ->
274  forall x, P x.
275Proof.
276  intros.
277  apply (well_founded_ind Plt_wf P).
278  intros.
279  case (peq x0 xH); intro.
280  subst x0; auto.
281  elim (Psucc_pred x0); intro. contradiction. rewrite <- H2.
282  apply H0. apply H1. apply Ppred_Plt. auto.
283Qed.
284
285End POSITIVE_ITERATION.
286
287(** * Definitions and theorems over the type [Z] *)
288
289Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec.
290
291Lemma zeq_true:
292  forall (A: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a.
293Proof.
294  intros. case (zeq x x); intros.
295  auto.
296  elim n; auto.
297Qed.
298
299Lemma zeq_false:
300  forall (A: Type) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.
301Proof.
302  intros. case (zeq x y); intros.
303  elim H; auto.
304  auto.
305Qed. 
306
307Open Scope Z_scope.
308
309Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec.
310
311Lemma zlt_true:
312  forall (A: Type) (x y: Z) (a b: A),
313  x < y -> (if zlt x y then a else b) = a.
314Proof.
315  intros. case (zlt x y); intros.
316  auto.
317  omegaContradiction.
318Qed.
319
320Lemma zlt_false:
321  forall (A: Type) (x y: Z) (a b: A),
322  x >= y -> (if zlt x y then a else b) = b.
323Proof.
324  intros. case (zlt x y); intros.
325  omegaContradiction.
326  auto.
327Qed.
328
329Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec.
330
331Lemma zle_true:
332  forall (A: Type) (x y: Z) (a b: A),
333  x <= y -> (if zle x y then a else b) = a.
334Proof.
335  intros. case (zle x y); intros.
336  auto.
337  omegaContradiction.
338Qed.
339
340Lemma zle_false:
341  forall (A: Type) (x y: Z) (a b: A),
342  x > y -> (if zle x y then a else b) = b.
343Proof.
344  intros. case (zle x y); intros.
345  omegaContradiction.
346  auto.
347Qed.
348*)
349(* * Properties of powers of two. *)
350(*
351lemma two_power_nat_O : two_power_nat O = one.
352// qed.
353
354lemma two_power_nat_pos : ∀n:nat. Z_two_power_nat n > 0.
355// qed.
356
357lemma two_power_nat_two_p:
358  ∀x. Z_two_power_nat x = two_p (Z_of_nat x).
359#x cases x
360[ //
361| normalize #p elim p // #p' #H >(nat_succ_pos …) //
362] qed.*)
363(*
364Lemma two_p_monotone:
365  forall x y, 0 <= x <= y -> two_p x <= two_p y.
366Proof.
367  intros.
368  replace (two_p x) with (two_p x * 1) by omega.
369  replace y with (x + (y - x)) by omega.
370  rewrite two_p_is_exp; try omega.
371  apply Zmult_le_compat_l.
372  assert (two_p (y - x) > 0). apply two_p_gt_ZERO. omega. omega.
373  assert (two_p x > 0). apply two_p_gt_ZERO. omega. omega.
374Qed.
375
376Lemma two_p_monotone_strict:
377  forall x y, 0 <= x < y -> two_p x < two_p y.
378Proof.
379  intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; omega.
380  assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. omega.
381  replace y with (Zsucc (y - 1)) by omega. rewrite two_p_S. omega. omega.
382Qed.
383
384Lemma two_p_strict:
385  forall x, x >= 0 -> x < two_p x.
386Proof.
387  intros x0 GT. pattern x0. apply natlike_ind.
388  simpl. omega.
389  intros. rewrite two_p_S; auto. generalize (two_p_gt_ZERO x H). omega.
390  omega.
391Qed.
392
393Lemma two_p_strict_2:
394  forall x, x >= 0 -> 2 * x - 1 < two_p x.
395Proof.
396  intros. assert (x = 0 \/ x - 1 >= 0) by omega. destruct H0.
397  subst. vm_compute. auto.
398  replace (two_p x) with (2 * two_p (x - 1)).
399  generalize (two_p_strict _ H0). omega.
400  rewrite <- two_p_S. decEq. omega. omega.
401Qed.
402
403(** Properties of [Zmin] and [Zmax] *)
404
405Lemma Zmin_spec:
406  forall x y, Zmin x y = if zlt x y then x else y.
407Proof.
408  intros. case (zlt x y); unfold Zlt, Zge; intros.
409  unfold Zmin. rewrite z. auto.
410  unfold Zmin. caseEq (x ?= y); intro.
411  apply Zcompare_Eq_eq. auto.
412  contradiction.
413  reflexivity.
414Qed.
415
416Lemma Zmax_spec:
417  forall x y, Zmax x y = if zlt y x then x else y.
418Proof.
419  intros. case (zlt y x); unfold Zlt, Zge; intros.
420  unfold Zmax. rewrite <- (Zcompare_antisym y x).
421  rewrite z. simpl. auto.
422  unfold Zmax. rewrite <- (Zcompare_antisym y x).
423  caseEq (y ?= x); intro; simpl.
424  symmetry. apply Zcompare_Eq_eq. auto.
425  contradiction. reflexivity.
426Qed.
427
428Lemma Zmax_bound_l:
429  forall x y z, x <= y -> x <= Zmax y z.
430Proof.
431  intros. generalize (Zmax1 y z). omega.
432Qed.
433Lemma Zmax_bound_r:
434  forall x y z, x <= z -> x <= Zmax y z.
435Proof.
436  intros. generalize (Zmax2 y z). omega.
437Qed.
438
439(** Properties of Euclidean division and modulus. *)
440
441Lemma Zdiv_small:
442  forall x y, 0 <= x < y -> x / y = 0.
443Proof.
444  intros. assert (y > 0). omega.
445  assert (forall a b,
446    0 <= a < y ->
447    0 <= y * b + a < y ->
448    b = 0).
449  intros.
450  assert (b = 0 \/ b > 0 \/ (-b) > 0). omega.
451  elim H3; intro.
452  auto.
453  elim H4; intro.
454  assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega.
455  omegaContradiction.
456  assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega.
457  rewrite <- Zopp_mult_distr_r in H6. omegaContradiction.
458  apply H1 with (x mod y).
459  apply Z_mod_lt. auto.
460  rewrite <- Z_div_mod_eq. auto. auto.
461Qed.
462
463Lemma Zmod_small:
464  forall x y, 0 <= x < y -> x mod y = x.
465Proof.
466  intros. assert (y > 0). omega.
467  generalize (Z_div_mod_eq x y H0).
468  rewrite (Zdiv_small x y H). omega.
469Qed.
470
471Lemma Zmod_unique:
472  forall x y a b,
473  x = a * y + b -> 0 <= b < y -> x mod y = b.
474Proof.
475  intros. subst x. rewrite Zplus_comm.
476  rewrite Z_mod_plus. apply Zmod_small. auto. omega.
477Qed.
478
479Lemma Zdiv_unique:
480  forall x y a b,
481  x = a * y + b -> 0 <= b < y -> x / y = a.
482Proof.
483  intros. subst x. rewrite Zplus_comm.
484  rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega.
485Qed.
486
487Lemma Zdiv_Zdiv:
488  forall a b c,
489  b > 0 -> c > 0 -> (a / b) / c = a / (b * c).
490Proof.
491  intros.
492  generalize (Z_div_mod_eq a b H). generalize (Z_mod_lt a b H). intros.
493  generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros.
494  set (q1 := a / b) in *. set (r1 := a mod b) in *.
495  set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *.
496  symmetry. apply Zdiv_unique with (r2 * b + r1).
497  rewrite H2. rewrite H4. ring.
498  split.
499  assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega.
500  assert ((r2 + 1) * b <= c * b).
501  apply Zmult_le_compat_r. omega. omega.
502  replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring.
503  replace (c * b) with (b * c) in H5 by ring.
504  omega.
505Qed.
506
507Lemma Zmult_le_compat_l_neg :
508  forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m.
509Proof.
510  intros.
511  assert ((-p) * n >= (-p) * m). apply Zmult_ge_compat_l. auto. omega.
512  replace (p * n) with (- ((-p) * n)) by ring.
513  replace (p * m) with (- ((-p) * m)) by ring.
514  omega.
515Qed.
516
517Lemma Zdiv_interval_1:
518  forall lo hi a b,
519  lo <= 0 -> hi > 0 -> b > 0 ->
520  lo * b <= a < hi * b ->
521  lo <= a/b < hi.
522Proof.
523  intros.
524  generalize (Z_div_mod_eq a b H1). generalize (Z_mod_lt a b H1). intros.
525  set (q := a/b) in *. set (r := a mod b) in *.
526  split.
527  assert (lo < (q + 1)).
528  apply Zmult_lt_reg_r with b. omega. 
529  apply Zle_lt_trans with a. omega.
530  replace ((q + 1) * b) with (b * q + b) by ring.
531  omega.
532  omega.
533  apply Zmult_lt_reg_r with b. omega.
534  replace (q * b) with (b * q) by ring.
535  omega.
536Qed.
537
538Lemma Zdiv_interval_2:
539  forall lo hi a b,
540  lo <= a <= hi -> lo <= 0 -> hi >= 0 -> b > 0 ->
541  lo <= a/b <= hi.
542Proof.
543  intros.
544  assert (lo <= a / b < hi+1).
545  apply Zdiv_interval_1. omega. omega. auto.
546  assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega.
547  replace (lo * 1) with lo in H3 by ring.
548  assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega.
549  replace ((hi + 1) * 1) with (hi + 1) in H4 by ring.
550  omega.
551  omega.
552Qed.
553
554(** Properties of divisibility. *)
555
556Lemma Zdivides_trans:
557  forall x y z, (x | y) -> (y | z) -> (x | z).
558Proof.
559  intros. inv H. inv H0. exists (q0 * q). ring.
560Qed.
561
562Definition Zdivide_dec:
563  forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.
564Proof.
565  intros. destruct (zeq (Zmod q p) 0).
566  left. exists (q / p).
567  transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto.
568  transitivity (p * (q / p)). omega. ring.
569  right; red; intros. elim n. apply Z_div_exact_1; auto.
570  inv H0. rewrite Z_div_mult; auto. ring.
571Defined.
572*)
573(* * Alignment: [align n amount] returns the smallest multiple of [amount]
574  greater than or equal to [n]. *)
575(*naxiom align : Z → Z → Z.*)
576
577definition align : nat → nat → nat ≝ λn: nat. λamount: nat.
578  ((minus (n + amount) 1) ÷ amount) * amount.
579(*
580Lemma align_le: forall x y, y > 0 -> x <= align x y.
581Proof.
582  intros. unfold align.
583  generalize (Z_div_mod_eq (x + y - 1) y H). intro.
584  replace ((x + y - 1) / y * y)
585     with ((x + y - 1) - (x + y - 1) mod y).
586  generalize (Z_mod_lt (x + y - 1) y H). omega.
587  rewrite Zmult_comm. omega.
588Qed.
589
590Lemma align_divides: forall x y, y > 0 -> (y | align x y).
591Proof.
592  intros. unfold align. apply Zdivide_factor_l.
593Qed.
594
595(** * Definitions and theorems on the data types [option], [sum] and [list] *)
596
597Set Implicit Arguments.
598*)
599(* * Mapping a function over an option type. *)
600
601definition option_map ≝ λA,B.λf:A→B.λv:option A.
602  match v with [ Some v' ⇒ Some ? (f v') | None ⇒ None ? ].
603
604(*
605(** Mapping a function over a sum type. *)
606
607Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C :=
608  match x with
609  | inl y => inl C (f y)
610  | inr z => inr B z
611  end.
612
613(** Properties of [List.nth] (n-th element of a list). *)
614
615Hint Resolve in_eq in_cons: coqlib.
616
617Lemma nth_error_in:
618  forall (A: Type) (n: nat) (l: list A) (x: A),
619  List.nth_error l n = Some x -> In x l.
620Proof.
621  induction n; simpl.
622   destruct l; intros.
623    discriminate.
624    injection H; intro; subst a. apply in_eq.
625   destruct l; intros.
626    discriminate.
627    apply in_cons. auto.
628Qed.
629Hint Resolve nth_error_in: coqlib.
630
631Lemma nth_error_nil:
632  forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.
633Proof.
634  induction idx; simpl; intros; reflexivity.
635Qed.
636Hint Resolve nth_error_nil: coqlib.
637
638(** Compute the length of a list, with result in [Z]. *)
639
640Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z :=
641  match l with
642  | nil => acc
643  | hd :: tl => list_length_z_aux tl (Zsucc acc)
644  end.
645
646Remark list_length_z_aux_shift:
647  forall (A: Type) (l: list A) n m,
648  list_length_z_aux l n = list_length_z_aux l m + (n - m).
649Proof.
650  induction l; intros; simpl.
651  omega.
652  replace (n - m) with (Zsucc n - Zsucc m) by omega. auto.
653Qed.
654
655Definition list_length_z (A: Type) (l: list A) : Z :=
656  list_length_z_aux l 0.
657
658Lemma list_length_z_cons:
659  forall (A: Type) (hd: A) (tl: list A),
660  list_length_z (hd :: tl) = list_length_z tl + 1.
661Proof.
662  intros. unfold list_length_z. simpl.
663  rewrite (list_length_z_aux_shift tl 1 0). omega.
664Qed.
665
666Lemma list_length_z_pos:
667  forall (A: Type) (l: list A),
668  list_length_z l >= 0.
669Proof.
670  induction l; simpl. unfold list_length_z; simpl. omega.
671  rewrite list_length_z_cons. omega.
672Qed.
673
674Lemma list_length_z_map:
675  forall (A B: Type) (f: A -> B) (l: list A),
676  list_length_z (map f l) = list_length_z l.
677Proof.
678  induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence.
679Qed.
680
681(** Extract the n-th element of a list, as [List.nth_error] does,
682    but the index [n] is of type [Z]. *)
683
684Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A :=
685  match l with
686  | nil => None
687  | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n)
688  end.
689
690Lemma list_nth_z_in:
691  forall (A: Type) (l: list A) n x,
692  list_nth_z l n = Some x -> In x l.
693Proof.
694  induction l; simpl; intros.
695  congruence.
696  destruct (zeq n 0). left; congruence. right; eauto.
697Qed.
698
699Lemma list_nth_z_map:
700  forall (A B: Type) (f: A -> B) (l: list A) n,
701  list_nth_z (List.map f l) n = option_map f (list_nth_z l n).
702Proof.
703  induction l; simpl; intros.
704  auto.
705  destruct (zeq n 0). auto. eauto.
706Qed.
707
708Lemma list_nth_z_range:
709  forall (A: Type) (l: list A) n x,
710  list_nth_z l n = Some x -> 0 <= n < list_length_z l.
711Proof.
712  induction l; simpl; intros.
713  discriminate.
714  rewrite list_length_z_cons. destruct (zeq n 0).
715  generalize (list_length_z_pos l); omega.
716  exploit IHl; eauto. unfold Zpred. omega.
717Qed.
718
719(** Properties of [List.incl] (list inclusion). *)
720
721Lemma incl_cons_inv:
722  forall (A: Type) (a: A) (b c: list A),
723  incl (a :: b) c -> incl b c.
724Proof.
725  unfold incl; intros. apply H. apply in_cons. auto.
726Qed.
727Hint Resolve incl_cons_inv: coqlib.
728
729Lemma incl_app_inv_l:
730  forall (A: Type) (l1 l2 m: list A),
731  incl (l1 ++ l2) m -> incl l1 m.
732Proof.
733  unfold incl; intros. apply H. apply in_or_app. left; assumption.
734Qed.
735
736Lemma incl_app_inv_r:
737  forall (A: Type) (l1 l2 m: list A),
738  incl (l1 ++ l2) m -> incl l2 m.
739Proof.
740  unfold incl; intros. apply H. apply in_or_app. right; assumption.
741Qed.
742
743Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
744
745Lemma incl_same_head:
746  forall (A: Type) (x: A) (l1 l2: list A),
747  incl l1 l2 -> incl (x::l1) (x::l2).
748Proof.
749  intros; red; simpl; intros. intuition.
750Qed.
751
752(** Properties of [List.map] (mapping a function over a list). *)
753
754Lemma list_map_exten:
755  forall (A B: Type) (f f': A -> B) (l: list A),
756  (forall x, In x l -> f x = f' x) ->
757  List.map f' l = List.map f l.
758Proof.
759  induction l; simpl; intros.
760  reflexivity.
761  rewrite <- H. rewrite IHl. reflexivity.
762  intros. apply H. tauto.
763  tauto.
764Qed.
765
766Lemma list_map_compose:
767  forall (A B C: Type) (f: A -> B) (g: B -> C) (l: list A),
768  List.map g (List.map f l) = List.map (fun x => g(f x)) l.
769Proof.
770  induction l; simpl. reflexivity. rewrite IHl; reflexivity.
771Qed.
772
773Lemma list_map_identity:
774  forall (A: Type) (l: list A),
775  List.map (fun (x:A) => x) l = l.
776Proof.
777  induction l; simpl; congruence.
778Qed.
779
780Lemma list_map_nth:
781  forall (A B: Type) (f: A -> B) (l: list A) (n: nat),
782  nth_error (List.map f l) n = option_map f (nth_error l n).
783Proof.
784  induction l; simpl; intros.
785  repeat rewrite nth_error_nil. reflexivity.
786  destruct n; simpl. reflexivity. auto.
787Qed.
788
789Lemma list_length_map:
790  forall (A B: Type) (f: A -> B) (l: list A),
791  List.length (List.map f l) = List.length l.
792Proof.
793  induction l; simpl; congruence.
794Qed.
795*) (*
796lemma list_in_map_inv:
797  ∀A,B: Type[0]. ∀f: A -> B. ∀l: list A. ∀y: B.
798  in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l.
799#A B f l; nelim l;
800##[ nnormalize; #y H; ninversion H;
801  ##[ #x l' e1 e2; ndestruct;
802  ##| #x z l' H1 H2 H3 H4; ndestruct;
803  ##]
804##| #x l' IH y H; ninversion H;
805  ##[ nnormalize; #y' l'' e1 e2; ndestruct; @x; @; //;
806  ##| nnormalize; #h h' t H1 H2 H3 H4; ndestruct;
807      nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/;
808  ##]
809##] nqed.*)
810(*
811Lemma list_append_map:
812  forall (A B: Type) (f: A -> B) (l1 l2: list A),
813  List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.
814Proof.
815  induction l1; simpl; intros.
816  auto. rewrite IHl1. auto.
817Qed.
818
819(** Properties of list membership. *)
820
821Lemma in_cns:
822  forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
823Proof.
824  intros. simpl. tauto.
825Qed.
826
827Lemma in_app:
828  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
829Proof.
830  intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
831Qed.
832
833Lemma list_in_insert:
834  forall (A: Type) (x: A) (l1 l2: list A) (y: A),
835  In x (l1 ++ l2) -> In x (l1 ++ y :: l2).
836Proof.
837  intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto.
838Qed.
839*)
840(* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements
841  in common. *)
842(*
843definition list_disjoint : ∀A:Type[0]. list A → list A → Prop ≝
844  λA,l1,l2.
845  ∀x,y: A. in_list A x l1 → in_list A y l2 → x ≠ y.
846
847lemma list_disjoint_cons_left:
848  ∀A: Type[0]. ∀a: A. ∀l1,l2: list A.
849  list_disjoint A (a :: l1) l2 → list_disjoint A l1 l2.
850#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
851#x;#y;#in1;#in2; napply H; /2/;
852nqed.
853
854nlemma list_disjoint_cons_right:
855  ∀A: Type. ∀a: A. ∀l1,l2: list A.
856  list_disjoint A l1 (a :: l2) → list_disjoint A l1 l2.
857#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
858#x;#y;#in1;#in2; napply H; /2/;
859nqed.
860
861nlemma list_disjoint_notin:
862  ∀A: Type. ∀l1,l2: list A. ∀a: A.
863  list_disjoint A l1 l2 → in_list A a l1 → ¬(in_list A a l2).
864#A;#l1;#l2;#a;nwhd in ⊢ (% → ?); #H; #H1;
865napply nmk; #H2;
866napply (absurd ?? (H … H1 H2)); //;
867nqed.
868
869nlemma list_disjoint_sym:
870  ∀A: Type. ∀l1,l2: list A.
871  list_disjoint A l1 l2 → list_disjoint A l2 l1.
872#A;#l1;#l2;
873nwhd in ⊢ (% → %);
874#H;#x;#y;#H1;#H2; napply sym_neq; /2/;
875nqed.*)
876
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(*
901inductive list_norepet (A: Type[0]) : 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.