Library Coqlib

Require Import Omega.
Require Export ZArith.
Require Export Znumtheory.
Require Export List.
Require Export Bool.
Require Import FunctionalExtensionality.

Lemma extensionality:
  forall (A B: Set) (f g : A -> B),
  (forall x, f x = g x) -> f = g.

Inductive OptionT (T : Type) : Type :=
    NoneT1 : OptionT T
  | SomeT1 : T -> OptionT T.

Inductive optionT (A : Type) : Type :=
  | SomeT : A -> optionT A
  | NoneT : optionT A.

Implicit Arguments SomeT [A].
Implicit Arguments NoneT [A].

Notation opt_predT :=
  (fun opt:optionT _ =>
    fun f =>
      match opt with
        | SomeT t => f t
        | NoneT => False
      end).

Notation optpT :=
  (fun f => fun opt:optionT _ =>
    match opt with
      | SomeT t => f t
      | NoneT => False
    end).

Notation optgT :=
  (fun f => fun opt:optionT _ =>
    fun t´ =>
      match opt with
        | SomeT t => f t t´
        | NoneT => False
      end).

Notation opt_predT2 :=
  (fun opt:optionT _ =>
    fun opt´:optionT _ =>
      fun f =>
        match opt, opt´ with
          | SomeT t, SomeT t´ => f t t´
          | _, _ => False
        end).

Inductive prodT (A : Set) (B : Type) : Type :=
    pairT : A -> B -> prodT A B.
Implicit Arguments pairT [A B].

Notation "( x , y , .. , z )" :=
  (pairT .. (pairT x y) .. z) : t_type_scope.

Ltac hypreplace H y :=
  let H´ := fresh in
    (assert (H´ := y); try (clear H; rename H´ into H)).

Ltac hypreplace2 H y Hn:=
  let H´ := fresh in
    (assert (H´ := y); try (clear H; rename H´ into Hn)).

Tactic Notation "substH" hyp (H) :=
  match goal with
    | |- ?a -> ?b => clear H; intro H
    | |- _ => fail 1 "goal must be 'A -> B'."
  end.

Tactic Notation "substH" hyp (H) "with" constr (t) :=
  hypreplace H t.

Tactic Notation "substH" hyp (H) "with" constr (t) "into" ident (Hn) :=
  hypreplace2 H t Hn.

Tactic Notation "bool_destruct" hyp (H) "as" simple_intropattern (pat) :=
  let H0 := fresh "H" in
    (rename H into H0;
    match type of (H0) with
      | (andb ?a ?b = true) =>
        destruct (andb_prop a b H0) as pat; clear H0
      | (orb ?a ?b = true) =>
        destruct (orb_prop a b H0) as pat; clear H0
      | _ => fail "not destructable"
    end).

Tactic Notation "destructH" hyp (H) "with" constr (t) :=
  destruct t; clear H.

Tactic Notation "destructH" hyp (H) "with" constr (t)
  "as" simple_intropattern (p) :=
  destruct t as p; clear H.

Tactic Notation "discri" :=
  match goal with
    | H : ?a <> ?a |- _ =>
      elimtype False; apply H; reflexivity
    | |- _ -> _ => intros; discriminate
    | H : False |- _ => destruct H
    | _ => discriminate
  end.

Tactic Notation "gen_clear" hyp (H) :=
  generalize H; clear H.

Tactic Notation "gen_clear" hyp (H1) hyp (H2) :=
  generalize H1 H2; clear H1 H2.

Tactic Notation "gen_clear"
  hyp (H1) hyp (H2) hyp (H3) :=
  generalize H1 H2 H3; clear H1 H2 H3.

Tactic Notation "gen_clear"
  hyp (H1) hyp (H2) hyp (H3) hyp (H4) :=
  generalize H1 H2 H3 H4;
    clear H1 H2 H3 H4.

Tactic Notation "gen_clear"
  hyp (H1) hyp (H2) hyp (H3)
  hyp (H4) hyp (H5):=
  generalize H1 H2 H3 H4 H5;
    clear H1 H2 H3 H4 H5.

Tactic Notation "gen_clear"
  hyp (H1) hyp (H2) hyp (H3)
  hyp (H4) hyp (H5) hyp (H6):=
  generalize H1 H2 H3 H4 H5 H6;
    clear H1 H2 H3 H4 H5 H6.

Tactic Notation "split_l" :=
  split; [trivial | idtac].

Tactic Notation "split_r" :=
  split; [idtac | trivial ].

