Require Import Coq.Classes.Morphisms.
Require Import Coq.Lists.List.
Require Export Logic.lib.Relation_ext.

Instance list_Reflexive {A R} {EqA: @Equivalence A R}: Reflexive (Forall2 (@equiv A _ _)).
Proof.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  hnf; intros.
(* Goal: @Forall2 A A (@equiv A R EqA) x x *)
  induction x; constructor.
  + reflexivity.
  + auto.
Qed.

Instance list_Symmetric {A R} {EqA: @Equivalence A R}: Symmetric (Forall2 (@equiv A _ _)).
Proof.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  hnf; intros.
(* Goal: @Forall2 A A (@equiv A R EqA) y x *)
  revert y H; induction x; intros; destruct y; try solve [inversion H]; constructor.
  + inversion H; subst. symmetry. auto.
  + inversion H; subst. apply IHx; auto.
Qed.

Instance list_Transitive {A R} {EqA: @Equivalence A R}: Transitive (Forall2 (@equiv A _ _)).
Proof.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  hnf; intros.
(* Goal: @Forall2 A A (@equiv A R EqA) x z *)
  revert y z H H0; induction x; intros; destruct y, z; try solve [inversion H; subst; inversion H0]; constructor.
  + inversion H; inversion H0; subst. etransitivity; eauto.
  + inversion H; inversion H0; subst. eapply IHx; eauto.
Qed.

Instance list_Equivalence {A R} {EqA: @Equivalence A R}: Equivalence (Forall2 (@equiv A _ _)).
Proof.
(* Goal: @Equivalence A (@respectful_relation A B f R) *)
  split.
(* Goal: @Reflexive (list A) (@Forall2 A A (@equiv A R EqA)) *)
(* Goal: @Symmetric (list A) (@Forall2 A A (@equiv A R EqA)) *)
(* Goal: @Transitive (list A) (@Forall2 A A (@equiv A R EqA)) *)
  apply list_Reflexive.
(* Goal: @Symmetric (list A) (@Forall2 A A (@equiv A R EqA)) *)
(* Goal: @Transitive (list A) (@Forall2 A A (@equiv A R EqA)) *)
  apply list_Symmetric.
(* Goal: @Transitive (list A) (@Forall2 A A (@equiv A R EqA)) *)
  apply list_Transitive.
Qed.

(* The Instances-Searching for type classes are type oriented.
As resp_Equivalence is a (Equvalence B), it should not be involved
in Instances-Searching. Or else, searching engine will apply this
Instance, and do never terminate. *)

Lemma resp_Reflexive {A B} (f: A -> B) (R: relation B) {RR: Reflexive R}: Reflexive (respectful_relation f R).
Proof.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  intros.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  hnf; intros.
(* Goal: @respectful_relation A B f R x z *)
  unfold respectful_relation.
(* Goal: R (f x) (f x) *)
  reflexivity.
Qed.

Lemma resp_Symmetric {A B} (f: A -> B) (R: relation B) {SR: Symmetric R}: Symmetric (respectful_relation f R).
Proof.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  intros.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  hnf; intros.
(* Goal: @respectful_relation A B f R x z *)
  unfold respectful_relation.
(* Goal: R (f y) (f x) *)
  symmetry.
(* Goal: R (f x) (f y) *)
  auto.
Qed.

Lemma resp_Transitive {A B} (f: A -> B) (R: relation B) {TR: Transitive R}: Transitive (respectful_relation f R).
Proof.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  intros.
(* Goal: @Transitive A (@respectful_relation A B f R) *)
  hnf; intros.
(* Goal: @respectful_relation A B f R x z *)
  unfold respectful_relation.  
(* Goal: R (f x) (f y) *)
  transitivity (f y); auto. 
Qed.

Lemma resp_Equivalence {A B} (f: A -> B) (R: relation B) {ER: Equivalence R}: Equivalence (respectful_relation f R).
Proof.
(* Goal: @Equivalence A (@respectful_relation A B f R) *)
  destruct ER.
(* Goal: @Equivalence A (@respectful_relation A B f R) *)
  split.
  + apply resp_Reflexive; auto.
  + apply resp_Symmetric; auto.
  + apply resp_Transitive; auto.
Qed.



