diff options
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 709 |
1 files changed, 709 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v new file mode 100644 index 0000000..039dd03 --- /dev/null +++ b/lib/Coqlib.v @@ -0,0 +1,709 @@ +(** This file collects a number of definitions and theorems that are + used throughout the development. It complements the Coq standard + library. *) + +Require Export ZArith. +Require Export List. +Require Import Wf_nat. + +(** * Logical axioms *) + +(** We use two logical axioms that are not provable in Coq but consistent + with the logic: function extensionality and proof irrelevance. + These are used in the memory model to show that two memory states + that have identical contents are equal. *) + +Axiom extensionality: + forall (A B: Set) (f g : A -> B), + (forall x, f x = g x) -> f = g. + +Axiom proof_irrelevance: + forall (P: Prop) (p1 p2: P), p1 = p2. + +(** * Useful tactics *) + +Ltac predSpec pred predspec x y := + generalize (predspec x y); case (pred x y); intro. + +Ltac caseEq name := + generalize (refl_equal name); pattern name at -1 in |- *; case name. + +Ltac destructEq name := + generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro. + +Ltac decEq := + match goal with + | [ |- (_, _) = (_, _) ] => + apply injective_projections; unfold fst,snd; try reflexivity + | [ |- (@Some ?T _ = @Some ?T _) ] => + apply (f_equal (@Some T)); try reflexivity + | [ |- (?X _ _ _ _ _ = ?X _ _ _ _ _) ] => + apply (f_equal5 X); try reflexivity + | [ |- (?X _ _ _ _ = ?X _ _ _ _) ] => + apply (f_equal4 X); try reflexivity + | [ |- (?X _ _ _ = ?X _ _ _) ] => + apply (f_equal3 X); try reflexivity + | [ |- (?X _ _ = ?X _ _) ] => + apply (f_equal2 X); try reflexivity + | [ |- (?X _ = ?X _) ] => + apply (f_equal X); try reflexivity + | [ |- (?X ?A <> ?X ?B) ] => + cut (A <> B); [intro; congruence | try discriminate] + end. + +Ltac byContradiction := + cut False; [contradiction|idtac]. + +Ltac omegaContradiction := + cut False; [contradiction|omega]. + +(** * Definitions and theorems over the type [positive] *) + +Definition peq (x y: positive): {x = y} + {x <> y}. +Proof. + intros. caseEq (Pcompare x y Eq). + intro. left. apply Pcompare_Eq_eq; auto. + intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. + intro. right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. +Qed. + +Lemma peq_true: + forall (A: Set) (x: positive) (a b: A), (if peq x x then a else b) = a. +Proof. + intros. case (peq x x); intros. + auto. + elim n; auto. +Qed. + +Lemma peq_false: + forall (A: Set) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b. +Proof. + intros. case (peq x y); intros. + elim H; auto. + auto. +Qed. + +Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y). + +Lemma Plt_ne: + forall (x y: positive), Plt x y -> x <> y. +Proof. + unfold Plt; intros. red; intro. subst y. omega. +Qed. +Hint Resolve Plt_ne: coqlib. + +Lemma Plt_trans: + forall (x y z: positive), Plt x y -> Plt y z -> Plt x z. +Proof. + unfold Plt; intros; omega. +Qed. + +Remark Psucc_Zsucc: + forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x). +Proof. + intros. rewrite Pplus_one_succ_r. + reflexivity. +Qed. + +Lemma Plt_succ: + forall (x: positive), Plt x (Psucc x). +Proof. + intro. unfold Plt. rewrite Psucc_Zsucc. omega. +Qed. +Hint Resolve Plt_succ: coqlib. + +Lemma Plt_trans_succ: + forall (x y: positive), Plt x y -> Plt x (Psucc y). +Proof. + intros. apply Plt_trans with y. assumption. apply Plt_succ. +Qed. +Hint Resolve Plt_succ: coqlib. + +Lemma Plt_succ_inv: + forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y. +Proof. + intros x y. unfold Plt. rewrite Psucc_Zsucc. + intro. assert (A: (Zpos x < Zpos y)%Z \/ Zpos x = Zpos y). omega. + elim A; intro. left; auto. right; injection H0; auto. +Qed. + +Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}. +Proof. + intros. unfold Plt. apply Z_lt_dec. +Qed. + +Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q). + +Lemma Ple_refl: forall (p: positive), Ple p p. +Proof. + unfold Ple; intros; omega. +Qed. + +Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r. +Proof. + unfold Ple; intros; omega. +Qed. + +Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q. +Proof. + unfold Plt, Ple; intros; omega. +Qed. + +Lemma Ple_succ: forall (p: positive), Ple p (Psucc p). +Proof. + intros. apply Plt_Ple. apply Plt_succ. +Qed. + +Lemma Plt_Ple_trans: + forall (p q r: positive), Plt p q -> Ple q r -> Plt p r. +Proof. + unfold Plt, Ple; intros; omega. +Qed. + +Lemma Plt_strict: forall p, ~ Plt p p. +Proof. + unfold Plt; intros. omega. +Qed. + +Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. + +(** Peano recursion over positive numbers. *) + +Section POSITIVE_ITERATION. + +Lemma Plt_wf: well_founded Plt. +Proof. + apply well_founded_lt_compat with nat_of_P. + intros. apply nat_of_P_lt_Lt_compare_morphism. exact H. +Qed. + +Variable A: Set. +Variable v1: A. +Variable f: positive -> A -> A. + +Lemma Ppred_Plt: + forall x, x <> xH -> Plt (Ppred x) x. +Proof. + intros. elim (Psucc_pred x); intro. contradiction. + set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ. +Qed. + +Let iter (x: positive) (P: forall y, Plt y x -> A) : A := + match peq x xH with + | left EQ => v1 + | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ)) + end. + +Definition positive_rec : positive -> A := + Fix Plt_wf (fun _ => A) iter. + +Lemma unroll_positive_rec: + forall x, + positive_rec x = iter x (fun y _ => positive_rec y). +Proof. + unfold positive_rec. apply (Fix_eq Plt_wf (fun _ => A) iter). + intros. unfold iter. case (peq x 1); intro. auto. decEq. apply H. +Qed. + +Lemma positive_rec_base: + positive_rec 1%positive = v1. +Proof. + rewrite unroll_positive_rec. unfold iter. case (peq 1 1); intro. + auto. elim n; auto. +Qed. + +Lemma positive_rec_succ: + forall x, positive_rec (Psucc x) = f x (positive_rec x). +Proof. + intro. rewrite unroll_positive_rec. unfold iter. + case (peq (Psucc x) 1); intro. + destruct x; simpl in e; discriminate. + rewrite Ppred_succ. auto. +Qed. + +Lemma positive_Peano_ind: + forall (P: positive -> Prop), + P xH -> + (forall x, P x -> P (Psucc x)) -> + forall x, P x. +Proof. + intros. + apply (well_founded_ind Plt_wf P). + intros. + case (peq x0 xH); intro. + subst x0; auto. + elim (Psucc_pred x0); intro. contradiction. rewrite <- H2. + apply H0. apply H1. apply Ppred_Plt. auto. +Qed. + +End POSITIVE_ITERATION. + +(** * Definitions and theorems over the type [Z] *) + +Definition zeq: forall (x y: Z), {x = y} + {x <> y} := Z_eq_dec. + +Lemma zeq_true: + forall (A: Set) (x: Z) (a b: A), (if zeq x x then a else b) = a. +Proof. + intros. case (zeq x x); intros. + auto. + elim n; auto. +Qed. + +Lemma zeq_false: + forall (A: Set) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b. +Proof. + intros. case (zeq x y); intros. + elim H; auto. + auto. +Qed. + +Open Scope Z_scope. + +Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec. + +Lemma zlt_true: + forall (A: Set) (x y: Z) (a b: A), + x < y -> (if zlt x y then a else b) = a. +Proof. + intros. case (zlt x y); intros. + auto. + omegaContradiction. +Qed. + +Lemma zlt_false: + forall (A: Set) (x y: Z) (a b: A), + x >= y -> (if zlt x y then a else b) = b. +Proof. + intros. case (zlt x y); intros. + omegaContradiction. + auto. +Qed. + +Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec. + +Lemma zle_true: + forall (A: Set) (x y: Z) (a b: A), + x <= y -> (if zle x y then a else b) = a. +Proof. + intros. case (zle x y); intros. + auto. + omegaContradiction. +Qed. + +Lemma zle_false: + forall (A: Set) (x y: Z) (a b: A), + x > y -> (if zle x y then a else b) = b. +Proof. + intros. case (zle x y); intros. + omegaContradiction. + auto. +Qed. + +(** Properties of powers of two. *) + +Lemma two_power_nat_O : two_power_nat O = 1. +Proof. reflexivity. Qed. + +Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0. +Proof. + induction n. rewrite two_power_nat_O. omega. + rewrite two_power_nat_S. omega. +Qed. + +(** Properties of [Zmin] and [Zmax] *) + +Lemma Zmin_spec: + forall x y, Zmin x y = if zlt x y then x else y. +Proof. + intros. case (zlt x y); unfold Zlt, Zge; intros. + unfold Zmin. rewrite z. auto. + unfold Zmin. caseEq (x ?= y); intro. + apply Zcompare_Eq_eq. auto. + contradiction. + reflexivity. +Qed. + +Lemma Zmax_spec: + forall x y, Zmax x y = if zlt y x then x else y. +Proof. + intros. case (zlt y x); unfold Zlt, Zge; intros. + unfold Zmax. rewrite <- (Zcompare_antisym y x). + rewrite z. simpl. auto. + unfold Zmax. rewrite <- (Zcompare_antisym y x). + caseEq (y ?= x); intro; simpl. + symmetry. apply Zcompare_Eq_eq. auto. + contradiction. reflexivity. +Qed. + +Lemma Zmax_bound_l: + forall x y z, x <= y -> x <= Zmax y z. +Proof. + intros. generalize (Zmax1 y z). omega. +Qed. +Lemma Zmax_bound_r: + forall x y z, x <= z -> x <= Zmax y z. +Proof. + intros. generalize (Zmax2 y z). omega. +Qed. + +(** Properties of Euclidean division and modulus. *) + +Lemma Zdiv_small: + forall x y, 0 <= x < y -> x / y = 0. +Proof. + intros. assert (y > 0). omega. + assert (forall a b, + 0 <= a < y -> + 0 <= y * b + a < y -> + b = 0). + intros. + assert (b = 0 \/ b > 0 \/ (-b) > 0). omega. + elim H3; intro. + auto. + elim H4; intro. + assert (y * b >= y * 1). apply Zmult_ge_compat_l. omega. omega. + omegaContradiction. + assert (y * (-b) >= y * 1). apply Zmult_ge_compat_l. omega. omega. + rewrite <- Zopp_mult_distr_r in H6. omegaContradiction. + apply H1 with (x mod y). + apply Z_mod_lt. auto. + rewrite <- Z_div_mod_eq. auto. auto. +Qed. + +Lemma Zmod_small: + forall x y, 0 <= x < y -> x mod y = x. +Proof. + intros. assert (y > 0). omega. + generalize (Z_div_mod_eq x y H0). + rewrite (Zdiv_small x y H). omega. +Qed. + +Lemma Zmod_unique: + forall x y a b, + x = a * y + b -> 0 <= b < y -> x mod y = b. +Proof. + intros. subst x. rewrite Zplus_comm. + rewrite Z_mod_plus. apply Zmod_small. auto. omega. +Qed. + +Lemma Zdiv_unique: + forall x y a b, + x = a * y + b -> 0 <= b < y -> x / y = a. +Proof. + intros. subst x. rewrite Zplus_comm. + rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega. +Qed. + +(** Alignment: [align n amount] returns the smallest multiple of [amount] + greater than or equal to [n]. *) + +Definition align (n: Z) (amount: Z) := + ((n + amount - 1) / amount) * amount. + +Lemma align_le: forall x y, y > 0 -> x <= align x y. +Proof. + intros. unfold align. + generalize (Z_div_mod_eq (x + y - 1) y H). intro. + replace ((x + y - 1) / y * y) + with ((x + y - 1) - (x + y - 1) mod y). + generalize (Z_mod_lt (x + y - 1) y H). omega. + rewrite Zmult_comm. omega. +Qed. + +(** * Definitions and theorems on the data types [option], [sum] and [list] *) + +Set Implicit Arguments. + +(** Mapping a function over an option type. *) + +Definition option_map (A B: Set) (f: A -> B) (x: option A) : option B := + match x with + | None => None + | Some y => Some (f y) + end. + +(** Mapping a function over a sum type. *) + +Definition sum_left_map (A B C: Set) (f: A -> B) (x: A + C) : B + C := + match x with + | inl y => inl C (f y) + | inr z => inr B z + end. + +(** Properties of [List.nth] (n-th element of a list). *) + +Hint Resolve in_eq in_cons: coqlib. + +Lemma nth_error_in: + forall (A: Set) (n: nat) (l: list A) (x: A), + List.nth_error l n = Some x -> In x l. +Proof. + induction n; simpl. + destruct l; intros. + discriminate. + injection H; intro; subst a. apply in_eq. + destruct l; intros. + discriminate. + apply in_cons. auto. +Qed. +Hint Resolve nth_error_in: coqlib. + +Lemma nth_error_nil: + forall (A: Set) (idx: nat), nth_error (@nil A) idx = None. +Proof. + induction idx; simpl; intros; reflexivity. +Qed. +Hint Resolve nth_error_nil: coqlib. + +(** Properties of [List.incl] (list inclusion). *) + +Lemma incl_cons_inv: + forall (A: Set) (a: A) (b c: list A), + incl (a :: b) c -> incl b c. +Proof. + unfold incl; intros. apply H. apply in_cons. auto. +Qed. +Hint Resolve incl_cons_inv: coqlib. + +Lemma incl_app_inv_l: + forall (A: Set) (l1 l2 m: list A), + incl (l1 ++ l2) m -> incl l1 m. +Proof. + unfold incl; intros. apply H. apply in_or_app. left; assumption. +Qed. + +Lemma incl_app_inv_r: + forall (A: Set) (l1 l2 m: list A), + incl (l1 ++ l2) m -> incl l2 m. +Proof. + unfold incl; intros. apply H. apply in_or_app. right; assumption. +Qed. + +Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. + +Lemma incl_same_head: + forall (A: Set) (x: A) (l1 l2: list A), + incl l1 l2 -> incl (x::l1) (x::l2). +Proof. + intros; red; simpl; intros. intuition. +Qed. + +(** Properties of [List.map] (mapping a function over a list). *) + +Lemma list_map_exten: + forall (A B: Set) (f f': A -> B) (l: list A), + (forall x, In x l -> f x = f' x) -> + List.map f' l = List.map f l. +Proof. + induction l; simpl; intros. + reflexivity. + rewrite <- H. rewrite IHl. reflexivity. + intros. apply H. tauto. + tauto. +Qed. + +Lemma list_map_compose: + forall (A B C: Set) (f: A -> B) (g: B -> C) (l: list A), + List.map g (List.map f l) = List.map (fun x => g(f x)) l. +Proof. + induction l; simpl. reflexivity. rewrite IHl; reflexivity. +Qed. + +Lemma list_map_nth: + forall (A B: Set) (f: A -> B) (l: list A) (n: nat), + nth_error (List.map f l) n = option_map f (nth_error l n). +Proof. + induction l; simpl; intros. + repeat rewrite nth_error_nil. reflexivity. + destruct n; simpl. reflexivity. auto. +Qed. + +Lemma list_length_map: + forall (A B: Set) (f: A -> B) (l: list A), + List.length (List.map f l) = List.length l. +Proof. + induction l; simpl; congruence. +Qed. + +Lemma list_in_map_inv: + forall (A B: Set) (f: A -> B) (l: list A) (y: B), + In y (List.map f l) -> exists x:A, y = f x /\ In x l. +Proof. + induction l; simpl; intros. + contradiction. + elim H; intro. + exists a; intuition auto. + generalize (IHl y H0). intros [x [EQ IN]]. + exists x; tauto. +Qed. + +Lemma list_append_map: + forall (A B: Set) (f: A -> B) (l1 l2: list A), + List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2. +Proof. + induction l1; simpl; intros. + auto. rewrite IHl1. auto. +Qed. + +(** [list_disjoint l1 l2] holds iff [l1] and [l2] have no elements + in common. *) + +Definition list_disjoint (A: Set) (l1 l2: list A) : Prop := + forall (x y: A), In x l1 -> In y l2 -> x <> y. + +Lemma list_disjoint_cons_left: + forall (A: Set) (a: A) (l1 l2: list A), + list_disjoint (a :: l1) l2 -> list_disjoint l1 l2. +Proof. + unfold list_disjoint; simpl; intros. apply H; tauto. +Qed. + +Lemma list_disjoint_cons_right: + forall (A: Set) (a: A) (l1 l2: list A), + list_disjoint l1 (a :: l2) -> list_disjoint l1 l2. +Proof. + unfold list_disjoint; simpl; intros. apply H; tauto. +Qed. + +Lemma list_disjoint_notin: + forall (A: Set) (l1 l2: list A) (a: A), + list_disjoint l1 l2 -> In a l1 -> ~(In a l2). +Proof. + unfold list_disjoint; intros; red; intros. + apply H with a a; auto. +Qed. + +Lemma list_disjoint_sym: + forall (A: Set) (l1 l2: list A), + list_disjoint l1 l2 -> list_disjoint l2 l1. +Proof. + unfold list_disjoint; intros. + apply sym_not_equal. apply H; auto. +Qed. + +(** [list_norepet l] holds iff the list [l] contains no repetitions, + i.e. no element occurs twice. *) + +Inductive list_norepet (A: Set) : list A -> Prop := + | list_norepet_nil: + list_norepet nil + | list_norepet_cons: + forall hd tl, + ~(In hd tl) -> list_norepet tl -> list_norepet (hd :: tl). + +Lemma list_norepet_dec: + forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A), + {list_norepet l} + {~list_norepet l}. +Proof. + induction l. + left; constructor. + destruct IHl. + case (In_dec eqA_dec a l); intro. + right. red; intro. inversion H. contradiction. + left. constructor; auto. + right. red; intro. inversion H. contradiction. +Qed. + +Lemma list_map_norepet: + forall (A B: Set) (f: A -> B) (l: list A), + list_norepet l -> + (forall x y, In x l -> In y l -> x <> y -> f x <> f y) -> + list_norepet (List.map f l). +Proof. + induction 1; simpl; intros. + constructor. + constructor. + red; intro. generalize (list_in_map_inv f _ _ H2). + intros [x [EQ IN]]. generalize EQ. change (f hd <> f x). + apply H1. tauto. tauto. + red; intro; subst x. contradiction. + apply IHlist_norepet. intros. apply H1. tauto. tauto. auto. +Qed. + +Remark list_norepet_append_commut: + forall (A: Set) (a b: list A), + list_norepet (a ++ b) -> list_norepet (b ++ a). +Proof. + intro A. + assert (forall (x: A) (b: list A) (a: list A), + list_norepet (a ++ b) -> ~(In x a) -> ~(In x b) -> + list_norepet (a ++ x :: b)). + induction a; simpl; intros. + constructor; auto. + inversion H. constructor. red; intro. + elim (in_app_or _ _ _ H6); intro. + elim H4. apply in_or_app. tauto. + elim H7; intro. subst a. elim H0. left. auto. + elim H4. apply in_or_app. tauto. + auto. + induction a; simpl; intros. + rewrite <- app_nil_end. auto. + inversion H0. apply H. auto. + red; intro; elim H3. apply in_or_app. tauto. + red; intro; elim H3. apply in_or_app. tauto. +Qed. + +Lemma list_norepet_append: + forall (A: Set) (l1 l2: list A), + list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 -> + list_norepet (l1 ++ l2). +Proof. + induction l1; simpl; intros. + auto. + inversion H. subst hd tl. + constructor. red; intro. apply (H1 a a). auto with coqlib. + elim (in_app_or _ _ _ H2); tauto. auto. + apply IHl1. auto. auto. + red; intros; apply H1; auto with coqlib. +Qed. + +Lemma list_norepet_append_right: + forall (A: Set) (l1 l2: list A), + list_norepet (l1 ++ l2) -> list_norepet l2. +Proof. + induction l1; intros. + assumption. + simpl in H. inversion H. eauto. +Qed. + +Lemma list_norepet_append_left: + forall (A: Set) (l1 l2: list A), + list_norepet (l1 ++ l2) -> list_norepet l1. +Proof. + intros. apply list_norepet_append_right with l2. + apply list_norepet_append_commut. auto. +Qed. + +(** [list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and + [P xi yi] holds for all [i]. *) + +Section FORALL2. + +Variable A: Set. +Variable B: Set. +Variable P: A -> B -> Prop. + +Inductive list_forall2: list A -> list B -> Prop := + | list_forall2_nil: + list_forall2 nil nil + | list_forall2_cons: + forall a1 al b1 bl, + P a1 b1 -> + list_forall2 al bl -> + list_forall2 (a1 :: al) (b1 :: bl). + +End FORALL2. + +Lemma list_forall2_imply: + forall (A B: Set) (P1: A -> B -> Prop) (l1: list A) (l2: list B), + list_forall2 P1 l1 l2 -> + forall (P2: A -> B -> Prop), + (forall v1 v2, In v1 l1 -> In v2 l2 -> P1 v1 v2 -> P2 v1 v2) -> + list_forall2 P2 l1 l2. +Proof. + induction 1; intros. + constructor. + constructor. auto with coqlib. apply IHlist_forall2; auto. + intros. auto with coqlib. +Qed. |