# Library Coq.Lists.SetoidList

Require Export List.
Require Export Sorting.
Require Export Setoid.

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

Hint Constructors InA.

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.

lists with same elements modulo eqA

Definition equivlistA l l' := forall x, InA x l <-> InA x l'.

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.

Compatibility of a boolean function with respect to an equality.

Definition compat_bool (f : A->bool) := forall x y, eqA x y -> f x = f y.

Compatibility of a function upon natural numbers.

Definition compat_nat (f : A->nat) := forall x y, eqA x y -> f x = f y.

Compatibility of a predicate with respect to an equality.

Definition compat_P (P : A->Prop) := forall x y, eqA x y -> P x -> P y.

Results concerning lists modulo eqA

Hypothesis eqA_refl : forall x, eqA x x.
Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.

Hint Resolve eqA_refl eqA_trans.
Hint Immediate eqA_sym.

Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
Hint Immediate InA_eqA.

Lemma In_InA : forall l x, In x l -> InA x l.
Hint Resolve In_InA.

Lemma InA_split : forall l x, InA x l ->
exists l1, exists y, exists 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.

Results concerning lists modulo eqA and ltA

Variable ltA : A -> A -> Prop.

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 -> ~ eqA x y.
Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z.
Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z.

Hint Resolve ltA_trans.
Hint Immediate ltA_eqA eqA_ltA.

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

Hint Constructors lelistA sort.

Lemma InfA_ltA :
forall l x y, ltA x y -> InfA y l -> InfA x l.

Lemma InfA_eqA :
forall l x y, eqA x y -> InfA y l -> InfA x l.
Hint Immediate InfA_ltA InfA_eqA.

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

Section NoDupA.

Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l.

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

End NoDupA.

Section EqlistA.

Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'.

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

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

Lemma filter_InA : forall f, (compat_bool 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.

Section Fold.

Variable B:Type.
Variable eqB:B->B->Prop.

Compatibility of a two-argument function with respect to two equalities.
Definition compat_op (f : A -> B -> B) :=
forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').

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 st:Equivalence eqB.
Variable f:A->B->B.
Variable i:B.
Variable Comp:compat_op f.

Lemma fold_right_eqlistA :
forall s s', eqlistA s s' ->
eqB (fold_right f i s) (fold_right f i s').

Lemma equivlistA_NoDupA_split : forall 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).

ForallList2 : specifies that a certain binary predicate should always hold when inspecting two different elements of the list.

Inductive ForallList2 (R : A -> A -> Prop) : list A -> Prop :=
| ForallNil : ForallList2 R nil
| ForallCons : forall a l,
(forall b, In b l -> R a b) ->
ForallList2 R l -> ForallList2 R (a::l).
Hint Constructors ForallList2.

NoDupA can be written in terms of ForallList2

Lemma ForallList2_NoDupA : forall l,
ForallList2 (fun a b => ~eqA a b) l <-> NoDupA l.

Lemma ForallList2_impl : forall (R R':A->A->Prop),
(forall a b, R a b -> R' a b) ->
forall l, ForallList2 R l -> ForallList2 R' l.

The following definition is easier to use than ForallList2.

Definition ForallList2_alt (R:A->A->Prop) l :=
forall a b, InA a l -> InA b l -> ~eqA a b -> R a b.

Section Restriction.
Variable R : A -> A -> Prop.

ForallList2 and ForallList2_alt are related, but no completely equivalent. For proving one implication, we need to know that the list has no duplicated elements...

Lemma ForallList2_equiv1 : forall l, NoDupA l ->
ForallList2_alt R l -> ForallList2 R l.

... and for proving the other implication, we need to be able to reverse and adapt relation R modulo eqA.

Hypothesis R_sym : forall a b, R a b -> R b a.
Hypothesis R_compat : forall a, compat_P (R a).

Lemma ForallList2_equiv2 : forall l,
ForallList2 R l -> ForallList2_alt R l.

Lemma ForallList2_equiv : forall l, NoDupA l ->
(ForallList2 R l <-> ForallList2_alt R l).

Lemma ForallList2_equivlistA : forall l l', NoDupA l' ->
equivlistA l l' -> ForallList2 R l -> ForallList2 R l'.

Variable TraR :transpose_restr R f.

Lemma fold_right_commutes_restr :
forall s1 s2 x, ForallList2 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' -> ForallList2 R s ->
equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').

forall s' s x, NoDupA s -> NoDupA s' -> ForallList2 R s' -> ~ InA x s ->
equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).

End Restriction.

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

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){struct l} : 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.

End Fold.

End Type_with_equality.

Hint Unfold compat_bool compat_nat compat_P.
Hint Constructors InA NoDupA sort lelistA eqlistA.

Section Find.
Variable A B : Type.
Variable eqA : A -> A -> Prop.
Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x.
Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z.
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.