(* Copied from RamifyCoq project *)

Require Export Coq.Relations.Relations.
Require Import Coq.Classes.Morphisms.
Require Export Coq.Classes.Equivalence.
Require Coq.Setoids.Setoid.

Definition full_relation {A} : relation A := fun _ _ => True.

Lemma inclusion_full_relation: forall {A} P, inclusion A P full_relation.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: @full_relation A x y *)
  hnf.
(* Goal: @eq A n n *)
  auto.
Qed.

Lemma same_relation_spec: forall {A} a1 a2, same_relation A a1 a2 <-> pointwise_relation A (pointwise_relation A iff) a1 a2.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: iff (same_relation A a1 a2) (@pointwise_relation A (forall _ : A, Prop) (@pointwise_relation A Prop iff) a1 a2) *)
  unfold same_relation, inclusion, pointwise_relation.
(* Goal: forall a a0 : A, iff (y a a0) (x a a0) *)
  firstorder.
Qed.

Lemma same_relation_Reflexive {A}: Reflexive (same_relation A).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: same_relation A x x *)
  rewrite same_relation_spec.
(* Goal: @pointwise_relation A (forall _ : A, Prop) (@pointwise_relation A Prop iff) x x *)
  unfold pointwise_relation.
(* Goal: forall a a0 : A, iff (y a a0) (x a a0) *)
  firstorder.
Qed.

Lemma same_relation_Symmetric {A}: Symmetric (same_relation A).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: same_relation A y x *)
  rewrite same_relation_spec in *.
(* Goal: @pointwise_relation A (forall _ : A, Prop) (@pointwise_relation A Prop iff) x z *)
  unfold pointwise_relation in *.
(* Goal: forall a a0 : A, iff (y a a0) (x a a0) *)
  firstorder.
Qed.

Lemma same_relation_Transitive {A}: Transitive (same_relation A).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: same_relation A x z *)
  rewrite same_relation_spec in H, H0 |- *.
(* Goal: @pointwise_relation A (forall _ : A, Prop) (@pointwise_relation A Prop iff) x z *)
  unfold pointwise_relation in *.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: iff (x a a0) (z a a0) *)
  rewrite H, H0.
(* Goal: @eq A n n *)
  tauto.
Qed.

Instance same_relation_Equivalence {A}: Equivalence (same_relation A).
Proof.
(* Goal: @Equivalence (relation A) (same_relation A) *)
  split.
  + apply same_relation_Reflexive.
  + apply same_relation_Symmetric.
  + apply same_relation_Transitive.
Qed.

Instance inclusion_proper {A}: Proper (same_relation A ==> same_relation A ==> iff) (inclusion A).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: @Proper (forall (_ : relation A) (_ : relation A), Prop) (@respectful (relation A) (forall _ : relation A, Prop) (same_relation A) (@respectful (relation A) Prop (same_relation A) iff)) (inclusion A) *)
  do 2 (hnf; intros ?F ?G ?H).
(* Goal: iff (inclusion A F F0) (inclusion A G G0) *)
  unfold inclusion.
(* Goal: iff (forall (x y : A) (_ : F x y), F0 x y) (forall (x y : A) (_ : G x y), G0 x y) *)
  rewrite same_relation_spec in H, H0.
(* Goal: iff (forall (x y : A) (_ : F x y), F0 x y) (forall (x y : A) (_ : G x y), G0 x y) *)
  split; intros HH x y; specialize (HH x y).
  + rewrite (H x y), (H0 x y) in HH.
(* Goal: @eq A n n *)
    auto.
  + rewrite (H x y), (H0 x y).
(* Goal: @eq A n n *)
    auto.
Qed.

Lemma app_same_relation: forall {A: Type} (R1 R2: relation A) (a1 a2: A),
  same_relation A R1 R2 ->
  (R1 a1 a2 <-> R2 a1 a2).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: iff (R1 a1 a2) (R2 a1 a2) *)
  rewrite same_relation_spec in H.
(* Goal: iff (R1 a1 a2) (R2 a1 a2) *)
  specialize (H a1 a2).
(* Goal: @eq A n n *)
  tauto.
Qed.

Inductive compond_relation {A: Type} (R1 R2: relation A) : relation A :=
  | compond_intro: forall x y z, R1 x y -> R2 y z -> compond_relation R1 R2 x z.

Lemma compond_relation_spec: forall {A} (R1 R2: relation A) x z,
  compond_relation R1 R2 x z ->
  exists y, R1 x y /\ R2 y z.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: @respectful_relation A B f (@compond_relation B R1 R2) a1 a2 *)
  inversion H; subst.
