source: Deliverables/D3.1/C-semantics/Coqlib.ma @ 535

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

Port Clight semantics to the new-new matita syntax.

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