# Library Coq.Lists.SetoidList

``` Require Export List. Require Export Sorting. Require Export Setoid. Set Implicit Arguments. Unset Strict Implicit. ```

# 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 : Set. 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. ```
An alternative definition of `InA`.
``` Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l. Proof.  induction l; intuition.  inversion H.  firstorder.  inversion H1; firstorder.  firstorder; subst; auto. Qed. ```
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 eqlistA l l' := forall x, InA x l <-> InA x l'. ```
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. Proof.  intros s x y.  do 2 rewrite InA_alt.  intros H (z,(U,V)).  exists z; split; eauto. Qed. Hint Immediate InA_eqA. Lemma In_InA : forall l x, In x l -> InA x l. Proof.  simple induction l; simpl in |- *; intuition.  subst; auto. Qed. 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. Proof. induction l; inversion_clear 1. exists (@nil A); exists a; exists l; auto. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. Qed. ```
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). Lemma InfA_ltA :  forall l x y, ltA x y -> InfA y l -> InfA x l. Proof.  intro s; case s; constructor; inversion_clear H0.  eapply ltA_trans; eauto. Qed. Lemma InfA_eqA :  forall l x y, eqA x y -> InfA y l -> InfA x l. Proof.  intro s; case s; constructor; inversion_clear H0; eauto. Qed. 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. Proof.  simple induction l.  intros; inversion H1.  intros.  inversion_clear H0; inversion_clear H1; inversion_clear H2.  eapply ltA_eqA; eauto.  eauto. Qed. Lemma In_InfA :  forall l x, (forall y, In y l -> ltA x y) -> InfA x l. Proof.  simple induction l; simpl in |- *; intros; constructor; auto. Qed. Lemma InA_InfA :  forall l x, (forall y, InA y l -> ltA x y) -> InfA x l. Proof.  simple induction l; simpl in |- *; intros; constructor; auto. Qed. Lemma InfA_alt :  forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)). Proof. split. intros; eapply SortA_InfA_InA; eauto. apply InA_InfA. Qed. Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. Proof.  simple induction l; auto.  intros x l' H H0.  inversion_clear H0.  constructor; auto.  intro.  assert (ltA x x) by (eapply SortA_InfA_InA; eauto).  elim (ltA_not_eqA H3); auto. Qed. Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' ->   (forall x, InA x l -> InA x l' -> False) ->   NoDupA (l++l'). Proof. induction l; simpl; auto; intros. inversion_clear H. constructor. rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). elim H2. rewrite InA_alt. exists y; auto. apply (H1 a). auto. rewrite InA_alt. exists y; auto. apply IHl; auto. intros. apply (H1 x); auto. Qed. Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). Proof. induction l. simpl; auto. simpl; intros. inversion_clear H. apply NoDupA_app; auto. constructor; auto. intro H2; inversion H2. intros x. rewrite InA_alt. intros (x1,(H2,H3)). inversion_clear 1. destruct H0. apply InA_eqA with x1; eauto. apply In_InA. rewrite In_rev; auto. inversion H4. Qed. Lemma InA_app : forall l1 l2 x,  InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. Proof.  induction l1; simpl in *; intuition.  inversion_clear H; auto.  elim (IHl1 l2 x H0); auto. Qed.  Hint Constructors lelistA sort. Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). Proof.  induction l1; simpl; auto.  inversion_clear 1; auto. Qed. 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). Proof.  induction l1; simpl in *; intuition.  inversion_clear H.  constructor; auto.  apply InfA_app; auto.  destruct l2; auto. Qed. 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 }. Proof. induction l. right; auto. red; inversion 1. destruct (eqA_dec x a). left; auto. destruct IHl. left; auto. right; red; inversion_clear 1; tauto. Qed. 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. Proof. induction l; simpl; auto. destruct (eqA_dec x a); auto. rewrite IHl; auto. Qed. Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y. Proof. induction l; simpl; auto. split. inversion_clear 1. destruct 1; inversion_clear H. intros. destruct (eqA_dec x a); simpl; auto. rewrite IHl; split; destruct 1; split; auto. inversion_clear H; auto. destruct H0; apply eqA_trans with a; auto. split. inversion_clear 1. split; auto. swap n. apply eqA_trans with y; auto. rewrite (IHl x y) in H0; destruct H0; auto. destruct 1; inversion_clear H; auto. constructor 2; rewrite IHl; auto. Qed. Lemma removeA_NoDupA :   forall s x, NoDupA s -> NoDupA (removeA x s). Proof. simple induction s; simpl; intros. auto. inversion_clear H0. destruct (eqA_dec x a); simpl; auto. constructor; auto. rewrite removeA_InA. intuition. Qed. Lemma removeA_eqlistA : forall l l' x,   ~InA x l -> eqlistA (x :: l) l' -> eqlistA l (removeA x l'). Proof. unfold eqlistA; intros. rewrite removeA_InA. split; intros. rewrite <- H0; split; auto. swap H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. inversion_clear H1; auto. elim H2; auto. Qed. Let addlistA x l l' := forall y, InA y l' <-> eqA x y \/ InA y l. Lemma removeA_add :   forall s s' x x', NoDupA s -> NoDupA (x' :: s') ->   ~ eqA x x' -> ~ InA x s ->   addlistA x s (x' :: s') -> addlistA x (removeA x' s) s'. Proof. unfold addlistA; intros. inversion_clear H0. rewrite removeA_InA; auto. split; intros. destruct (eqA_dec x y); auto; intros. right; split; auto. destruct (H3 y); clear H3. destruct H6; intuition. swap H4; apply InA_eqA with y; auto. destruct H0. assert (InA y (x' :: s')) by (rewrite H3; auto). inversion_clear H6; auto. elim H1; apply eqA_trans with y; auto. destruct H0. assert (InA y (x' :: s')) by (rewrite H3; auto). inversion_clear H7; auto. elim H6; auto. Qed. Section Fold. Variable B:Set. Variable eqB:B->B->Prop. ```
Two-argument functions that allow to reorder its arguments.
``` Definition transpose (f : A -> B -> B) :=   forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). ```
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'). ```
Compatibility of a function upon natural numbers.
``` Definition compat_nat (f : A -> nat) :=   forall x x' : A, eqA x x' -> f x = f x'. Variable st:Setoid_Theory _ eqB. Variable f:A->B->B. Variable Comp:compat_op f. Variable Ass:transpose f. Variable i:B. Lemma removeA_fold_right_0 :   forall s x, ~InA x s ->   eqB (fold_right f i s) (fold_right f i (removeA x s)). Proof.  simple induction s; simpl; intros.  refl_st.  destruct (eqA_dec x a); simpl; intros.  absurd_hyp e; auto.  apply Comp; auto. Qed. Lemma removeA_fold_right :   forall s x, NoDupA s -> InA x s ->   eqB (fold_right f i s) (f x (fold_right f i (removeA x s))). Proof.  simple induction s; simpl.  inversion_clear 2.  intros.  inversion_clear H0.  destruct (eqA_dec x a); simpl; intros.  apply Comp; auto.  apply removeA_fold_right_0; auto.  swap H2; apply InA_eqA with x; auto.  inversion_clear H1.  destruct n; auto.  trans_st (f a (f x (fold_right f i (removeA x l)))). Qed. Lemma fold_right_equal :   forall s s', NoDupA s -> NoDupA s' ->   eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof.  simple induction s.  destruct s'; simpl.  intros; refl_st; auto.  unfold eqlistA; intros.  destruct (H1 a).  assert (X : InA a nil); auto; inversion X.  intros x l Hrec s' N N' E; simpl in *.  trans_st (f x (fold_right f i (removeA x s'))).  apply Comp; auto.  apply Hrec; auto.  inversion N; auto.  apply removeA_NoDupA; auto; apply eqA_trans.  apply removeA_eqlistA; auto.  inversion_clear N; auto.  sym_st.  apply removeA_fold_right; auto.  unfold eqlistA in E.  rewrite <- E; auto. Qed. Lemma fold_right_add :   forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->   addlistA x s s' -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof.  simple induction s'.  unfold addlistA; intros.  destruct (H2 x); clear H2.  assert (X : InA x nil); auto; inversion X.  intros x' l' Hrec s x N N' IN EQ; simpl.  destruct (eqA_dec x x').  apply Comp; auto.  apply fold_right_equal; auto.  inversion_clear N'; trivial.  unfold eqlistA; unfold addlistA in EQ; intros.  destruct (EQ x0); clear EQ.  split; intros.  destruct H; auto.  inversion_clear N'.  destruct H2; apply InA_eqA with x0; auto.  apply eqA_trans with x; auto.  assert (X:InA x0 (x' :: l')); auto; inversion_clear X; auto.  destruct IN; apply InA_eqA with x0; auto.  apply eqA_trans with x'; auto.  trans_st (f x' (f x (fold_right f i (removeA x' s)))).  apply Comp; auto.  apply Hrec; auto.  apply removeA_NoDupA; auto; apply eqA_trans.  inversion_clear N'; auto.  rewrite removeA_InA; intuition.  apply removeA_add; auto.  trans_st (f x (f x' (fold_right f i (removeA x' s)))).  apply Comp; auto.  sym_st.  apply removeA_fold_right; auto.  destruct (EQ x').  destruct H; auto; destruct n; auto. Qed. End Fold. End Remove. End Type_with_equality. Hint Constructors InA. Hint Constructors NoDupA. Hint Constructors sort. Hint Constructors lelistA. Section Find. Variable A B : Set. 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). Proof. induction l; simpl; intros. split; intros; try discriminate. inversion H0. destruct a as (a',b'); rename a0 into a. inversion_clear H. split; intros. inversion_clear H. simpl in *; destruct H2; subst b'. destruct (eqA_dec a a'); intuition. destruct (eqA_dec a a'); simpl. destruct H0. generalize e H2 eqA_trans eqA_sym; clear. induction l. inversion 2. inversion_clear 2; intros; auto. destruct a0. compute in H; destruct H. subst b. constructor 1; auto. simpl. apply eqA_trans with a; auto. rewrite <- IHl; auto. destruct (eqA_dec a a'); simpl in *. inversion H; clear H; intros; subst b'; auto. constructor 2. rewrite IHl; auto. Qed. End Find. ```