source: src/utilities/Coqlib.ma @ 744

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

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

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