Tactic Notation "split_lr" :=
  split; [trivial | trivial ].

Tactic Notation "split_l" "with" constr (t) :=
  split; [apply t | idtac].

Tactic Notation "split_r" "with" constr (t) :=
  split; [idtac | apply t ].

Tactic Notation "split_l" "by" tactic (tac) :=
  split; [tac | idtac ].

Tactic Notation "split_r" "by" tactic (tac) :=
  split; [idtac | tac ].

Tactic Notation "split_l_clear" "with" hyp (H) :=
  split; [apply H | clear H].

Tactic Notation "split_r_clear" "with" hyp (H) :=
  split; [clear H | apply H ].

Lemma and_sym : forall (A B : Prop), A /\ B -> B /\ A.
Implicit Arguments and_sym [A B].

Ltac rsplit := apply and_sym; split.

Lemma and_sym_rr : forall A B C : Prop, A /\ B /\ C -> B /\ C /\ A.

Ltac rrsplit := apply and_sym_rr; split.

Tactic Notation "inj_hyp" hyp (H) :=
  injection H; clear H; intro H.

Tactic Notation "rew_clear" hyp (H) :=
  rewrite H; clear H.

Tactic Notation "injection" hyp (H) :=
  injection H.

Tactic Notation "injection" hyp (H) "as"
  simple_intropattern (pat) :=
  injection H; intros pat.

Tactic Notation "injsubst" ident (id) "in" hyp (H) :=
  injection H; intro; subst id; clear H.

Ltac InvertAll :=
  repeat
    match goal with
      | H: _ /\ _ |- _ => inversion_clear H
      | H: ex _ |- _ => inversion_clear H
    end.

Ltac arith_replace t1 t2 :=
  (replace t1 with t2; fail "error") ||
    (replace t1 with t2; [trivial | try omega; fail "error" ]).

Ltac arith_replaceH H t1 t2 :=
  (replace t1 with t2 in H; fail "error") ||
    (replace t1 with t2 in H; [trivial | try omega; fail "error" ]).

Tactic Notation "arith_rep" constr(t1) "with" constr (t2) :=
  arith_replace t1 t2.

Tactic Notation "arith_rep" constr(t1) "with" constr (t2) "in" hyp (H):=
  arith_replaceH H t1 t2.

Ltac clearall :=
  match goal with
    | H : _ |- _ =>
      (clear H || (generalize H; clear H)); clearall
    | _ => intros
  end.

Ltac clearall_arith :=
  match goal with
    | H : ?a > ?b |- _ => (generalize H; clear H); clearall_arith
    | H : ?a >= ?b |- _ => (generalize H; clear H); clearall_arith
    | H : ?a < ?b |- _ => (generalize H; clear H); clearall_arith
    | H : ?a <= ?b |- _ => (generalize H; clear H); clearall_arith
    | H : ?a = ?b |- _ =>
      match type of a with
        | nat => (generalize H; clear H); clearall_arith
        | _ => (clear H || (generalize H; clear H)); clearall_arith
      end
    | H : _ |- _ =>
      (clear H || (generalize H; clear H)); clearall_arith
    | _ => intros
  end.

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 :=
  destruct name eqn:?.

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: forall (x y: positive), {x = y } + {x <> y } := Pos.eq_dec.
Global Opaque peq.

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: positive -> positive -> Prop := Pos.lt.

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.

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 }.
Global Opaque plt.

Definition Ple: positive -> positive -> Prop := Pos.le.

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.

Ltac xomega := unfold Plt, Ple in *; zify; omega.
Ltac xomegaContradiction := exfalso; xomega.

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

Lemma Zmod_recombine:
  forall x a b,
  a > 0 -> b > 0 ->
  x mod (a * b ) = ((x /b ) mod a ) * b + (x mod b ).

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 ) }.
Global Opaque Zdivide_dec.

Lemma Zdivide_interval:
  forall a b c,
  0 < c -> 0 <= a < b -> (c | a ) -> (c | b ) -> 0 <= a <= b - c.

Conversion from Z to nat.

Definition nat_of_Z: Z -> nat := Z.to_nat.

Lemma nat_of_Z_of_nat:
  forall n, nat_of_Z (Z_of_nat n) = n.

Lemma nat_of_Z_max:
  forall z, Z_of_nat (nat_of_Z z) = Zmax z 0.

Lemma nat_of_Z_eq:
  forall z, z >= 0 -> Z_of_nat (nat_of_Z z) = z.

Lemma nat_of_Z_neg:
  forall n, n <= 0 -> nat_of_Z n = O.

