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.Section Type_with_equality.
Variable A : Type.
Variable eqA : A -> A -> Prop.
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.
Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l.
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
Lemma NoDupA_altdef : forall l,
NoDupA l <-> ForallOrdPairs (complement eqA) l.
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.
Lemma eqlistA_altdef : forall l l', eqlistA l l' <-> Forall2 eqA l l'.
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.
Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA.
InA is compatible with eqA (for its first arg) and with
equivlistA (and hence eqlistA) for its second arg
Global Instance InA_compat : Proper (eqA==>equivlistA==>iff) InA.
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.