Library Coqlib

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 Znumtheory.

Require Export List.

Require Export Bool.

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: Type) (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 inv H := inversion H; clear H; subst.




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

  | [ |- _ = _ ] => f_equal

  | [ |- (?X ?A <> ?X ?B) ] =>

      cut (A <> B); [intro; congruence | try discriminate]

  end.




Ltac byContradiction :=

  cut False; [contradiction|idtac].




Ltac omegaContradiction :=

  cut False; [contradiction|omega].




Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.






Ltac exploit x :=

    refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _ _) _)

 || refine (modusponens _ _ (x _ _ _) _)

 || refine (modusponens _ _ (x _ _) _)

 || refine (modusponens _ _ (x _) _).

Definitions and theorems over the type `positive`





Definition peq (x y: positive): {x = y} + {x <> y}.






Lemma peq_true:

  forall (A: Type) (x: positive) (a b: A), (if peq x x then a else b) = a.






Lemma peq_false:

  forall (A: Type) (x y: positive) (a b: A), x <> y -> (if peq x y then a else b) = b.






Definition Plt (x y: positive): Prop := Zlt (Zpos x) (Zpos y).




Lemma Plt_ne:

  forall (x y: positive), Plt x y -> x <> y.



Hint Resolve Plt_ne: coqlib.




Lemma Plt_trans:

  forall (x y z: positive), Plt x y -> Plt y z -> Plt x z.






Remark Psucc_Zsucc:

  forall (x: positive), Zpos (Psucc x) = Zsucc (Zpos x).






Lemma Plt_succ:

  forall (x: positive), Plt x (Psucc x).



Hint Resolve Plt_succ: coqlib.




Lemma Plt_trans_succ:

  forall (x y: positive), Plt x y -> Plt x (Psucc y).



Hint Resolve Plt_succ: coqlib.




Lemma Plt_succ_inv:

  forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y.






Definition plt (x y: positive) : {Plt x y} + {~ Plt x y}.






Definition Ple (p q: positive) := Zle (Zpos p) (Zpos q).




Lemma Ple_refl: forall (p: positive), Ple p p.






Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r.






Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q.






Lemma Ple_succ: forall (p: positive), Ple p (Psucc p).






Lemma Plt_Ple_trans:

  forall (p q r: positive), Plt p q -> Ple q r -> Plt p r.






Lemma Plt_strict: forall p, ~ Plt p p.






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.






Variable A: Type.

Variable v1: A.

Variable f: positive -> A -> A.




Lemma Ppred_Plt:

  forall x, x <> xH -> Plt (Ppred x) x.






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).






Lemma positive_rec_base:

  positive_rec 1%positive = v1.






Lemma positive_rec_succ:

  forall x, positive_rec (Psucc x) = f x (positive_rec x).






Lemma positive_Peano_ind:

  forall (P: positive -> Prop),

  P xH ->

  (forall x, P x -> P (Psucc x)) ->

  forall x, P x.






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: Type) (x: Z) (a b: A), (if zeq x x then a else b) = a.






Lemma zeq_false:

  forall (A: Type) (x y: Z) (a b: A), x <> y -> (if zeq x y then a else b) = b.






Open Scope Z_scope.




Definition zlt: forall (x y: Z), {x < y} + {x >= y} := Z_lt_ge_dec.




Lemma zlt_true:

  forall (A: Type) (x y: Z) (a b: A), 

  x < y -> (if zlt x y then a else b) = a.






Lemma zlt_false:

  forall (A: Type) (x y: Z) (a b: A), 

  x >= y -> (if zlt x y then a else b) = b.






Definition zle: forall (x y: Z), {x <= y} + {x > y} := Z_le_gt_dec.




Lemma zle_true:

  forall (A: Type) (x y: Z) (a b: A), 

  x <= y -> (if zle x y then a else b) = a.






Lemma zle_false:

  forall (A: Type) (x y: Z) (a b: A), 

  x > y -> (if zle x y then a else b) = b.

