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