(* Goal: @eq A n n *)
  eauto.
Qed.

Lemma compond_relation_inclusion: forall {A} (R1 R2 R3 R4: relation A),
  inclusion _ R1 R2 ->
  inclusion _ R3 R4 ->
  inclusion _ (compond_relation R1 R3) (compond_relation R2 R4).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: @relation_conjunction A R2 R4 x y *)
  inversion H1; subst.
(* Goal: @eq A n n *)
  apply compond_intro with y0; auto.
Qed.

Instance compond_relation_proper {A: Type}: Proper (same_relation A ==> same_relation A ==> same_relation A) compond_relation.
Proof.
(* Goal: @Proper (forall (_ : relation A) (_ : relation A), relation A) (@respectful (relation A) (forall _ : relation A, relation A) (same_relation A) (@respectful (relation A) (relation A) (same_relation A) (same_relation A))) (@relation_conjunction A) *)
  do 2 (hnf; intros).
(* Goal: same_relation A (@relation_conjunction A x x0) (@relation_conjunction A y y0) *)
  destruct H, H0.
(* Goal: @eq A n n *)
  split; apply compond_relation_inclusion; auto.
Defined.

Lemma compond_assoc: forall {A: Type} (R1 R2 R3: relation A),
  same_relation _ (compond_relation (compond_relation R1 R2) R3) (compond_relation R1 (compond_relation R2 R3)).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
  split; hnf; intros;
  do 2
  match goal with
  | H : compond_relation _ _ _ _ |- _ => inversion H; subst; clear H
  end;
  do 2 (econstructor; eauto).
Qed.

Lemma compond_eq_right: forall {A: Type} (R: relation A), same_relation _(compond_relation R eq) R.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  split; hnf; intros.
  + inversion H; subst.
(* Goal: @eq A n n *)
    auto.
(* Goal: @eq A n n *)
  + econstructor; eauto.
Qed.

Lemma compond_eq_left: forall {A: Type} (R: relation A), same_relation _(compond_relation eq R) R.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  split; hnf; intros.
  + inversion H; subst.
(* Goal: @eq A n n *)
    auto.
(* Goal: @eq A n n *)
  + econstructor; eauto.
Qed.

Lemma relation_conjunction_inclusion: forall {A} (R1 R2 R3 R4: relation A),
  inclusion _ R1 R2 ->
  inclusion _ R3 R4 ->
  inclusion _ (relation_conjunction R1 R3) (relation_conjunction R2 R4).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: @relation_conjunction A R2 R4 x y *)
  inversion H1; subst.
(* Goal: @eq A n n *)
  split; auto.
Qed.

Instance relation_conjunction_proper {A: Type}: Proper (same_relation A ==> same_relation A ==> same_relation A) relation_conjunction.
Proof.
(* Goal: @Proper (forall (_ : relation A) (_ : relation A), relation A) (@respectful (relation A) (forall _ : relation A, relation A) (same_relation A) (@respectful (relation A) (relation A) (same_relation A) (same_relation A))) (@relation_conjunction A) *)
  do 2 (hnf; intros).
(* Goal: same_relation A (@relation_conjunction A x x0) (@relation_conjunction A y y0) *)
  destruct H, H0.
(* Goal: @eq A n n *)
  split; apply relation_conjunction_inclusion; auto.
Defined.

Lemma relation_conjunction_iff: forall {A} (R R': relation A) x y,
  relation_conjunction R R' x y <-> R x y /\ R' x y.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: iff (@relation_disjunction A R R' x y) (or (R x y) (R' x y)) *)
  reflexivity.
Qed.

Lemma relation_disjunction_iff: forall {A} (R R': relation A) x y,
  relation_disjunction R R' x y <-> R x y \/ R' x y.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: iff (@relation_disjunction A R R' x y) (or (R x y) (R' x y)) *)
  reflexivity.
Qed.

Lemma relation_disjunction_inclusion_left: forall {A} (R R': relation A),
  inclusion _ R (relation_disjunction R R').
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: inclusion A R' (@relation_disjunction A R R') *)
  intros ? ? ?.
(* Goal: @relation_disjunction A R R' x y *)
  rewrite relation_disjunction_iff.
(* Goal: @eq A n n *)
  tauto.
Qed.

Lemma relation_disjunction_inclusion_right: forall {A} (R R': relation A),
  inclusion _ R' (relation_disjunction R R').
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: inclusion A R' (@relation_disjunction A R R') *)
  intros ? ? ?.