Properties of powers of two.





Lemma two_power_nat_O : two_power_nat O = 1.






Lemma two_power_nat_pos : forall n : nat, two_power_nat n > 0.






Lemma two_power_nat_two_p:

  forall x, two_power_nat x = two_p (Z_of_nat x).






Lemma two_p_monotone:

  forall x y, 0 <= x <= y -> two_p x <= two_p y.






Lemma two_p_monotone_strict:

  forall x y, 0 <= x < y -> two_p x < two_p y.






Lemma two_p_strict:

  forall x, x >= 0 -> x < two_p x.






Lemma two_p_strict_2:

  forall x, x >= 0 -> 2 * x - 1 < two_p x.

Properties of Zmin and Zmax





Lemma Zmin_spec:

  forall x y, Zmin x y = if zlt x y then x else y.






Lemma Zmax_spec:

  forall x y, Zmax x y = if zlt y x then x else y.






Lemma Zmax_bound_l:

  forall x y z, x <= y -> x <= Zmax y z.



Lemma Zmax_bound_r:

  forall x y z, x <= z -> x <= Zmax y z.

Properties of Euclidean division and modulus.





Lemma Zdiv_small:

  forall x y, 0 <= x < y -> x / y = 0.






Lemma Zmod_small:

  forall x y, 0 <= x < y -> x mod y = x.






Lemma Zmod_unique:

  forall x y a b,

  x = a * y + b -> 0 <= b < y -> x mod y = b.






Lemma Zdiv_unique:

  forall x y a b,

  x = a * y + b -> 0 <= b < y -> x / y = a.






Lemma Zdiv_Zdiv:

  forall a b c,

  b > 0 -> c > 0 -> (a / b) / c = a / (b * c).






Lemma Zmult_le_compat_l_neg :

  forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m.






Lemma Zdiv_interval_1:

  forall lo hi a b,

  lo <= 0 -> hi > 0 -> b > 0 ->

  lo * b <= a < hi * b ->

  lo <= a/b < hi.






Lemma Zdiv_interval_2:

  forall lo hi a b,

  lo <= a <= hi -> lo <= 0 -> hi >= 0 -> b > 0 ->

  lo <= a/b <= hi.

Properties of divisibility.





Lemma Zdivides_trans:

  forall x y z, (x | y) -> (y | z) -> (x | z).






Definition Zdivide_dec:

  forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.

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.






Lemma align_divides: forall x y, y > 0 -> (y | align x y).

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: Type) (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: Type) (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: Type) (n: nat) (l: list A) (x: A),

  List.nth_error l n = Some x -> In x l.



Hint Resolve nth_error_in: coqlib.




Lemma nth_error_nil:

  forall (A: Type) (idx: nat), nth_error (@nil A) idx = None.



Hint Resolve nth_error_nil: coqlib.

Compute the length of a list, with result in Z.





Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z :=

  match l with

  | nil => acc

  | hd :: tl => list_length_z_aux tl (Zsucc acc)

  end.




Remark list_length_z_aux_shift:

  forall (A: Type) (l: list A) n m,

  list_length_z_aux l n = list_length_z_aux l m + (n - m).






Definition list_length_z (A: Type) (l: list A) : Z :=

  list_length_z_aux l 0.




Lemma list_length_z_cons:

  forall (A: Type) (hd: A) (tl: list A),

  list_length_z (hd :: tl) = list_length_z tl + 1.






Lemma list_length_z_pos:

  forall (A: Type) (l: list A),

  list_length_z l >= 0.






Lemma list_length_z_map:

  forall (A B: Type) (f: A -> B) (l: list A),

  list_length_z (map f l) = list_length_z l.

Extract the n-th element of a list, as List.nth_error does, but the index n is of type Z.





Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A :=

  match l with

  | nil => None

  | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n)

  end.




