Library CoqListFacts
Assorted facts about lists.
Require Import Coq.Lists.List.
Require Import Coq.Lists.SetoidList.
Require Import CoqUniquenessTac.
Open Scope list_scope.
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 app_cons_not_nil : forall (A : Type) (y : A) (xs ys : list A),
xs ++ y :: ys <> nil.
Lemma In_map : forall (A B : Type) (xs : list A) (x : A) (f : A -> B),
In x xs ->
In (f x) (map f xs).
Lemma not_In_cons : forall (A : Type) (ys : list A) (x y : A),
x <> y ->
~ In x ys ->
~ In x (y :: ys).
Lemma not_In_app : forall (A : Type) (xs ys : list A) (x : A),
~ 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.
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.
InA and In are related when the relation is eq. The lemma
In_InA, the converse of InA_In, is in Coq's standard
library.
Lemma InA_In : forall (A : Type) (x : A) (xs : list A),
InA (@eq _) x xs -> In x xs.
Lemma InA_iff_In : forall (A : Type) (x : A) (xs : list A),
InA (@eq _) x xs <-> In x xs.
Whether a list is sorted is a decidable proposition.
Section DecidableSorting.
Variable A : Type.
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}.
End DecidableSorting.
Two sorted lists with the same elements are equal to each other.
Section SortedListEquality.
Variable A : Type.
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 eqlist_eq : forall (xs ys : list A),
eqlistA (@eq _) xs ys ->
xs = ys.
Lemma Sort_InA_eq : forall xs ys,
Sort xs ->
Sort ys ->
(forall a, InA (@eq _) a xs <-> InA (@eq _) a ys) ->
xs = ys.
Lemma Sort_In_eq : forall xs ys,
Sort xs ->
Sort ys ->
(forall a, In a xs <-> In a ys) ->
xs = ys.
End SortedListEquality.
Uniqueness of proofs for predicates on lists often comes up when
discussing extensional equality on finite sets, as implemented by
the FSets library.
Section Uniqueness_Of_SetoidList_Proofs.
Variable A : Type.
Variable R : A -> A -> Prop.
Hypothesis R_unique : forall (x y : A) (p q : R x y), p = q.
Hypothesis list_eq_dec : forall (xs ys : list A), {xs = ys} + {xs <> ys}.
Scheme lelistA_ind' := Induction for lelistA Sort Prop.
Scheme sort_ind' := Induction for sort Sort Prop.
Scheme eqlistA_ind' := Induction for eqlistA Sort Prop.
Theorem lelistA_unique :
forall (x : A) (xs : list A) (p q : lelistA R x xs), p = q.
Theorem sort_unique :
forall (xs : list A) (p q : sort R xs), p = q.
Theorem eqlistA_unique :
forall (xs ys : list A) (p q : eqlistA R xs ys), p = q.
End Uniqueness_Of_SetoidList_Proofs.
This page has been generated by coqdoc