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

Proof. auto. Qed.




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

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_identity:

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

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

Proof.

  induction l; simpl; congruence.

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.

Properties of list membership.





Lemma in_cns:

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

Proof.

  intros. simpl. tauto.

Qed.




Lemma in_app:

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

Proof.

  intros. split; intro. apply in_app_or. auto. apply in_or_app. auto.

Qed.




Lemma list_in_insert:

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

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

Proof.

  intros. apply in_or_app; simpl. elim (in_app_or _ _ _ H); intro; 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.




Lemma list_disjoint_dec:

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

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

Proof.

  induction l1; intros.

  left; red; intros. elim H.

  case (In_dec eqA_dec a l2); intro.

  right; red; intro. apply (H a a); auto with coqlib.

  case (IHl1 l2); intro.

  left; red; intros. elim H; intro.

    red; intro; subst a y. contradiction.

    apply l; auto.

  right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto.

Defined.

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.

Defined.




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_app:

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

  list_norepet (l1 ++ l2) <->

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

Proof.

  induction l1; simpl; intros; split; intros.

  intuition. constructor. red;simpl;auto.

  tauto.

  inversion H; subst. rewrite IHl1 in H3. rewrite in_app in H2.

  intuition.

  constructor; auto. red; intros. elim H2; intro. congruence. auto.

  destruct H as [B [C D]]. inversion B; subst.

  constructor. rewrite in_app. intuition. elim (D a a); auto. apply in_eq.

  rewrite IHl1. intuition. red; intros. apply D; auto. apply in_cons; auto.

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.

  generalize list_norepet_app; firstorder.

Qed.




Lemma list_norepet_append_right:

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

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

Proof.

  generalize list_norepet_app; firstorder.

Qed.




Lemma list_norepet_append_left:

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

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

Proof.

  generalize list_norepet_app; firstorder.

Qed.

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





Inductive is_tail (A: Set): 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: Set) (i: A) c1 c2, is_tail (i :: c1) c2 -> In i c2.

Proof.

  induction c2; simpl; intros.

  inversion H.

  inversion H. tauto. right; auto.

Qed.




Lemma is_tail_cons_left:

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

Proof.

  induction c2; intros; inversion H.

  constructor. constructor. constructor. auto.

Qed.




Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib.




Lemma is_tail_incl:

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

Proof.

  induction 1; eauto with coqlib.

Qed.




Lemma is_tail_trans:

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

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

Proof.

  induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto.

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.

Dropping the first or first two elements of a list.





Definition list_drop1 (A: Set) (x: list A) :=

  match x with nil => nil | hd :: tl => tl end.

Definition list_drop2 (A: Set) (x: list A) :=

  match x with nil => nil | hd :: nil => nil | hd1 :: hd2 :: tl => tl end.




Lemma list_drop1_incl:

  forall (A: Set) (x: A) (l: list A), In x (list_drop1 l) -> In x l.

Proof.

  intros. destruct l. elim H. simpl in H. auto with coqlib.

Qed.




Lemma list_drop2_incl:

  forall (A: Set) (x: A) (l: list A), In x (list_drop2 l) -> In x l.

Proof.

  intros. destruct l. elim H. destruct l. elim H.

  simpl in H. auto with coqlib.

Qed.




Lemma list_drop1_norepet:

  forall (A: Set) (l: list A), list_norepet l -> list_norepet (list_drop1 l).

Proof.

  intros. destruct l; simpl. constructor. inversion H. auto.

Qed.




Lemma list_drop2_norepet:

  forall (A: Set) (l: list A), list_norepet l -> list_norepet (list_drop2 l).

Proof.

  intros. destruct l; simpl. constructor.

  destruct l; simpl. constructor. inversion H. inversion H3. auto.

Qed.




Lemma list_map_drop1:

  forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l).

Proof.

  intros; destruct l; reflexivity.

Qed.




Lemma list_map_drop2:

  forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l).

Proof.

  intros; destruct l. reflexivity. destruct l; reflexivity.

Qed.

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.

Proof.

  intros P Q a. destruct a; simpl. auto. congruence.

Qed.




Section DECIDABLE_EQUALITY.




Variable A: Set.

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

Variable B: Set.




Lemma dec_eq_true:

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

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

Proof.

  intros. destruct (dec_eq x x). auto. congruence.

Qed.




Lemma dec_eq_false:

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

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

Proof.

  intros. destruct (dec_eq x y). congruence. auto.

Qed.




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

Proof.

  intros. destruct (dec_eq x y).

  subst y. rewrite dec_eq_true. auto.

  rewrite dec_eq_false; auto.

Qed.




End DECIDABLE_EQUALITY.