(* (c) 2017, Jonas Kaiser *)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Notation "R <<= S" := (forall x y, R x y -> S x y) (at level 70, no associativity).
Notation "R === S" := (R <<= S /\ S <<= R) (at level 70, no associativity).

Definition Pred T := T -> Prop.
Definition Rel T := T -> Pred T.

Definition reflexive T (R : Rel T) := forall x, R x x.
Definition symmetric T (R : Rel T) := forall x y, R x y -> R y x.
Definition transitive T (R : Rel T) := forall x y z, R x y -> R y z -> R x z.
Definition equivalence T (R : Rel T) := reflexive R /\ symmetric R /\ transitive R.

(* We use composite to capture a number transitivity like properties *)
Definition composite T (R S U : Rel T) := forall x y z, R x y -> S y z -> U x z.

Lemma subT X (R S T : Rel X) : R <<= S -> S <<= T -> R <<= T.
Proof. firstorder. Qed.

(* Inverse Relation *)
Definition inverse {T} (R : Rel T) (y x : T) := R x y.

(* Joinable terms *)
Definition joinable {T} (R : Rel T) (x y : T) := exists2 z, R x z & R y z.

(* joinable is symmetric *)
Lemma joinableS {T} (R : Rel T) : symmetric (joinable R).
Proof. intros x y [z H1 H2]. exists z; trivial. Qed.

(* Definition liftRel {U T} (R : Rel T) : Rel (U -> T) := fun f g : U -> T => forall x : U, R (f x) (g x). *)