Lemma list_nth_z_in:

  forall (A: Type) (l: list A) n x,

  list_nth_z l n = Some x -> In x l.






Lemma list_nth_z_map:

  forall (A B: Type) (f: A -> B) (l: list A) n,

  list_nth_z (List.map f l) n = option_map f (list_nth_z l n).






Lemma list_nth_z_range:

  forall (A: Type) (l: list A) n x,

  list_nth_z l n = Some x -> 0 <= n < list_length_z l.

Properties of List.incl (list inclusion).





Lemma incl_cons_inv:

  forall (A: Type) (a: A) (b c: list A),

  incl (a :: b) c -> incl b c.



Hint Resolve incl_cons_inv: coqlib.




Lemma incl_app_inv_l:

  forall (A: Type) (l1 l2 m: list A),

  incl (l1 ++ l2) m -> incl l1 m.






Lemma incl_app_inv_r:

  forall (A: Type) (l1 l2 m: list A),

  incl (l1 ++ l2) m -> incl l2 m.






Hint Resolve  incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib.




Lemma incl_same_head:

  forall (A: Type) (x: A) (l1 l2: list A),

  incl l1 l2 -> incl (x::l1) (x::l2).

Properties of List.map (mapping a function over a list).





Lemma list_map_exten:

  forall (A B: Type) (f f': A -> B) (l: list A),

  (forall x, In x l -> f x = f' x) ->

  List.map f' l = List.map f l.






Lemma list_map_compose:

  forall (A B C: Type) (f: A -> B) (g: B -> C) (l: list A),

  List.map g (List.map f l) = List.map (fun x => g(f x)) l.






Lemma list_map_identity:

  forall (A: Type) (l: list A),

  List.map (fun (x:A) => x) l = l.






Lemma list_map_nth:

  forall (A B: Type) (f: A -> B) (l: list A) (n: nat),

  nth_error (List.map f l) n = option_map f (nth_error l n).






Lemma list_length_map:

  forall (A B: Type) (f: A -> B) (l: list A),

  List.length (List.map f l) = List.length l.






Lemma list_in_map_inv:

  forall (A B: Type) (f: A -> B) (l: list A) (y: B),

  In y (List.map f l) -> exists x:A, y = f x /\ In x l.






Lemma list_append_map:

  forall (A B: Type) (f: A -> B) (l1 l2: list A),

  List.map f (l1 ++ l2) = List.map f l1 ++ List.map f l2.

Properties of list membership.





Lemma in_cns:

  forall (A: Type) (x y: A) (l: list A), In x (y :: l) <-> y = x \/ In x l.






Lemma in_app:

  forall (A: Type) (x: A) (l1 l2: list A), In x (l1 ++ l2) <-> In x l1 \/ In x l2.






Lemma list_in_insert:

  forall (A: Type) (x: A) (l1 l2: list A) (y: A),

  In x (l1 ++ l2) -> In x (l1 ++ y :: l2).

list_disjoint l1 l2 holds iff l1 and l2 have no elements in common.





Definition list_disjoint (A: Type) (l1 l2: list A) : Prop :=

  forall (x y: A), In x l1 -> In y l2 -> x <> y.




Lemma list_disjoint_cons_left:

  forall (A: Type) (a: A) (l1 l2: list A),

  list_disjoint (a :: l1) l2 -> list_disjoint l1 l2.






Lemma list_disjoint_cons_right:

  forall (A: Type) (a: A) (l1 l2: list A),

  list_disjoint l1 (a :: l2) -> list_disjoint l1 l2.






Lemma list_disjoint_notin:

  forall (A: Type) (l1 l2: list A) (a: A),

  list_disjoint l1 l2 -> In a l1 -> ~(In a l2).






Lemma list_disjoint_sym:

  forall (A: Type) (l1 l2: list A),

  list_disjoint l1 l2 -> list_disjoint l2 l1.






Lemma list_disjoint_dec:

  forall (A: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A),

  {list_disjoint l1 l2} + {~list_disjoint l1 l2}.

list_equiv l1 l2 holds iff the lists l1 and l2 contain the same elements.





Definition list_equiv (A : Type) (l1 l2: list A) : Prop :=

  forall x, In x l1 <-> In x l2.

list_norepet l holds iff the list l contains no repetitions, i.e. no element occurs twice.





Inductive list_norepet (A: Type) : 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: Type) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l: list A),

  {list_norepet l} + {~list_norepet l}.






