Library ListFacts

``` ```

Author: Brian Aydemir.

Implicit arguments are declared by default in this library.
``` Require Import Eqdep_dec. Require Import List. Require Import Omega. Require Import SetoidList. Require Import Sorting. Require Import Relations. ```

Assorted facts.

``` Lemma app_head_eq_nil : forall (A : Type) (xs ys : list A),   ys = xs ++ ys ->   xs = nil. Lemma app_inj_head : forall (A : Type) (xs xs' ys : list A),   xs ++ ys = xs' ++ ys ->   xs = xs'. ```

List membership

``` Lemma not_in_cons :   forall (A : Type) (ys : list A) x y,   x <> y -> ~ In x ys -> ~ In x (y :: ys). Lemma not_In_app :   forall (A : Type) (xs ys : list A) x,   ~ In x xs -> ~ In x ys -> ~ In x (xs ++ ys). Lemma elim_not_In_cons :   forall (A : Type) (y : A) (ys : list A) (x : A),   ~ In x (y :: ys) -> x <> y /\ ~ In x ys. Lemma elim_not_In_app :   forall (A : Type) (xs ys : list A) (x : A),   ~ In x (xs ++ ys) -> ~ In x xs /\ ~ In x ys. ```

List inclusion

``` Lemma incl_nil :   forall (A : Type) (xs : list A), incl nil xs. Lemma incl_trans :   forall (A : Type) (xs ys zs : list A),   incl xs ys -> incl ys zs -> incl xs zs. Lemma In_incl :   forall (A : Type) (x : A) (ys zs : list A),   In x ys -> incl ys zs -> In x zs. Lemma elim_incl_cons :   forall (A : Type) (x : A) (xs zs : list A),   incl (x :: xs) zs -> In x zs /\ incl xs zs. Lemma elim_incl_app :   forall (A : Type) (xs ys zs : list A),   incl (xs ++ ys) zs -> incl xs zs /\ incl ys zs. ```

Setoid facts

``` Lemma InA_iff_In :   forall (A : Set) x xs, InA (@eq A) x xs <-> In x xs. ```

Equality proofs for lists

``` Section EqRectList. Variable A : Type. Variable eq_A_dec : forall (x y : A), {x = y} + {x <> y}. Lemma eq_rect_eq_list :   forall (p : list A) (Q : list A -> Type) (x : Q p) (h : p = p),   eq_rect p Q x p h = x. End EqRectList. ```

Decidable sorting and uniqueness of proofs

``` Section DecidableSorting. Variable A : Set. Variable leA : relation A. Hypothesis leA_dec : forall x y, {leA x y} + {~ leA x y}. Theorem lelistA_dec :   forall a xs, {lelistA leA a xs} + {~ lelistA leA a xs}. Theorem sort_dec :   forall xs, {sort leA xs} + {~ sort leA xs}. Section UniqueSortingProofs.   Hypothesis eq_A_dec : forall (x y : A), {x = y} + {x <> y}.   Hypothesis leA_unique : forall (x y : A) (p q : leA x y), p = q.   Scheme lelistA_ind' := Induction for lelistA Sort Prop.   Scheme sort_ind' := Induction for sort Sort Prop.   Theorem lelistA_unique :     forall (x : A) (xs : list A) (p q : lelistA leA x xs), p = q.   Theorem sort_unique :     forall (xs : list A) (p q : sort leA xs), p = q. End UniqueSortingProofs. End DecidableSorting. ```

Equality on sorted lists

``` Section Equality_ext. Variable A : Set. Variable ltA : relation A. Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z. Hypothesis ltA_not_eqA : forall x y, ltA x y -> x <> y. Hypothesis ltA_eqA : forall x y z, ltA x y -> y = z -> ltA x z. Hypothesis eqA_ltA : forall x y z, x = y -> ltA y z -> ltA x z. Hint Resolve ltA_trans. Hint Immediate ltA_eqA eqA_ltA. Notation Inf := (lelistA ltA). Notation Sort := (sort ltA). Lemma not_InA_if_Sort_Inf :   forall xs a, Sort xs -> Inf a xs -> ~ InA (@eq A) a xs. Lemma Sort_eq_head :   forall x xs y ys,   Sort (x :: xs) ->   Sort (y :: ys) ->   (forall a, InA (@eq A) a (x :: xs) <-> InA (@eq A) a (y :: ys)) ->   x = y. Lemma Sort_InA_eq_ext :   forall xs ys,   Sort xs ->   Sort ys ->   (forall a, InA (@eq A) a xs <-> InA (@eq A) a ys) ->   xs = ys. End Equality_ext. ```