Section Definitions.

  Variables (X : Type) (R : Rel X).
  Implicit Types (R : Rel X) (x y z : X) (rho : X -> X).

  Inductive star : Rel X :=
  | starR x : star x x
  | starRS x y z : R x y -> star y z -> star x z.

  Inductive conv x : Pred X :=
  | convR : conv x x
  | convCR y z : conv x y -> R y z -> conv x z
  | convCRi y z : conv x y -> R z y -> conv x z.

  Hint Resolve starR convR.

  (* Definition com R S := forall x y z, R x y -> S x z -> exists2 u, S y u & R z u. *)

  (* Properties of star. *)
  Lemma star1 : R <<= star.
  Proof. intros x y Rxy. eapply starRS; eauto. Qed.

  Lemma starT : transitive star.
  Proof. intros x y z. induction 1; eauto using star. Qed.

  Lemma starSR : composite star R star.
  Proof. intros x y z Sxy Ryz. eapply starT; eauto using star1. Qed.

  (* Properties of conv *)
  Lemma conv1 : R <<= conv.
  Proof. intros x y. now apply convCR. Qed.

  Lemma conv1i : inverse R <<= conv.
  Proof. intros x y. now apply convCRi. Qed.

  Lemma convT : transitive conv.
  Proof. intros x y z. induction 2; eauto using conv. Qed.

  Lemma convRC : composite R conv conv.
  Proof. intros x y z Rxy. now apply convT, conv1. Qed.

  Lemma convRCi : composite (inverse R) conv conv.
  Proof. intros x y z Ryx. now apply convT, conv1i. Qed.

  Lemma convS : symmetric conv.
  Proof. intros x y. induction 1; eauto using convRC, convRCi. Qed.

  Lemma convE : equivalence conv.
  Proof. now split; auto using convS, convT. Qed.

  Lemma convTi : composite (inverse conv) conv conv.
  Proof. intros x y z Cyx. now apply convT, convS. Qed.

  (* Properties of star and conv *)
  Lemma star_conv : star <<= conv.
  Proof. intros x y. induction 1; eauto using conv, convT. Qed.

  Lemma join_conv : joinable star <<= conv.
  Proof. intros x y [z Sxy Szy]. eapply convT; [|apply convS]; apply star_conv; eassumption. Qed.

  (* Further properties of relations *)
  Definition diamond := forall x y z, R x y -> R x z -> joinable R y z.
  Definition semiconfluent := forall x y z, star x y -> R x z -> joinable star y z.
  Definition confluent := forall x y z, star x y -> star x z -> joinable star y z.
  Definition CR := forall x y, conv x y -> joinable star x y.

  (* When R has a triangle function, then R is confluent, via diamond and semiconfluence *)
  Definition triangle rho := forall x y, R x y -> R y (rho x).

  Lemma triangle_diamond rho : triangle rho -> diamond.
  Proof. intros T x y z Rxy Rxz. exists (rho x); auto. Qed.

  Lemma diamond_semiconfluent : diamond -> semiconfluent.
  Proof.
    intros D. intros x y z H; revert z. induction H; intros w H'.
    - exists w; trivial. now apply star1.
    - destruct (D _ _ _ H H') as [v Ryv Rwv].
      destruct (IHstar _ Ryv) as [u Szu Svu].
      assert (Swu : star w u) by eauto using star. now exists u.
  Qed.

  Lemma semiconfluent_confluent : semiconfluent -> confluent.
  Proof.
    intros S. intros x y z H; revert z. induction H; intros w H'.
    - exists w; trivial.
    - destruct (S _ _ _ H' H) as [v Swv Syv].
      destruct (IHstar _ Syv) as [u Szu Svu].
      assert (Swu : star w u) by eauto using star, starT. now exists u.
  Qed.

  Theorem diamond_confluent : diamond -> confluent.
  Proof. intros D. now apply semiconfluent_confluent, diamond_semiconfluent. Qed.

  Theorem triangle_confluent rho : triangle rho -> confluent.
  Proof. intros T. now apply diamond_confluent, (@triangle_diamond rho). Qed.

  (* Confluence and Church Rosser *)
  Lemma semiconfluent_CR : semiconfluent -> CR.
  Proof.
    intros S x y H. induction H.
    - exists x; trivial.
    - destruct IHconv as [w Sxw Syw].
      destruct (S _ _ _ Syw H0) as [v Swv Szv].
      assert (Sxv : star x v) by eauto using star, starT. exists v; trivial.
    - destruct IHconv as [w Sxw Syw].
      assert (Szw : star z w) by eauto using star. exists w; trivial.
  Qed.

  Lemma CR_confluent : CR -> confluent.
  Proof. intros J x y z Sxy Sxz. apply J. eapply convT; [apply convS|]; apply star_conv; eassumption. Qed.

  Lemma confluent_semiconfluent : confluent -> semiconfluent.
  Proof. intros C x y z H1 H2. eapply C; eauto using star1. Qed.

  Lemma confluent_CR: confluent -> CR.
  Proof. intros C. now apply semiconfluent_CR, confluent_semiconfluent. Qed.

End Definitions.

Hint Resolve starR convR.
Arguments starT {X R x} y {z} A B.
Arguments convT {X R x} y {z} A B.

Lemma diamond_star_confluent X (R : Rel X) : diamond (star R) = confluent R.
Proof. reflexivity. Qed.

Lemma star_monotone X (R S : Rel X) : R <<= S -> (star R) <<= (star S).
Proof. intros H x y J. induction J; eauto using star. Qed.

Lemma star_idem X (R : Rel X) : (star (star R)) <<= (star R).
Proof. intros x y H. induction H; trivial. now apply (starT y). Qed.

Lemma star_interpolate X (R S : Rel X) : R <<= S -> S <<= star R -> star S === star R.
Proof.
  intros RS SsR. split.
  - now eapply subT; [apply star_monotone|apply star_idem].
  - now apply star_monotone.
Qed.

Lemma eq_diamond X (R S : Rel X) : diamond R -> R === S -> diamond S.
Proof.
  intros D [subRS subSR] x y z Sxy Sxz.
  destruct (D _ _ _ (subSR _ _ Sxy) ((subSR _ _ Sxz))) as [w Ryw zw].
  exists w; now apply subRS.
Qed.

Theorem TTML_confluence X (R pR : Rel X) (rho : X -> X) : R <<= pR -> pR <<= (star R) -> triangle pR rho -> confluent R.
Proof.
  intros S1 S2 T. rewrite <- diamond_star_confluent.
  eapply eq_diamond; [eapply triangle_confluent|apply star_interpolate]; eassumption.
Qed.

(* when R preserves property P, then so does star R *)
Lemma starL X (R : Rel X) (P : X -> Prop) :
  (forall x y, R x y -> P x -> P y) ->
  forall x y, star R x y -> P x -> P y.
Proof. intros H x y J. induction J; intros K; eauto. Qed.

Lemma star_proper X f (R : Rel X) :
  (forall x y, R x y -> R (f x) (f y)) ->
  forall x y, star R x y -> star R (f x) (f y).
Proof. intros A x y H. induction H; eauto using star. Qed.

Lemma star_proper2 X g (R : Rel X) :
  (forall x y z, R x y -> R (g x z) (g y z)) ->
  (forall x y z, R y z -> R (g x y) (g x z)) ->
  forall x x' y y', star R x x' -> star R y y' -> star R (g x y) (g x' y').
Proof.
  intros A B x x' y y' Sxx' Syy'. apply starT with (y0:=(g x y')).
  - apply star_proper; auto.
  - revert x x' Sxx'. apply star_proper. auto.
Qed.

Lemma conv_proper X f (R : Rel X) :
  (forall x y, R x y -> R (f x) (f y)) ->
  forall x y, conv R x y -> conv R (f x) (f y).
Proof. intros A x y H. induction H; eauto using conv. Qed.

Lemma conv_proper2 X g (R : Rel X) :
  (forall x y z, R x y -> R (g x z) (g y z)) ->
  (forall x y z, R y z -> R (g x y) (g x z)) ->
  forall x x' y y', conv R x x' -> conv R y y' -> conv R (g x y) (g x' y').
Proof.
  intros A B x x' y y' Cxx' Cyy'. apply (convT (g x y')).
  - auto using conv_proper.
  - revert x x' Cxx'. apply conv_proper. auto.
Qed.

Lemma star_proper2_inv X g (R: Rel X):
  (forall x1 y1 z, R (g x1 y1) z -> (exists x2, z = g x2 y1 /\ R x1 x2) \/ (exists y2, z = g x1 y2 /\ R y1 y2)) ->
  forall x1 y1 z, star R (g x1 y1) z -> exists x2 y2, z = g x2 y2 /\ star R x1 x2 /\ star R y1 y2.
Proof.
  intros A x1 y1 z H. remember (g x1 y1) as w. revert x1 y1 Heqw. induction H; intros x1 y1 E1.
  - subst. exists x1, y1. repeat split; auto.
  - subst. apply A in H as [[x2 [E H]]|[y2 [E H]]]; subst.
    + destruct (IHstar _ _ (eq_refl _)) as [x3 [y3 [E3 [IH1 IH2]]]].
      exists x3, y3. split; trivial. split; eauto using star.
    + destruct (IHstar _ _ (eq_refl _)) as [x3 [y3 [E3 [IH1 IH2]]]].
      exists x3, y3. split; trivial. split; eauto using star.
Qed.

(* Section StarConstr2Inv. *)

(*   Variable X Y Z : Type. *)
(*   Variable R : Rel X. *)
(*   Variable S : Rel Y. *)
(*   Variable T : Rel Z. *)
(*   Variable c : X -> Y -> Z. *)

(*   Variable CGR : forall x1 y1 z, T (c x1 y1) z -> (exists x2, z = c x2 y1 /\ R x1 x2) \/ (exists y2, z = c x1 y2 /\ S y1 y2). *)

(*   Lemma star_constr_2_inv x1 y1 z : *)
(*     star T (c x1 y1) z -> exists x2 y2, z = c x2 y2 /\ star R x1 x2 /\ star S y1 y2. *)
(*   Proof. *)
(*     intros H. remember (c x1 y1) as w. *)
(*     revert x1 y1 Heqw. induction H; intros x1 y1 E1. *)
(*     - subst. exists x1, y1. repeat split; auto. *)
(*     - subst. apply CGR in H as [x2 [E HR]]|[y2 [E HS]]; subst. *)
(*       + destruct (IHstar _ _ (eq_refl _)) as x3 [y3 [E3 [IHR IHS]]]. *)
(*         exists x3, y3. split; trivial. split; eauto using star. *)
(*       + destruct (IHstar _ _ (eq_refl _)) as x3 [y3 [E3 [IHR IHS]]]. *)
(*         exists x3, y3. split; trivial. split; eauto using star. *)
(*   Qed. *)

(* End StarConstr2Inv. *)