Library Lib_ListFacts
Require Import List.
Require Import SetoidList.
Require Import Sorting.
Require Import Relations.
Lemma not_in_cons :
forall (A : Type) (ys : list A) x y,
x <> y -> ~ In x ys -> ~ In x (y :: ys).
Hint Resolve not_in_cons.
Lemma not_In_app :
forall (A : Type) (xs ys : list A) x,
~ In x xs -> ~ In x ys -> ~ In x (xs ++ ys).
Hint Resolve not_In_app.
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.
Hint Resolve incl_nil.
Lemma incl_trans :
forall (A : Type) (xs ys zs : list A),
incl xs ys -> incl ys zs -> incl xs zs.
Hint Immediate incl_trans.
Lemma In_incl :
forall (A : Type) (x : A) (ys zs : list A),
In x ys -> incl ys zs -> In x zs.
Hint Immediate In_incl.
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.
The following are placed in the
datatypes
library by the List theory.
It's convenient to also have them in core
.
Hint Resolve in_eq.
Hint Resolve in_cons.
Hint Resolve incl_refl.
Hint Resolve incl_nil.
Hint Resolve incl_cons.
Hint Resolve incl_tl.
Hint Resolve incl_app.
Hint Immediate incl_trans.
The following tactics can be used to simply hypotheses concerning lists.
Ltac simpl_list_hyp H :=
let LH1 := fresh "LH" in
let LH2 := fresh "LH" in
match type of H with
| incl (?J :: ?K) ?L =>
destruct (elim_incl_cons H) as [LH1 LH2]; clear H;
try simpl_list_hyp LH1; try simpl_list_hyp LH2
| incl (?J ++ ?K) ?L =>
destruct (elim_incl_app J K H) as [LH1 LH2]; clear H;
try simpl_list_hyp LH1; try simpl_list_hyp LH2
| incl nil _ =>
clear H
| In ?x (?y :: ?ys) =>
destruct (in_inv H) as [LH1 | LH1]; clear H;
try simpl_list_hyp LH1
| In ?x (?ys ++ ?zs) =>
destruct (in_app_or ys zs x H) as [LH1 | LH1]; clear H;
try simpl_list_hyp LH1
| In _ nil =>
simpl in H; intuition
| ~ In _ nil =>
clear H
| ~ In _ (_ :: _) =>
destruct (elim_not_In_cons H) as [LH1 LH2]; clear H;
try simpl_list_hyp LH1; try simpl_list_hyp LH2
| ~ In ?x (?K ++ ?L) =>
destruct (elim_not_In_app K L x H) as [LH1 LH2]; clear H;
try simpl_list_hyp LH1; try simpl_list_hyp LH2
| In _ _ =>
progress (simpl in H)
| incl _ _ =>
progress (simpl in H)
| ~ In _ _ =>
progress (simpl in H)
end.
Ltac simpl_list_hyps :=
match goal with
| H : _ |- _ => simpl_list_hyp H; simpl_list_hyps
| H : ~ (?a = ?b \/ False), J : ?b = ?a |- _ => subst b; intuition
| H : ~ (?a = ?b \/ False), J : ?a = ?b |- _ => subst a; intuition
| _ => idtac
end.
Hint Extern 4 (In ?x ?L) => simpl; simpl_list_hyps.
Hint Extern 4 (~ In ?x ?L) => simpl; simpl_list_hyps.
Hint Extern 4 (incl ?L1 ?L2) => simpl; simpl_list_hyps.
Lemma InA_iff_In :
forall (A : Set) x xs, InA (@eq A) x xs <-> In x xs.
It is decidable to tell whether a list a sorted according to
some relation.
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}.
End DecidableSorting.
Two sorted lists are equal if they contain the same elements.
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.