# 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.

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.

Lemma pow_star R x y n:
pow R n x y star R x y.

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).

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 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.

Lemma diamond_to_semi_confluent R :
diamond R semi_confluent R.

Lemma semi_confluent_confluent R :
semi_confluent R confluent R.

Lemma diamond_to_confluent R :
diamond R confluent R.

Lemma confluent_CR R :
church_rosser R confluent R.

Lemma pow_add R n m (x y : X) : pow R (n + m) x y rcomp (pow R n) (pow R m) x y.

Lemma rcomp_1 (R : X X Prop): R =2 pow R 1.

End FixX.

Instance star_PreOrder X (R:X X Prop): PreOrder (star R).

Instance ecl_equivalence X (R:X X Prop): Equivalence (ecl R).

Instance R_star_subrelation X (R:X X Prop): subrelation R (star R).

Instance pow_star_subrelation X (R:X X Prop) n: subrelation (pow R n) (star R).

Instance star_ecl_subrelation X (R:X X Prop) : subrelation (star R) (ecl R).

Instance R_ecl_subrelation X (R:X X Prop): subrelation R (ecl R).