Library ListFacts

Assorted facts about lists.

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.

Require Import AdditionalTactics.

Open Scope list_scope.

List structure


Lemma cons_eq_app : forall (A : Type) (z : A) (xs ys zs : list A),
  z :: zs = xs ++ ys ->
  (exists qs, xs = z :: qs /\ zs = qs ++ ys) \/
  (xs = nil /\ ys = z :: zs).

Lemma app_eq_cons : forall (A : Type) (z : A) (xs ys zs : list A),
  xs ++ ys = z :: zs ->
  (exists qs, xs = z :: qs /\ zs = qs ++ ys) \/
  (xs = nil /\ ys = z :: zs).

Lemma nil_eq_app : forall (A : Type) (xs ys : list A),
  nil = xs ++ ys ->
  xs = nil /\ ys = nil.

Lemma nil_neq_cons_app : forall (A : Type) (y : A) (xs ys : list A),
  nil <> xs ++ y :: ys.

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 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 : A) (xs : list A),
  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.

This page has been generated by coqdoc