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