source: src/utilities/Coqlib.ma @ 761

Last change on this file since 761 was 761, checked in by campbell, 9 years ago

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

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 "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
601include "utilities/option.ma".
602
603(*
604(** Mapping a function over a sum type. *)
605
606Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C :=
607  match x with
608  | inl y => inl C (f y)
609  | inr z => inr B z
610  end.
611
612(** Properties of [List.nth] (n-th element of a list). *)
613
614Hint Resolve in_eq in_cons: coqlib.
615
616Lemma nth_error_in:
617  forall (A: Type) (n: nat) (l: list A) (x: A),
618  List.nth_error l n = Some x -> In x l.
619Proof.
620  induction n; simpl.
621   destruct l; intros.
622    discriminate.
623    injection H; intro; subst a. apply in_eq.
624   destruct l; intros.
625    discriminate.
626    apply in_cons. auto.
627Qed.
628Hint Resolve nth_error_in: coqlib.
629
630Lemma nth_error_nil:
631  forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.
632Proof.
633  induction idx; simpl; intros; reflexivity.
634Qed.
635Hint Resolve nth_error_nil: coqlib.
636
637(** Compute the length of a list, with result in [Z]. *)
638
639Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z :=
640  match l with
641  | nil => acc
642  | hd :: tl => list_length_z_aux tl (Zsucc acc)
643  end.
644
645Remark list_length_z_aux_shift:
646  forall (A: Type) (l: list A) n m,
647  list_length_z_aux l n = list_length_z_aux l m + (n - m).
648Proof.
649  induction l; intros; simpl.
650  omega.
651  replace (n - m) with (Zsucc n - Zsucc m) by omega. auto.
652Qed.
653
654Definition list_length_z (A: Type) (l: list A) : Z :=
655  list_length_z_aux l 0.
656
657Lemma list_length_z_cons:
658  forall (A: Type) (hd: A) (tl: list A),
659  list_length_z (hd :: tl) = list_length_z tl + 1.
660Proof.
661  intros. unfold list_length_z. simpl.
662  rewrite (list_length_z_aux_shift tl 1 0). omega.
663Qed.
664
665Lemma list_length_z_pos:
666  forall (A: Type) (l: list A),
667  list_length_z l >= 0.
668Proof.
669  induction l; simpl. unfold list_length_z; simpl. omega.
670  rewrite list_length_z_cons. omega.
671Qed.
672
673Lemma list_length_z_map:
674  forall (A B: Type) (f: A -> B) (l: list A),
675  list_length_z (map f l) = list_length_z l.
676Proof.
677  induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence.
678Qed.
679
680(** Extract the n-th element of a list, as [List.nth_error] does,
681    but the index [n] is of type [Z]. *)
682
683Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A :=
684  match l with
685  | nil => None
686  | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n)
687  end.
688
689Lemma list_nth_z_in:
690  forall (A: Type) (l: list A) n x,
691  list_nth_z l n = Some x -> In x l.
692Proof.
693  induction l; simpl; intros.
694  congruence.
695  destruct (zeq n 0). left; congruence. right; eauto.
696Qed.
697
698Lemma list_nth_z_map:
699  forall (A B: Type) (f: A -> B) (l: list A) n,
700  list_nth_z (List.map f l) n = option_map f (list_nth_z l n).
701Proof.
702  induction l; simpl; intros.
703  auto.
704  destruct (zeq n 0). auto. eauto.
705Qed.
706
707Lemma list_nth_z_range:
708  forall (A: Type) (l: list A) n x,
709  list_nth_z l n = Some x -> 0 <= n < list_length_z l.
710Proof.
711  induction l; simpl; intros.
712  discriminate.
713  rewrite list_length_z_cons. destruct (zeq n 0).
714  generalize (list_length_z_pos l); omega.
715  exploit IHl; eauto. unfold Zpred. omega.
716Qed.
717
718(** Properties of [List.incl] (list inclusion). *)
719
720Lemma incl_cons_inv:
721  forall (A: Type) (a: A) (b c: list A),
722  incl (a :: b) c -> incl b c.
723Proof.
724  unfold incl; intros. apply H. apply in_cons. auto.
725Qed.
726Hint Resolve incl_cons_inv: coqlib.
727
728Lemma incl_app_inv_l:
729  forall (A: Type) (l1 l2 m: list A),
730  incl (l1 ++ l2) m -> incl l1 m.
731Proof.
732  unfold incl; intros. apply H. apply in_or_app. left; assumption.
733Qed.
734
735Lemma incl_app_inv_r:
736  forall (A: Type) (l1 l2 m: list A),
737  incl (l1 ++ l2) m -> incl l2 m.
738Proof.
739  unfold incl; intros. apply H. apply in_or_app. right; assumption.
740Qed.
741
742Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.
743
744Lemma incl_same_head:
745  forall (A: Type) (x: A) (l1 l2: list A),
746  incl l1 l2 -> incl (x::l1) (x::l2).
747Proof.
748  intros; red; simpl; intros. intuition.
749Qed.
750
751(** Properties of [List.map] (mapping a function over a list). *)
752
753Lemma list_map_exten:
754  forall (A B: Type) (f f': A -> B) (l: list A),
755  (forall x, In x l -> f x = f' x) ->
756  List.map f' l = List.map f l.
757Proof.
758  induction l; simpl; intros.
759  reflexivity.
760  rewrite <- H. rewrite IHl. reflexivity.
761  intros. apply H. tauto.
762  tauto.
763Qed.
764
765Lemma list_map_compose:
766  forall (A B C: Type) (f: A -> B) (g: B -> C) (l: list A),
767  List.map g (List.map f l) = List.map (fun x => g(f x)) l.
768Proof.
769  induction l; simpl. reflexivity. rewrite IHl; reflexivity.
770Qed.
771
772Lemma list_map_identity:
773  forall (A: Type) (l: list A),
774  List.map (fun (x:A) => x) l = l.
775Proof.
776  induction l; simpl; congruence.
777Qed.
778
779Lemma list_map_nth:
780  forall (A B: Type) (f: A -> B) (l: list A) (n: nat),
781  nth_error (List.map f l) n = option_map f (nth_error l n).
782Proof.
783  induction l; simpl; intros.
784  repeat rewrite nth_error_nil. reflexivity.
785  destruct n; simpl. reflexivity. auto.
786Qed.
787
788Lemma list_length_map:
789  forall (A B: Type) (f: A -> B) (l: list A),
790  List.length (List.map f l) = List.length l.
791Proof.
792  induction l; simpl; congruence.
793Qed.
794*) (*
795lemma list_in_map_inv:
796  ∀A,B: Type[0]. ∀f: A -> B. ∀l: list A. ∀y: B.
797  in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l.
798#A B f l; nelim l;
799##[ nnormalize; #y H; ninversion H;
800  ##[ #x l' e1 e2; ndestruct;
801  ##| #x z l' H1 H2 H3 H4; ndestruct;
802  ##]
803##| #x l' IH y H; ninversion H;
804  ##[ nnormalize; #y' l'' e1 e2; ndestruct; @x; @; //;
805  ##| nnormalize; #h h' t H1 H2 H3 H4; ndestruct;
806      nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/;
807  ##]
808##] nqed.*)
809(*
810Lemma list_append_map:
811  forall (A B: Type) (f: A -> B) (l1 l2: list A),
812  List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.
813Proof.
814  induction l1; simpl; intros.
815  auto. rewrite IHl1. auto.
816Qed.
817
818(** Properties of list membership. *)
819
820Lemma in_cns:
821  forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.
822Proof.
823  intros. simpl. tauto.
824Qed.
825
826Lemma in_app:
827  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.
828Proof.
829  intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.
830Qed.
831
832Lemma list_in_insert:
833  forall (A: Type) (x: A) (l1 l2: list A) (y: A),
834  In x (l1 ++ l2) -> In x (l1 ++ y :: l2).
835Proof.
836  intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; auto.
837Qed.
838*)
839(* * [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements
840  in common. *)
841(*
842definition list_disjoint : ∀A:Type[0]. list A → list A → Prop ≝
843  λA,l1,l2.
844  ∀x,y: A. in_list A x l1 → in_list A y l2 → x ≠ y.
845
846lemma list_disjoint_cons_left:
847  ∀A: Type[0]. ∀a: A. ∀l1,l2: list A.
848  list_disjoint A (a :: l1) l2 → list_disjoint A l1 l2.
849#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
850#x;#y;#in1;#in2; napply H; /2/;
851nqed.
852
853nlemma list_disjoint_cons_right:
854  ∀A: Type. ∀a: A. ∀l1,l2: list A.
855  list_disjoint A l1 (a :: l2) → list_disjoint A l1 l2.
856#A;#a;#l1;#l2;nwhd in ⊢ (% → %); #H;
857#x;#y;#in1;#in2; napply H; /2/;
858nqed.
859
860nlemma list_disjoint_notin:
861  ∀A: Type. ∀l1,l2: list A. ∀a: A.
862  list_disjoint A l1 l2 → in_list A a l1 → ¬(in_list A a l2).
863#A;#l1;#l2;#a;nwhd in ⊢ (% → ?); #H; #H1;
864napply nmk; #H2;
865napply (absurd ?? (H … H1 H2)); //;
866nqed.
867
868nlemma list_disjoint_sym:
869  ∀A: Type. ∀l1,l2: list A.
870  list_disjoint A l1 l2 → list_disjoint A l2 l1.
871#A;#l1;#l2;
872nwhd in ⊢ (% → %);
873#H;#x;#y;#H1;#H2; napply sym_neq; /2/;
874nqed.*)
875
876(*
877Lemma list_disjoint_dec:
878  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),
879  {list_disjoint l1 l2} + {~list_disjoint l1 l2}.
880Proof.
881  induction l1; intros.
882  left; red; intros. elim H.
883  case (In_dec eqA_dec a l2); intro.
884  right; red; intro. apply (H a a); auto with coqlib.
885  case (IHl1 l2); intro.
886  left; red; intros. elim H; intro.
887    red; intro; subst a y. contradiction.
888    apply l; auto.
889  right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto.
890Defined.
891
892(** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *)
893
894Definition list_equiv (A : Type) (l1 l2: list A) : Prop :=
895  forall x, In x l1 <-> In x l2.
896*)
897(* * [list_norepet l] holds iff the list [l] contains no repetitions,
898  i.e. no element occurs twice. *)
899(*
900inductive list_norepet (A: Type[0]) : list A → Prop ≝
901  | list_norepet_nil:
902      list_norepet A (nil A)
903  | list_norepet_cons:
904      ∀hd,tl.
905      ¬(in_list A hd tl) → list_norepet A tl → list_norepet A (hd :: tl).*)
906(*
907Lemma list_norepet_dec:
908  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),
909  {list_norepet l} + {~list_norepet l}.
910Proof.
911  induction l.
912  left; constructor.
913  destruct IHl.
914  case (In_dec eqA_dec a l); intro.
915  right. red; intro. inversion H. contradiction.
916  left. constructor; auto.
917  right. red; intro. inversion H. contradiction.
918Defined.
919
920Lemma list_map_norepet:
921  forall (A B: Type) (f: A -> B) (l: list A),
922  list_norepet l ->
923  (forall x y, In x l -> In y l -> x <> y -> f x <> f y) ->
924  list_norepet (List.map f l).
925Proof.
926  induction 1; simpl; intros.
927  constructor.
928  constructor.
929  red; intro. generalize (list_in_map_inv f _ _ H2).
930  intros [x [EQ IN]]. generalize EQ. change (f hd <> f x).
931  apply H1. tauto. tauto.
932  red; intro; subst x. contradiction.
933  apply IHlist_norepet. intros. apply H1. tauto. tauto. auto.
934Qed.
935
936Remark list_norepet_append_commut:
937  forall (A: Type) (a b: list A),
938  list_norepet (a ++ b) -> list_norepet (b ++ a).
939Proof.
940  intro A.
941  assert (forall (x: A) (b: list A) (a: list A),
942           list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) ->
943           list_norepet (a ++ x :: b)).
944    induction a; simpl; intros.
945    constructor; auto.
946    inversion H. constructor. red; intro.
947    elim (in_app_or _ _ _ H6); intro.
948    elim H4. apply in_or_app. tauto.
949    elim H7; intro. subst a. elim H0. left. auto.
950    elim H4. apply in_or_app. tauto.
951    auto.
952  induction a; simpl; intros.
953  rewrite <- app_nil_end. auto.
954  inversion H0. apply H. auto.
955  red; intro; elim H3. apply in_or_app. tauto.
956  red; intro; elim H3. apply in_or_app. tauto.
957Qed.
958
959Lemma list_norepet_app:
960  forall (A: Type) (l1 l2: list A),
961  list_norepet (l1 ++ l2) <->
962  list_norepet l1 /\ list_norepet l2 /\ list_disjoint l1 l2.
963Proof.
964  induction l1; simpl; intros; split; intros.
965  intuition. constructor. red;simpl;auto.
966  tauto.
967  inversion H; subst. rewrite IHl1 in H3. rewrite in_app in H2.
968  intuition.
969  constructor; auto. red; intros. elim H2; intro. congruence. auto.
970  destruct H as [B [C D]]. inversion B; subst.
971  constructor. rewrite in_app. intuition. elim (D a a); auto. apply in_eq.
972  rewrite IHl1. intuition. red; intros. apply D; auto. apply in_cons; auto.
973Qed.
974
975Lemma list_norepet_append:
976  forall (A: Type) (l1 l2: list A),
977  list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->
978  list_norepet (l1 ++ l2).
979Proof.
980  generalize list_norepet_app; firstorder.
981Qed.
982
983Lemma list_norepet_append_right:
984  forall (A: Type) (l1 l2: list A),
985  list_norepet (l1 ++ l2) -> list_norepet l2.
986Proof.
987  generalize list_norepet_app; firstorder.
988Qed.
989
990Lemma list_norepet_append_left:
991  forall (A: Type) (l1 l2: list A),
992  list_norepet (l1 ++ l2) -> list_norepet l1.
993Proof.
994  generalize list_norepet_app; firstorder.
995Qed.
996
997(** [is_tail l1 l2] holds iff [l2] is of the form [l ++ l1] for some [l]. *)
998
999Inductive is_tail (A: Type): list A -> list A -> Prop :=
1000  | is_tail_refl:
1001      forall c, is_tail c c
1002  | is_tail_cons:
1003      forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).
1004
1005Lemma is_tail_in:
1006  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.
1007Proof.
1008  induction c2; simpl; intros.
1009  inversion H.
1010  inversion H. tauto. right; auto.
1011Qed.
1012
1013Lemma is_tail_cons_left:
1014  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
1015Proof.
1016  induction c2; intros; inversion H.
1017  constructor. constructor. constructor. auto.
1018Qed.
1019
1020Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.
1021
1022Lemma is_tail_incl:
1023  forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.
1024Proof.
1025  induction 1; eauto with coqlib.
1026Qed.
1027
1028Lemma is_tail_trans:
1029  forall (A: Type) (l1 l2: list A),
1030  is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3.
1031Proof.
1032  induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.
1033Qed.
1034
1035(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and
1036  [P xi yi] holds for all [i]. *)
1037
1038Section FORALL2.
1039
1040Variable A: Type.
1041Variable B: Type.
1042Variable P: A -> B -> Prop.
1043
1044Inductive list_forall2: list A -> list B -> Prop :=
1045  | list_forall2_nil:
1046      list_forall2 nil nil
1047  | list_forall2_cons:
1048      forall a1 al b1 bl,
1049      P a1 b1 ->
1050      list_forall2 al bl ->
1051      list_forall2 (a1 :: al) (b1 :: bl).
1052
1053End FORALL2.
1054
1055Lemma list_forall2_imply:
1056  forall (A B: Type) (P1: A -> B -> Prop) (l1: list A) (l2: list B),
1057  list_forall2 P1 l1 l2 ->
1058  forall (P2: A -> B -> Prop),
1059  (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) ->
1060  list_forall2 P2 l1 l2.
1061Proof.
1062  induction 1; intros.
1063  constructor.
1064  constructor. auto with coqlib. apply IHlist_forall2; auto.
1065  intros. auto with coqlib.
1066Qed.
1067
1068(** Dropping the first N elements of a list. *)
1069
1070Fixpoint list_drop (A: Type) (n: nat) (x: list A) {struct n} : list A :=
1071  match n with
1072  | O => x
1073  | S n' => match x with nil => nil | hd :: tl => list_drop n' tl end
1074  end.
1075
1076Lemma list_drop_incl:
1077  forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l.
1078Proof.
1079  induction n; simpl; intros. auto.
1080  destruct l; auto with coqlib.
1081Qed.
1082
1083Lemma list_drop_norepet:
1084  forall (A: Type) n (l: list A), list_norepet l -> list_norepet (list_drop n l).
1085Proof.
1086  induction n; simpl; intros. auto.
1087  inv H. constructor. auto.
1088Qed.
1089
1090Lemma list_map_drop:
1091  forall (A B: Type) (f: A -> B) n (l: list A),
1092  list_drop n (map f l) = map f (list_drop n l).
1093Proof.
1094  induction n; simpl; intros. auto.
1095  destruct l; simpl; auto.
1096Qed.
1097
1098(** * Definitions and theorems over boolean types *)
1099
1100Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=
1101  if a then true else false.
1102
1103Implicit Arguments proj_sumbool [P Q].
1104
1105Coercion proj_sumbool: sumbool >-> bool.
1106
1107Lemma proj_sumbool_true:
1108  forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P.
1109Proof.
1110  intros P Q a. destruct a; simpl. auto. congruence.
1111Qed.
1112
1113Section DECIDABLE_EQUALITY.
1114
1115Variable A: Type.
1116Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.
1117Variable B: Type.
1118
1119Lemma dec_eq_true:
1120  forall (x: A) (ifso ifnot: B),
1121  (if dec_eq x x then ifso else ifnot) = ifso.
1122Proof.
1123  intros. destruct (dec_eq x x). auto. congruence.
1124Qed.
1125
1126Lemma dec_eq_false:
1127  forall (x y: A) (ifso ifnot: B),
1128  x <> y -> (if dec_eq x y then ifso else ifnot) = ifnot.
1129Proof.
1130  intros. destruct (dec_eq x y). congruence. auto.
1131Qed.
1132
1133Lemma dec_eq_sym:
1134  forall (x y: A) (ifso ifnot: B),
1135  (if dec_eq x y then ifso else ifnot) =
1136  (if dec_eq y x then ifso else ifnot).
1137Proof.
1138  intros. destruct (dec_eq x y).
1139  subst y. rewrite dec_eq_true. auto.
1140  rewrite dec_eq_false; auto.
1141Qed.
1142
1143End DECIDABLE_EQUALITY.
1144*)
Note: See TracBrowser for help on using the repository browser.