Lemma nat_of_Z_plus:
  forall p q,
  p >= 0 -> q >= 0 ->
  nat_of_Z (p + q) = (nat_of_Z p + nat_of_Z q)%nat.

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.

Comparing option types.

Definition option_eq (A: Type) (eqA: forall (x y: A), {x =y } + {x <>y }):
forall (x y: option A), {x =y } + {x <>y }.
Global Opaque option_eq.

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.

Lemma list_append_map_inv:
  forall (A B: Type) (f: A -> B) (m1 m2: list B) (l: list A),
  List.map f l = m1 ++ m2 ->
  exists l1, exists l2, List.map f l1 = m1 /\ List.map f l2 = m2 /\ l = l1 ++ l2.

Folding a function over a list

Section LIST_FOLD.

Variables A B: Type.
Variable f: A -> B -> B.

This is exactly List.fold_left from Coq's standard library, with f taking arguments in a different order.

Fixpoint list_fold_left (accu: B) (l: list A) : B :=
match l with nil => accu | x :: l´ => list_fold_left (f x accu) l´ end.

This is exactly List.fold_right from Coq's standard library, except that it runs in constant stack space.

Definition list_fold_right (l: list A) (base: B) : B :=
  list_fold_left base (List.rev´ l).

Remark list_fold_left_app:
  forall l1 l2 accu,
  list_fold_left accu (l1 ++ l2) = list_fold_left (list_fold_left accu l1) l2.

Lemma list_fold_right_eq:
  forall l base,
  list_fold_right l base =
  match l with nil => base | x :: l´ => f x (list_fold_right l´ base) end.

Lemma list_fold_right_spec:
  forall l base, list_fold_right l base = List.fold_right f base l.

End LIST_FOLD.

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_l:
  forall (A: Type) (a: A) (l1 l2: list A),
  list_disjoint l1 l2 -> ~In a l2 -> list_disjoint (a :: l1) l2.

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

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

Lemma list_forall2_app:
  forall a2 b2 a1 b1,
  list_forall2 a1 b1 -> list_forall2 a2 b2 ->
  list_forall2 (a1 ++ a2) (b1 ++ b2).

Lemma list_forall2_length:
  forall l1 l2,
  list_forall2 l1 l2 -> length l1 = length l2.

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

A list of n elements, all equal to x.

Fixpoint list_repeat {A: Type} (n: nat) (x: A) {struct n} :=
  match n with
  | O => nil
  | S m => x :: list_repeat m x
  end.

Lemma length_list_repeat:
  forall (A: Type) n (x: A), length (list_repeat n x) = n.

Lemma in_list_repeat:
  forall (A: Type) n (x: A) y, In y (list_repeat n x) -> y = x.

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.

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

Ltac InvBooleans :=
  match goal with
  | [ H: _ && _ = true |- _ ] =>
      destruct (andb_prop _ _ H); clear H; InvBooleans
  | [ H: _ || _ = false |- _ ] =>
      destruct (orb_false_elim _ _ H); clear H; InvBooleans
  | [ H: proj_sumbool ?x = true |- _ ] =>
      generalize (proj_sumbool_true _ H); clear H; intro; InvBooleans
  | _ => idtac
  end.

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.

Section DECIDABLE_PREDICATE.

Variable P: Prop.
Variable dec: {P } + {~P }.
Variable A: Type.

Lemma pred_dec_true:
  forall (a b: A), P -> (if dec then a else b ) = a.

Lemma pred_dec_false:
  forall (a b: A), ~P -> (if dec then a else b ) = b.

End DECIDABLE_PREDICATE.

Well-founded orderings

Require Import Relations.

A non-dependent version of lexicographic ordering.

Section LEX_ORDER.

Variable A: Type.
Variable B: Type.
Variable ordA: A -> A -> Prop.
Variable ordB: B -> B -> Prop.

Inductive lex_ord: A *B -> A *B -> Prop :=
  | lex_ord_left: forall a1 b1 a2 b2,
      ordA a1 a2 -> lex_ord (a1 ,b1 ) (a2 ,b2 )
  | lex_ord_right: forall a b1 b2,
      ordB b1 b2 -> lex_ord (a ,b1 ) (a ,b2 ).

Lemma wf_lex_ord:
  well_founded ordA -> well_founded ordB -> well_founded lex_ord.

Lemma transitive_lex_ord:
  transitive _ ordA -> transitive _ ordB -> transitive _ lex_ord.

End LEX_ORDER.