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

Notation "p '<=1' q" := ( x, p xq 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 yS 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 : XYProp) (S : YZProp)
: XZProp :=
fun x z y, R x y S y z.

Power predicates

Definition pow X R n : XXProp := it (rcomp R) n eq.

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

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

Reflexive transitive closure

Inductive star R : XXProp :=
| starR x : star R x x
| starC x y z : R x ystar R y zstar R x z.

Lemma star_simpl_ind R (p : XProp) y :
p y
( x x', R x x'star R x' yp x'p x) →
x, star R x yp x.

Lemma star_trans R:
transitive (star R).

Power characterization

Lemma star_pow R x y :
star R x y n, pow R n x y.

Equivalence closure

Inductive ecl R : XXProp :=
| eclR x : ecl R x x
| eclC x y z : R x yecl R y zecl R x z
| eclS x y z : R y xecl R y zecl R x z.

Lemma ecl_trans R :
transitive (ecl R).

Lemma ecl_sym R :
symmetric (ecl R).

Lemma star_ecl R :
star R <=2 ecl R.

Diamond, confluence, Church-Rosser

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

Definition diamond R :=
x y z, R x yR x zjoinable R y z.

Definition confluent R := diamond (star R).

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

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

Goal R, diamond Rsemi_confluent R.

Lemma diamond_to_semi_confluent R :
diamond Rsemi_confluent R.

Lemma semi_confluent_confluent R :
semi_confluent R confluent R.

Lemma diamond_to_confluent R :
diamond Rconfluent R.

Lemma confluent_CR R :
church_rosser R confluent R.

Uniform confluence and parametrized confluence

Definition uniform_confluent (R : XXProp ) := s t1 t2, R s t1R s t2t1 = t2 u, R t1 u R t2 u.

Lemma pow_add R n m (s t : X) : pow R (n + m) s t rcomp (pow R n) (pow R m) s t.

Lemma rcomp_eq (R S R' S' : XXProp) (s t : X) : (R =2 R') → (S =2 S') → (rcomp R S s t rcomp R' S' s t).

Lemma eq_ref : (R : XXProp), R =2 R.

Lemma rcomp_1 (R : XXProp): R =2 pow R 1.

Lemma parametrized_semi_confluence (R : XXProp) (m : nat) (s t1 t2 : X) :
uniform_confluent R
pow R m s t1
R s t2
k l u,
k 1 l m pow R k t1 u pow R l t2 u m + k = S l.

Lemma rcomp_comm R m (s t : X) : rcomp R (it (rcomp R) m eq) s t rcomp (it (rcomp R) m eq) R s t.

Lemma parametrized_confluence (R : XXProp) (m n : nat) (s t1 t2 : X) :
uniform_confluent R
pow R m s t1
pow R n s t2
k l u,
k n l m pow R k t1 u pow R l t2 u m + k = n + l.

End FixX.