Library Coq.Lists.SetoidList
Require Export List.
Require Export Sorted.
Require Export Setoid Basics Morphisms.
Set Implicit Arguments.
Logical relations over lists with respect to a setoid equality
or ordering.
Being in a list modulo an equality relation over type A.
Inductive InA (x : A) : list A -> Prop :=
| InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
| InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
Hint Constructors InA : core.
TODO: it would be nice to have a generic definition instead
of the previous one. Having InA = Exists eqA raises too
many compatibility issues. For now, we only state the equivalence:
Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l.
Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l.
Lemma InA_nil : forall x, InA x nil <-> False.
An alternative definition of InA.
A list without redundancy modulo the equality over A.
Inductive NoDupA : list A -> Prop :=
| NoDupA_nil : NoDupA nil
| NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
Hint Constructors NoDupA : core.
An alternative definition of NoDupA based on ForallOrdPairs
lists with same elements modulo eqA
Definition inclA l l' := forall x, InA x l -> InA x l'.
Definition equivlistA l l' := forall x, InA x l <-> InA x l'.
Lemma incl_nil l : inclA nil l.
Hint Resolve incl_nil : list.
lists with same elements modulo eqA at the same place
Inductive eqlistA : list A -> list A -> Prop :=
| eqlistA_nil : eqlistA nil nil
| eqlistA_cons : forall x x' l l',
eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
Hint Constructors eqlistA : core.
We could also have written eqlistA = Forall2 eqA.
Results concerning lists modulo eqA
Hypothesis eqA_equiv : Equivalence eqA.
Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
Hint Resolve eqarefl eqatrans : core.
Hint Immediate eqasym : core.
Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
First, the two notions equivlistA and eqlistA are indeed equivlances
Global Instance equivlist_equiv : Equivalence equivlistA.
Global Instance eqlistA_equiv : Equivalence eqlistA.
Moreover, eqlistA implies equivlistA. A reverse result
will be proved later for sorted list without duplicates.
InA is compatible with eqA (for its first arg) and with
equivlistA (and hence eqlistA) for its second arg
For compatibility, an immediate consequence of InA_compat
Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
Hint Immediate InA_eqA : core.
Lemma In_InA : forall l x, In x l -> InA x l.
Hint Resolve In_InA : core.
Lemma InA_split : forall l x, InA x l ->
exists l1 y l2, eqA x y /\ l = l1++y::l2.
Lemma InA_app : forall l1 l2 x,
InA x (l1 ++ l2) -> InA x l1 \/ InA x l2.
Lemma InA_app_iff : forall l1 l2 x,
InA x (l1 ++ l2) <-> InA x l1 \/ InA x l2.
Lemma InA_rev : forall p m,
InA p (rev m) <-> InA p m.
Some more facts about InA
Lemma InA_singleton x y : InA x (y::nil) <-> eqA x y.
Lemma InA_double_head x y l :
InA x (y :: y :: l) <-> InA x (y :: l).
Lemma InA_permute_heads x y z l :
InA x (y :: z :: l) <-> InA x (z :: y :: l).
Lemma InA_app_idem x l : InA x (l ++ l) <-> InA x l.
Section NoDupA.
Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->
(forall x, InA x l -> InA x l' -> False) ->
NoDupA (l++l').
Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l).
Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l').
Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l').
Lemma NoDupA_singleton x : NoDupA (x::nil).
End NoDupA.
Section EquivlistA.
Global Instance equivlistA_cons_proper:
Proper (eqA ==> equivlistA ==> equivlistA) (@cons A).
Global Instance equivlistA_app_proper:
Proper (equivlistA ==> equivlistA ==> equivlistA) (@app A).
Lemma equivlistA_cons_nil x l : ~ equivlistA (x :: l) nil.
Lemma equivlistA_nil_eq l : equivlistA l nil -> l = nil.
Lemma equivlistA_double_head x l : equivlistA (x :: x :: l) (x :: l).
Lemma equivlistA_permute_heads x y l :
equivlistA (x :: y :: l) (y :: x :: l).
Lemma equivlistA_app_idem l : equivlistA (l ++ l) l.
Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y ->
NoDupA (x::l) -> NoDupA (l1++y::l2) ->
equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2).
End EquivlistA.
Section Fold.
Variable B:Type.
Variable eqB:B->B->Prop.
Variable st:Equivalence eqB.
Variable f:A->B->B.
Variable i:B.
Variable Comp:Proper (eqA==>eqB==>eqB) f.
Lemma fold_right_eqlistA :
forall s s', eqlistA s s' ->
eqB (fold_right f i s) (fold_right f i s').
Fold with restricted transpose hypothesis.
Section Fold_With_Restriction.
Variable R : A -> A -> Prop.
Hypothesis R_sym : Symmetric R.
Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
Compatibility of ForallOrdPairs with respect to inclA.
Lemma ForallOrdPairs_inclA : forall l l',
NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'.
Two-argument functions that allow to reorder their arguments.
Definition transpose (f : A -> B -> B) :=
forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)).
A version of transpose with restriction on where it should hold
Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) :=
forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
Variable TraR :transpose_restr R f.
Lemma fold_right_commutes_restr :
forall s1 s2 x, ForallOrdPairs R (s1++x::s2) ->
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
Lemma fold_right_equivlistA_restr :
forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
Lemma fold_right_add_restr :
forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
End Fold_With_Restriction.
forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)).
Variable TraR :transpose_restr R f.
Lemma fold_right_commutes_restr :
forall s1 s2 x, ForallOrdPairs R (s1++x::s2) ->
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
Lemma fold_right_equivlistA_restr :
forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
Lemma fold_right_add_restr :
forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
End Fold_With_Restriction.
we now state similar results, but without restriction on transpose.
Variable Tra :transpose f.
Lemma fold_right_commutes : forall s1 s2 x,
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
Lemma fold_right_equivlistA :
forall s s', NoDupA s -> NoDupA s' ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
Lemma fold_right_add :
forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
End Fold.
Section Fold2.
Variable B:Type.
Variable eqB:B->B->Prop.
Variable st:Equivalence eqB.
Variable f:A->B->B.
Variable Comp:Proper (eqA==>eqB==>eqB) f.
Lemma fold_right_eqlistA2 :
forall s s' (i j:B) (heqij: eqB i j) (heqss': eqlistA s s'),
eqB (fold_right f i s) (fold_right f j s').
Section Fold2_With_Restriction.
Variable R : A -> A -> Prop.
Hypothesis R_sym : Symmetric R.
Hypothesis R_compat : Proper (eqA==>eqA==>iff) R.
Two-argument functions that allow to reorder their arguments.
Definition transpose2 (f : A -> B -> B) :=
forall (x y : A) (z z': B), eqB z z' -> eqB (f x (f y z)) (f y (f x z')).
forall (x y : A) (z z': B), eqB z z' -> eqB (f x (f y z)) (f y (f x z')).
A version of transpose with restriction on where it should hold
Definition transpose_restr2 (R : A -> A -> Prop)(f : A -> B -> B) :=
forall (x y : A) (z z': B), R x y -> eqB z z' -> eqB (f x (f y z)) (f y (f x z')).
Variable TraR :transpose_restr2 R f.
Lemma fold_right_commutes_restr2 :
forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) ->
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))).
Lemma fold_right_equivlistA_restr2 :
forall s s' i j,
NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
equivlistA s s' -> eqB i j ->
eqB (fold_right f i s) (fold_right f j s').
Lemma fold_right_add_restr2 :
forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
End Fold2_With_Restriction.
Variable Tra :transpose2 f.
Lemma fold_right_commutes2 : forall s1 s2 i x x',
eqA x x' ->
eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))).
Lemma fold_right_equivlistA2 :
forall s s' i j, NoDupA s -> NoDupA s' -> eqB i j ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
Lemma fold_right_add2 :
forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
End Fold2.
Section Remove.
Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
Fixpoint removeA (x : A) (l : list A) : list A :=
match l with
| nil => nil
| y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
end.
Lemma removeA_filter : forall x l,
removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
Lemma removeA_NoDupA :
forall s x, NoDupA s -> NoDupA (removeA x s).
Lemma removeA_equivlistA : forall l l' x,
~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
End Remove.
forall (x y : A) (z z': B), R x y -> eqB z z' -> eqB (f x (f y z)) (f y (f x z')).
Variable TraR :transpose_restr2 R f.
Lemma fold_right_commutes_restr2 :
forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) ->
eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))).
Lemma fold_right_equivlistA_restr2 :
forall s s' i j,
NoDupA s -> NoDupA s' -> ForallOrdPairs R s ->
equivlistA s s' -> eqB i j ->
eqB (fold_right f i s) (fold_right f j s').
Lemma fold_right_add_restr2 :
forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
End Fold2_With_Restriction.
Variable Tra :transpose2 f.
Lemma fold_right_commutes2 : forall s1 s2 i x x',
eqA x x' ->
eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))).
Lemma fold_right_equivlistA2 :
forall s s' i j, NoDupA s -> NoDupA s' -> eqB i j ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
Lemma fold_right_add2 :
forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)).
End Fold2.
Section Remove.
Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }.
Fixpoint removeA (x : A) (l : list A) : list A :=
match l with
| nil => nil
| y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl)
end.
Lemma removeA_filter : forall x l,
removeA x l = filter (fun y => if eqA_dec x y then false else true) l.
Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
Lemma removeA_NoDupA :
forall s x, NoDupA s -> NoDupA (removeA x s).
Lemma removeA_equivlistA : forall l l' x,
~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
End Remove.
Results concerning lists modulo eqA and ltA
Variable ltA : A -> A -> Prop.
Hypothesis ltA_strorder : StrictOrder ltA.
Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
Hint Resolve sotrans : core.
Notation InfA:=(lelistA ltA).
Notation SortA:=(sort ltA).
Hint Constructors lelistA sort : core.
Lemma InfA_ltA :
forall l x y, ltA x y -> InfA y l -> InfA x l.
Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA.
For compatibility, can be deduced from InfA_compat
Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
Hint Immediate InfA_ltA InfA_eqA : core.
Lemma SortA_InfA_InA :
forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
Lemma In_InfA :
forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
Lemma InA_InfA :
forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
Lemma InfA_alt :
forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
Lemma SortA_app :
forall l1 l2, SortA l1 -> SortA l2 ->
(forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
SortA (l1 ++ l2).
Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
Hint Immediate InfA_ltA InfA_eqA : core.
Lemma SortA_InfA_InA :
forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
Lemma In_InfA :
forall l x, (forall y, In y l -> ltA x y) -> InfA x l.
Lemma InA_InfA :
forall l x, (forall y, InA y l -> ltA x y) -> InfA x l.
Lemma InfA_alt :
forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)).
Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2).
Lemma SortA_app :
forall l1 l2, SortA l1 -> SortA l2 ->
(forall x y, InA x l1 -> InA y l2 -> ltA x y) ->
SortA (l1 ++ l2).
Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.
Some results about eqlistA
Section EqlistA.
Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.
Global Instance app_eqlistA_compat :
Proper (eqlistA==>eqlistA==>eqlistA) (@app A).
For compatibility, can be deduced from app_eqlistA_compat
Lemma eqlistA_app : forall l1 l1' l2 l2',
eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
Lemma eqlistA_rev_app : forall l1 l1',
eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
eqlistA ((rev l1)++l2) ((rev l1')++l2').
Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
Lemma eqlistA_rev : forall l1 l1',
eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
Lemma SortA_equivlistA_eqlistA : forall l l',
SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
End EqlistA.
eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2').
Lemma eqlistA_rev_app : forall l1 l1',
eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' ->
eqlistA ((rev l1)++l2) ((rev l1')++l2').
Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A).
Lemma eqlistA_rev : forall l1 l1',
eqlistA l1 l1' -> eqlistA (rev l1) (rev l1').
Lemma SortA_equivlistA_eqlistA : forall l l',
SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'.
End EqlistA.
A few things about filter
Section Filter.
Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
Lemma filter_split :
forall f, (forall x y, f x = true -> f y = false -> ltA x y) ->
forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
End Filter.
End Type_with_equality.
Hint Constructors InA eqlistA NoDupA sort lelistA : core.
Section Find.
Variable A B : Type.
Variable eqA : A -> A -> Prop.
Hypothesis eqA_equiv : Equivalence eqA.
Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B :=
match l with
| nil => None
| (a,b)::l => if f a then Some b else findA f l
end.
Lemma findA_NoDupA :
forall l a b,
NoDupA (fun p p' => eqA (fst p) (fst p')) l ->
(InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <->
findA (fun a' => if eqA_dec a a' then true else false) l = Some b).
End Find.
Compatibility aliases. Proper is rather to be used directly now.
Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) :=
Proper (eqA==>Logic.eq) f.
Definition compat_nat {A} (eqA:A->A->Prop)(f:A->nat) :=
Proper (eqA==>Logic.eq) f.
Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) :=
Proper (eqA==>impl) P.
Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) :=
Proper (eqA==>eqB==>eqB) f.