Top.Util.ListFacts

Assorted facts about lists.

Author: Brian Aydemir.

Implicit arguments are declared by default in this library.

List membership

Lemma not_in_cons :
  ∀ (A : Type) (ys : list A) x y,
  x ≠ y → ¬ In x ys → ¬ In x (y :: ys).

Lemma not_In_app :
  ∀ (A : Type) (xs ys : list A) x,
  ¬ In x xs → ¬ In x ys → ¬ In x (xs ++ ys).

Lemma elim_not_In_cons :
  ∀ (A : Type) (y : A) (ys : list A) (x : A),
  ¬ In x (y :: ys) → x ≠ y ∧ ¬ In x ys.

Lemma elim_not_In_app :
  ∀ (A : Type) (xs ys : list A) (x : A),
  ¬ In x (xs ++ ys) → ¬ In x xs ∧ ¬ In x ys.

List inclusion

Lemma incl_nil :
  ∀ (A : Type) (xs : list A), incl nil xs.

Lemma incl_trans :
  ∀ (A : Type) (xs ys zs : list A),
  incl xs ys → incl ys zs → incl xs zs.

Lemma In_incl :
  ∀ (A : Type) (x : A) (ys zs : list A),
  In x ys → incl ys zs → In x zs.

Lemma elim_incl_cons :
  ∀ (A : Type) (x : A) (xs zs : list A),
  incl (x :: xs) zs → In x zs ∧ incl xs zs.

Lemma elim_incl_app :
  ∀ (A : Type) (xs ys zs : list A),
  incl (xs ++ ys) zs → incl xs zs ∧ incl ys zs.

Setoid facts

Lemma InA_iff_In :
  ∀ (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 : ∀ (x y : A), {x = y} + {x ≠ y}.

Lemma eq_rect_eq_list :
  ∀ (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 : ∀ x y, {leA x y} + {¬ leA x y}.

Theorem lelistA_dec :
  ∀ a xs, {lelistA leA a xs} + {¬ lelistA leA a xs}.

Theorem sort_dec :
  ∀ xs, {sort leA xs} + {¬ sort leA xs}.

Section UniqueSortingProofs.

  Hypothesis eq_A_dec : ∀ (x y : A), {x = y} + {x ≠ y}.
  Hypothesis leA_unique : ∀ (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 :
    ∀ (x : A) (xs : list A) (p q : lelistA leA x xs), p = q.

  Theorem sort_unique :
    ∀ (xs : list A) (p q : sort leA xs), p = q.

End UniqueSortingProofs.
End DecidableSorting.

Equality on sorted lists

Section Equality_ext.

Variable A : Type.
Variable ltA : relation A.
Hypothesis ltA_trans : ∀ x y z, ltA x y → ltA y z → ltA x z.
Hypothesis ltA_not_eqA : ∀ x y, ltA x y → x ≠ y.
Hypothesis ltA_eqA : ∀ x y z, ltA x y → y = z → ltA x z.
Hypothesis eqA_ltA : ∀ x y z, x = y → ltA y z → ltA x z.


Notation Inf := (lelistA ltA).
Notation Sort := (sort ltA).

Lemma strictorder_irrel :
  ∀ a, (complement ltA) a a.

Instance strictorder_ltA : StrictOrder ltA :=
{
   StrictOrder_Irreflexive := strictorder_irrel;
   StrictOrder_Transitive := ltA_trans
}.

Lemma not_InA_if_Sort_Inf :
  ∀ xs a, Sort xs → Inf a xs → ¬ InA (@eq A) a xs.

Lemma Sort_eq_head :
  ∀ x xs y ys,
  Sort (x :: xs) →
  Sort (y :: ys) →
  (∀ a, InA (@eq A) a (x :: xs) ↔ InA (@eq A) a (y :: ys)) →
  x = y.

Lemma Sort_InA_eq_ext :
  ∀ xs ys,
  Sort xs →
  Sort ys →
  (∀ a, InA (@eq A) a xs ↔ InA (@eq A) a ys) →
  xs = ys.

End Equality_ext.