# 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.
This can be seen as a complement of predicate lelistA and sort found in Sorting.

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).

#[local]
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).

#[local]
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.
#[local]
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').

#[local]
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).

#[local]
Hint Resolve eqarefl eqatrans : core.
#[local]
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.
#[local]
Hint Immediate InA_eqA : core.

Lemma In_InA : forall l x, In x l -> InA x l.
#[local]
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.

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.
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)).

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').

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').

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')).

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').

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').

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).

#[local]
Hint Resolve sotrans : core.

Notation InfA:=(lelistA ltA).
Notation SortA:=(sort ltA).

#[local]
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.
#[local]
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.

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.

Section Filter.

Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
Arguments eq {A} x _.

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.

#[global]
Hint Constructors InA eqlistA NoDupA sort lelistA : core.

Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _.
Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _.

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.