Library Asm.Util.Coqlib

This code is written by Xavier Leroy as part of the Compcert project: http://pauillac.inria.fr/~xleroy/compcert-backend/

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

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

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

Lemma zeq_false:
  forall (A: Set) (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: Set) (x y: Z) (a b: A),
  x < y -> (if zlt x y then a else b) = a.

Lemma zlt_false:
  forall (A: Set) (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: Set) (x y: Z) (a b: A),
  x <= y -> (if zle x y then a else b) = a.

Lemma zle_false:
  forall (A: Set) (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.

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.

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.

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.
Hint Resolve nth_error_in: coqlib.

Lemma nth_error_nil:
  forall (A: Set) (idx: nat), nth_error (@nil A) idx = None.
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.
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.

Lemma incl_app_inv_r:
  forall (A: Set) (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: Set) (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: 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.

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.

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

Lemma list_length_map:
  forall (A B: Set) (f: A -> B) (l: list A),
  List.length (List.map f l) = List.length l.

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.

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.

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.

Lemma list_disjoint_cons_right:
  forall (A: Set) (a: A) (l1 l2: list A),
  list_disjoint l1 (a :: l2) -> list_disjoint l1 l2.

Lemma list_disjoint_notin:
  forall (A: Set) (l1 l2: list A) (a: A),
  list_disjoint l1 l2 -> In a l1 -> ~(In a l2).

Lemma list_disjoint_sym:
  forall (A: Set) (l1 l2: list A),
  list_disjoint l1 l2 -> list_disjoint l2 l1.

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

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

Remark list_norepet_append_commut:
  forall (A: Set) (a b: list A),
  list_norepet (a ++ b) -> list_norepet (b ++ a).

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

Lemma list_norepet_append_right:
  forall (A: Set) (l1 l2: list A),
  list_norepet (l1 ++ l2) -> list_norepet l2.

Lemma list_norepet_append_left:
  forall (A: Set) (l1 l2: list A),
  list_norepet (l1 ++ l2) -> list_norepet l1.

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.

Index
This page has been generated by coqdoc