# Library list_extensions.equiv_list

``` Require Import List. Require Import Relations. Lemma equiv_in_list :   forall (A : Set) (R : relation A) s ll, (forall s t, In (s,t) ll -> R s t) ->   In s (map (fun st => fst st) ll) ->   exists t, exists ll1, exists ll2, R s t /\ ll = ll1 ++ (s,t) :: ll2. Proof. intros A R s ll E_ll s_in_ll1; setoid_rewrite in_map_iff in s_in_ll1; destruct s_in_ll1 as [[s' t] [s'_eq_s st_in_ll]]; simpl in s'_eq_s; subst s'; destruct (In_split _ _ st_in_ll) as [ll1 [ll2 H]]; exists t; exists ll1; exists ll2; split; trivial. apply E_ll; trivial. Qed. Lemma equiv_in_list_2 :   forall (A : Set) (R : relation A) s ll, (forall s t, In (s,t) ll -> R s t) ->   In s (map (fun st => snd st) ll) ->   exists t, exists ll1, exists ll2, R t s /\ ll = ll1 ++ (t,s) :: ll2. Proof. intros A R s ll E_ll s_in_ll2; setoid_rewrite in_map_iff in s_in_ll2; destruct s_in_ll2 as [[t s'] [s'_eq_s ts_in_ll]]; simpl in s'_eq_s; subst s'; destruct (In_split _ _ ts_in_ll) as [ll1 [ll2 H]]; exists t; exists ll1; exists ll2; split; trivial. apply E_ll; trivial. Qed. Lemma equiv_swap :   forall (A : Set) (R : relation A),   forall ll, (forall s t, In (s,t) ll -> R s t) ->   exists ll', (forall s t, In (s,t) ll' -> R t s) /\                 map (fun st => fst st) ll = map (fun st => snd st) ll' /\                 map (fun st => snd st) ll = map (fun st => fst st) ll' /\                 (forall s t, In (s,t) ll <-> In (t,s) ll'). Proof. intros A R ll; induction ll as [ | [s t] ll]; intro E_ll. exists (@nil (A * A)); repeat split; trivial; contradiction. destruct IHll as [ll' [E_ll' [H1 [H2 H3]]]]. intros; apply E_ll; right; trivial. exists ((t,s) :: ll'); repeat split. intros t' s' [t's'_eq_ts | t's'_in_ll']. injection t's'_eq_ts; intros; subst; apply E_ll; left; trivial. apply E_ll'; trivial. simpl; rewrite H1; trivial. simpl; rewrite H2; trivial. intros [st_eq_st | st_in_ll]. injection st_eq_st; intros; subst; left; trivial. right; setoid_rewrite <- H3; trivial. intros [ts_eq_ts | ts_in_ll]. injection ts_eq_ts; intros; subst; left; trivial. right; setoid_rewrite H3; trivial. Qed. ```