(* Goal: @relation_disjunction A R R' x y *)
  rewrite relation_disjunction_iff.
(* Goal: @eq A n n *)
  tauto.
Qed.

Definition respectful_relation {A B} (f: A -> B) (R: relation B): relation A := fun x y => R (f x) (f y).

Definition fst_relation {A B}: relation A -> relation (A * B) := respectful_relation (@fst A B).

Definition snd_relation {A B}: relation B -> relation (A * B) := respectful_relation (@snd A B).

Instance respectful_relation_proper {A B} (f: A -> B): Proper (same_relation _ ==> same_relation _) (respectful_relation f).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: same_relation A (@respectful_relation A B f x) (@respectful_relation A B f y) *)
  rewrite @same_relation_spec in H |- *.
(* Goal: @pointwise_relation A (forall _ : A, Prop) (@pointwise_relation A Prop iff) (@respectful_relation A B f x) (@respectful_relation A B f y) *)
  intros b1 b2.
(* Goal: iff (@respectful_relation A B f x b1 b2) (@respectful_relation A B f y b1 b2) *)
  unfold respectful_relation.
(* Goal: iff (x (f b1) (f b2)) (y (f b1) (f b2)) *)
  apply H.
Defined.

Lemma respectful_compond_relation: forall {A B} (f: A -> B) R1 R2,
  inclusion _
    (compond_relation (respectful_relation f R1) (respectful_relation f R2))
    (respectful_relation f (compond_relation R1 R2)).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros.
(* Goal: inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros a1 a2 ?.
(* Goal: @respectful_relation A B f (@compond_relation B R1 R2) a1 a2 *)
  inversion H; subst.
(* Goal: @eq A n n *)
  apply compond_intro with (f y); auto.
Qed.

Definition partial_functional {A: Type} (R: relation A): Prop :=
  forall m n n', R m n -> R m n' -> n = n'.

Class PartialFunctional {A: Type} (R: relation A): Prop :=
  partial_functionality: forall m n n', R m n -> R m n' -> n = n'.

Definition functional {A: Type} (R: relation A): Prop :=
  forall m, exists n, forall n', R m n' <-> n' = n.

Class Functional {A: Type} (R: relation A): Prop :=
  functionality: forall m, exists n, forall n', R m n' <-> n' = n.

Definition serial {A: Type} (R: relation A): Prop :=
  forall m, exists n, R m n.

Class Serial {A: Type} (R: relation A): Prop :=
  seriality: forall m, exists n, R m n.

Lemma function_Functional {A: Type} {f: A -> A}: Functional (fun a => eq (f a)).
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  hnf; intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  exists (f m); intros.
(* Goal: iff (@eq A (f m) n') (@eq A n' (f m)) *)
  split; intros; congruence.
Qed.

Lemma SerialPartialFunctional_Functional {A: Type} {R: relation A}: Serial R -> PartialFunctional R -> Functional R.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros; hnf; intros.
(* Goal: @ex A (fun n : A => forall n' : A, iff (R m n') (@eq A n' n)) *)
  destruct (seriality m) as [n ?].
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  exists n; intros.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  split; intros.
(* Goal: @eq A n n *)
  + eapply partial_functionality; eauto.
(* Goal: @eq A n n *)
  + subst; auto.
Qed.

Instance Functional_PartialFunctional {A: Type} {R: relation A} {_: Functional R}: PartialFunctional R.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros; hnf; intros.
(* Goal: @eq A n n' *)
  destruct (functionality m) as [n0 ?].
(* Goal: @eq A n n' *)
  rewrite H2 in H0, H1.
(* Goal: @eq A n n' *)
  congruence.
Qed.

Instance Functional_Serial {A: Type} {R: relation A} {_: Functional R}: Serial R.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (R1 R2 : relation B), inclusion A (@compond_relation A (@respectful_relation A B f R1) (@respectful_relation A B f R2)) (@respectful_relation A B f (@compond_relation B R1 R2)) *)
  intros; hnf; intros.
(* Goal: @ex A (fun n : A => R m n) *)
  destruct (functionality m) as [n ?].
(* Goal: @ex A (fun n : A => R m n) *)
  exists n.
(* Goal: R m n *)
  rewrite H0.
(* Goal: @eq A n n *)
  auto.
Qed.

Class Inclusion {A: Type} (R1 R2: relation A) : Prop :=
  including: forall a b, R1 a b -> R2 a b.
