Library ListFacts

Assorted facts about lists.

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.