# Abstract Reduction Systems, from Semantics Lecture at Programming Systems Lab, https://www.ps.uni-saarland.de/courses/sem-ws13/

Require Export Base.

Notation "p '<=1' q" := ( x, p x q x) (at level 70).
Notation "p '=1' q" := (p <=1 q q <=1 p) (at level 70).
Notation "R '<=2' S" := ( x y, R x y S x y) (at level 70).
Notation "R '=2' S" := (R <=2 S S <=2 R) (at level 70).

Relational composition

Definition rcomp X Y Z (R : X Y Prop) (S : Y Z Prop)
: X Z Prop :=
fun x z y, R x y S y z.

Power predicates

Require Import Arith.
Definition pow X R n : X X Prop := it (rcomp R) n eq.

Section FixX.
Variable X : Type.
Implicit Types R S : X X Prop.
Implicit Types x y z : X.

Definition reflexive R := x, R x x.
Definition symmetric R := x y, R x y R y x.
Definition transitive R := x y z, R x y R y z R x z.
Definition functional R := x y z, R x y R x z y = z.

Reflexive transitive closure

Inductive star R : X X Prop :=
| starR x : star R x x
| starC x y z : R x y star R y z star R x z.

Lemma star_simpl_ind R (p : X Prop) y :
p y
( x x', R x x' star R x' y p x' p x)
x, star R x y p x.
Proof.
intros A B. induction 1; eauto.
Qed.

Lemma star_trans R:
transitive (star R).
Proof.
induction 1; eauto using star.
Qed.

Power characterization

Lemma star_pow R x y :
star R x y n, pow R n x y.
Proof.
split; intros A.
- induction A as [|x x' y B _ [n IH]].
+ 0. reflexivity.
+ (S n), x'. auto.
- destruct A as [n A].
revert x A. induction n; intros x A.
+ destruct A. constructor.
+ destruct A as [x' [A B]]. econstructor; eauto.
Qed.

Lemma pow_star R x y n:
pow R n x y star R x y.
Proof.
intros A. erewrite star_pow. eauto.
Qed.

Equivalence closure

Inductive ecl R : X X Prop :=
| eclR x : ecl R x x
| eclC x y z : R x y ecl R y z ecl R x z
| eclS x y z : R y x ecl R y z ecl R x z.

Lemma ecl_trans R :
transitive (ecl R).
Proof.
induction 1; eauto using ecl.
Qed.

Lemma ecl_sym R :
symmetric (ecl R).
Proof.
induction 1; eauto using ecl, (@ecl_trans R).
Qed.

Lemma star_ecl R :
star R <=2 ecl R.
Proof.
induction 1; eauto using ecl.
Qed.

Diamond, confluence, Church-Rosser

Definition joinable R x y :=
z, R x z R y z.

Definition diamond R :=
x y z, R x y R x z joinable R y z.

Definition confluent R := diamond (star R).

Definition semi_confluent R :=
x y z, R x y star R x z joinable (star R) y z.

Definition church_rosser R :=
ecl R <=2 joinable (star R).

Goal R, diamond R semi_confluent R.
Proof.
intros R A x y z B C.
revert x C y B.
refine (star_simpl_ind _ _).
- intros y C. y. eauto using star.
- intros x x' C D IH y E.
destruct (A _ _ _ C E) as [v [F G]].
destruct (IH _ F) as [u [H I]].
assert (J:= starC G H).
u. eauto using star.
Qed.

Lemma diamond_to_semi_confluent R :
diamond R semi_confluent R.
Proof.
intros A x y z B C. revert y B.
induction C as [|x x' z D _ IH]; intros y B.
- y. eauto using star.
- destruct (A _ _ _ B D) as [v [E F]].
destruct (IH _ F) as [u [G H]].
u. eauto using star.
Qed.

Lemma semi_confluent_confluent R :
semi_confluent R confluent R.
Proof.
split; intros A x y z B C.
- revert y B.
induction C as [|x x' z D _ IH]; intros y B.
+ y. eauto using star.
+ destruct (A _ _ _ D B) as [v [E F]].
destruct (IH _ E) as [u [G H]].
u. eauto using (@star_trans R).
- apply (A x y z); eauto using star.
Qed.

Lemma diamond_to_confluent R :
diamond R confluent R.
Proof.
intros A. apply semi_confluent_confluent, diamond_to_semi_confluent, A.
Qed.

Lemma confluent_CR R :
church_rosser R confluent R.
Proof.
split; intros A.
- intros x y z B C. apply A.
eauto using (@ecl_trans R), star_ecl, (@ecl_sym R).
- intros x y B. apply semi_confluent_confluent in A.
induction B as [x|x x' y C B IH|x x' y C B IH].
+ x. eauto using star.
+ destruct IH as [z [D E]]. z. eauto using star.
+ destruct IH as [u [D E]].
destruct (A _ _ _ C D) as [z [F G]].
z. eauto using (@star_trans R).
Qed.

Lemma pow_add R n m (x y : X) : pow R (n + m) x y rcomp (pow R n) (pow R m) x y.
Proof.
revert m x y; induction n; intros m x y.
- simpl. split; intros. econstructor. split. unfold pow. simpl. reflexivity. eassumption.
destruct H as [u [H1 H2]]. unfold pow in H1. simpl in ×. subst x. eassumption.
- simpl in *; split; intros.
+ destruct H as [u [H1 H2]].
change (it (rcomp R) (n + m) eq) with (pow R (n+m)) in H2.
rewrite IHn in H2.
destruct H2 as [u' [A B]]. unfold pow in A.
econstructor.
split. econstructor. repeat split; repeat eassumption. eassumption.
+ destruct H as [u [H1 H2]].
destruct H1 as [u' [A B]].
econstructor. split. eassumption. change (it (rcomp R) (n + m) eq) with (pow R (n + m)).
rewrite IHn. econstructor. split; eassumption.
Qed.

Lemma rcomp_1 (R : X X Prop): R =2 pow R 1.
Proof.
split; intros x t; unfold pow in *; simpl in *; intros H.
- t. tauto.
- destruct H as [u [H1 H2]]; subst u; eassumption.
Qed.

End FixX.

Instance star_PreOrder X (R:X X Prop): PreOrder (star R).
Proof.
constructor; hnf.
- eapply starR.
- eapply star_trans.
Qed.

Instance ecl_equivalence X (R:X X Prop): Equivalence (ecl R).
Proof.
constructor; hnf.
- apply eclR.
- apply ecl_sym.
-apply ecl_trans.
Qed.

Instance R_star_subrelation X (R:X X Prop): subrelation R (star R).
Proof.
intros s t st. eauto using star.
Qed.

Instance pow_star_subrelation X (R:X X Prop) n: subrelation (pow R n) (star R).
Proof.
intros ? ?. apply pow_star.
Qed.

Instance star_ecl_subrelation X (R:X X Prop) : subrelation (star R) (ecl R).
Proof.
intros ? ?. apply star_ecl.
Qed.

Instance R_ecl_subrelation X (R:X X Prop): subrelation R (ecl R).
Proof.
intros ? ? ?. apply star_ecl_subrelation. now apply R_star_subrelation.
Qed.