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

Hint Constructors InA.

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.

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.

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.

Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).

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.

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

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.

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

Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).

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.

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.

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.

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.


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.