Lemma list_map_norepet:

  forall (A B: Type) (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).






Remark list_norepet_append_commut:

  forall (A: Type) (a b: list A),

  list_norepet (a ++ b) -> list_norepet (b ++ a).






Lemma list_norepet_app:

  forall (A: Type) (l1 l2: list A),

  list_norepet (l1 ++ l2) <->

  list_norepet l1 /\ list_norepet l2 /\ list_disjoint l1 l2.






Lemma list_norepet_append:

  forall (A: Type) (l1 l2: list A),

  list_norepet l1 -> list_norepet l2 -> list_disjoint l1 l2 ->

  list_norepet (l1 ++ l2).






Lemma list_norepet_append_right:

  forall (A: Type) (l1 l2: list A),

  list_norepet (l1 ++ l2) -> list_norepet l2.






Lemma list_norepet_append_left:

  forall (A: Type) (l1 l2: list A),

  list_norepet (l1 ++ l2) -> list_norepet l1.

is_tail l1 l2 holds iff l2 is of the form l ++ l1 for some l.





Inductive is_tail (A: Type): list A -> list A -> Prop :=

  | is_tail_refl:

      forall c, is_tail c c

  | is_tail_cons:

      forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).




Lemma is_tail_in:

  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.






Lemma is_tail_cons_left:

  forall (A: Type) (i: A) c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.






Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.




Lemma is_tail_incl:

  forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2.






Lemma is_tail_trans:

  forall (A: Type) (l1 l2: list A),

  is_tail l1 l2 -> forall (l3: list A), is_tail l2 l3 -> is_tail l1 l3.

list_forall2 P [x1 ... xN] [y1 ... yM] holds iff [N = M] and
  [P xi yi] holds for all [i].





Section FORALL2.




Variable A: Type.

Variable B: Type.

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: Type) (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.

Dropping the first N elements of a list.





Fixpoint list_drop (A: Type) (n: nat) (x: list A) {struct n} : list A :=

  match n with

  | O => x

  | S n' => match x with nil => nil | hd :: tl => list_drop n' tl end

  end.




Lemma list_drop_incl:

  forall (A: Type) (x: A) n (l: list A), In x (list_drop n l) -> In x l.






Lemma list_drop_norepet:

  forall (A: Type) n (l: list A), list_norepet l -> list_norepet (list_drop n l).






Lemma list_map_drop:

  forall (A B: Type) (f: A -> B) n (l: list A),

  list_drop n (map f l) = map f (list_drop n l).

Definitions and theorems over boolean types





Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool :=

  if a then true else false.




Implicit Arguments proj_sumbool [P Q].




Coercion proj_sumbool: sumbool >-> bool.




Lemma proj_sumbool_true:

  forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P.






Section DECIDABLE_EQUALITY.




Variable A: Type.

Variable dec_eq: forall (x y: A), {x=y} + {x<>y}.

Variable B: Type.




Lemma dec_eq_true:

  forall (x: A) (ifso ifnot: B),

  (if dec_eq x x then ifso else ifnot) = ifso.






Lemma dec_eq_false:

  forall (x y: A) (ifso ifnot: B),

  x <> y -> (if dec_eq x y then ifso else ifnot) = ifnot.






Lemma dec_eq_sym:

  forall (x y: A) (ifso ifnot: B),

  (if dec_eq x y then ifso else ifnot) =

  (if dec_eq y x then ifso else ifnot).






End DECIDABLE_EQUALITY.