# Abstract Reduction Systems

Require Export Base.

Notation "p '<=1' q" := (forall 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" := (forall 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 => exists y, R x y /\ S y z.

Power predicates

Require Import Arith.

Definition it X f n x := @nat_iter n X f x.

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 := forall x, R x x.

Definition symmetric R := forall x y, R x y -> R y x.

Definition transitive R := forall x y z, R x y -> R y z -> R x z.

Definition functional R := forall 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.

Check star_ind.

Lemma star_simpl_ind R (p : X -> Prop) y :
p y ->
(forall x x', R x x' -> star R x' y -> p x' -> p x) ->
forall x, star R x y -> p x.

Proof.

intros A B.
induction 1; eauto.
Qed.

Goal forall R, transitive (star R).

Proof.

intros R x y z A B.
revert x A.
refine (star_simpl_ind _ _).

- exact B.

- intros x x' C D IH.

exact (starC C IH).

Qed.

Goal forall R, transitive (star R).

Proof.

intros R x y z A B.

induction A as [|x x' y C D IH].

- exact B.

-
specialize (IH B).

exact (starC C IH).

Qed.

Lemma star_trans R:
transitive (star R).

Proof.

induction 1; eauto using star.

Qed.

Lemma star_step R :
R <=2 star R.

Proof.

intros x y A.
econstructor. exact A. econstructor.
Qed.

Goal forall R, star (star R) <=2 star R.

Proof.

intros R x y.
revert x.
refine (star_simpl_ind _ _).

- apply starR.

- intros x x' B C IH.

exact (star_trans B IH).

Qed.

Right-to-left induction

Lemma star_right_ind R (p : X -> Prop) x :
p x ->
(forall y y', star R x y' -> p y' -> R y' y -> p y) ->
forall y, star R x y -> p y.

Proof.

intros A B y C.

induction C as [|x x' y D _ IH].

- exact A.

- apply IH; clear IH y.

+ apply (B x' x); auto using starR.

+ intros y y' E.
apply B. eauto using starC.
Qed.

Binary definition

Inductive rtc R : X -> X -> Prop :=
| rtcR x : rtc R x x
| rtcT x y z : rtc R x y -> rtc R y z -> rtc R x z
| rtcC x y : R x y -> rtc R x y.

Lemma star_rtc R :
star R =2 rtc R.

Proof.

split; intros x y A.

- induction A as [|x x' y C _ IH].

+ constructor.

+ apply rtcT with (y:=x').

* apply rtcC, C.

* exact IH.

- induction A as [|x x' y _ IHA _ IHB|x y A].

+ constructor.

+ eapply star_trans; eassumption.

+ apply star_step, A.

Qed.

Goal forall R, star R =2 rtc R.

Proof.

split.

- induction 1; eauto using rtc.

- induction 1; eauto using star, (@star_trans R).

Qed.

Goal forall R S, R =2 S -> star R =2 rtc S.

Proof.

intros R S [A B].
split.
- induction 1; eauto using rtc.

- induction 1; eauto using star, (@star_trans R).

Qed.

Power characterization

Lemma star_pow R x y :
star R x y <-> exists n, pow R n x y.

Proof.

split; intros A.

- induction A as [|x x' y B _ [n IH]].

+ exists 0.
reflexivity.
+ exists (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.

Normal forms

Definition reducible R x := exists y, R x y.

Definition normal R x := ~ reducible R x.

Definition NF R x y := star R x y /\ normal R y.

Definition WN R x := exists y, NF R x y.

Lemma star_normal R x y :
star R x y -> normal R x -> x = y.

Proof.

intros A B.
destruct A as [|x x' y A C]. reflexivity.
- exfalso.
apply B. exists x'. exact A.
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 :=
exists z, R x z /\ R y z.

Definition diamond R :=
forall x y z, R x y -> R x z -> joinable R y z.

Definition confluent R := diamond (star R).

Definition semi_confluent R :=
forall 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 forall 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.
exists 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).

exists u.
eauto using star.
Qed.

Proof.

intros A x y z B C.
revert y B.
induction C as [|x x' z D _ IH]; intros y B.

- exists y.
eauto using star.
- destruct (A _ _ _ B D) as [v [E F]].

destruct (IH _ F) as [u [G H]].

exists u.
eauto using star.
Qed.

Proof.

split; intros A x y z B C.

- revert y B.

induction C as [|x x' z D _ IH]; intros y B.

+ exists y.
eauto using star.
+ destruct (A _ _ _ D B) as [v [E F]].

destruct (IH _ E) as [u [G H]].

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

Qed.

Proof.

intros A x y z B C.

destruct C as [|x x' z D E].

- exists y.
eauto using star.
- assert (F:= A _ _ _ B D).
subst x'. exists z. eauto using star.
Qed.

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

+ exists x.
eauto using star.
+ destruct IH as [z [D E]].
exists z. eauto using star.
+ destruct IH as [u [D E]].

destruct (A _ _ _ C D) as [z [F G]].

exists z.
eauto using (@star_trans R).
Qed.

Lemma confluent_functional_NF R :
confluent R -> functional (NF R).

Proof.

intros A x y z [B C] [D E].

destruct (A _ _ _ B D) as [u [F G]].

apply (star_normal F) in C.

apply (star_normal G) in E.

congruence.

Qed.

Lemma CR_ecl_normal_NF R x y :
church_rosser R -> ecl R x y -> normal R y -> NF R x y.

Proof.

intros A B C.
apply A in B as [z [B D]].
assert (E := star_normal D C).
subst z.
hnf.
auto.
Qed.

Lemma CR_ecl_normal_eq R x y :
church_rosser R -> normal R x -> normal R y -> ecl R x y -> x = y.

Proof.

intros A B C D.
apply A in D as [z [E F]].
apply (star_normal E) in B.

apply (star_normal F) in C.

congruence.

Qed.

Triangle Property

Implicit Types rho : X -> X.

Definition triangle R rho := forall x y, R x y -> R y (rho x).

Lemma triangle_to_diamond R rho :
triangle R rho -> diamond R.

Proof.

intros T x y z A B.
exists (rho x). auto.
Qed.

# Strong Normalization

Inductive SN R : X -> Prop :=
| SNI : forall x, R x <=1 SN R -> SN R x.

Check SN_ind.

Goal forall R x, SN R x <-> R x <=1 SN R.

Proof.

split.

- intros A y B.
destruct A. auto.
- apply SNI.

Qed.

Goal forall R x, R x x -> SN R x -> False.

Proof.

intros R x A B.
induction B as [x B IH]. eauto.
Qed.

Lemma SN_induction R (p : X -> Prop) :
(forall x, R x <=1 SN R -> R x <=1 p -> p x) -> SN R <=1 p.

Proof.

exact (fun sigma => fix F x A :=
match A with
| SNI x' f => sigma x' f (fun y B => F y (f y B))
end).

Qed.

Definition locally_confluent R :=
forall x y z, R x y -> R x z -> joinable (star R) y z.

Lemma Newman R :
(forall x, SN R x) -> locally_confluent R -> confluent R.

Proof.

intros A B x.
specialize (A x). induction A as [x _ IH].
intros y z C D.

destruct C as [|x y' y C1 C2].

{ exists z.
eauto using star. }
destruct D as [|x z' z D1 D2].

{ exists y.
eauto using star. }
destruct (B _ _ _ C1 D1) as [u [E F]].

destruct (IH z' D1 u z F D2) as [v [G H]].

destruct (IH y' C1 y v C2) as [w [K L]].

{ eauto using (@star_trans R). }

exists w.
eauto using star, (@star_trans R).
Qed.

End FixX.

Hint Constructors star.

Hint Unfold reducible normal NF joinable.

Hint Resolve star_step (star_trans : forall X R x, _).

# Interpolation

Section Interpolation.

Variable X : Type.

Implicit Types R S : X -> X -> Prop.

Definition stable (p : (X -> X -> Prop) -> Prop) :=
forall R S, star R =2 star S -> p S -> p R.

Lemma confluent_stable :
stable (@confluent X).

Proof.

intros R S [A B] C x y z D E.

apply A in D.
apply A in E.
destruct (C _ _ _ D E) as [u [F G]].

exists u.
auto.
Qed.

Lemma star_mono R S :
R <=2 S -> star R <=2 star S.

Proof.

intros A x y B.
induction B ; eauto.
Qed.

Lemma star_least R S :
R <=2 S -> reflexive S -> transitive S -> star R <=2 S.

Proof.

intros A B C.
induction 1 ; eauto.
Qed.

Lemma star_idempotent R :
star (star R) =2 star R.

Proof.

split.

- apply (star_least (R := star R)); hnf; eauto.

- auto.

Qed.

Lemma interpolation R S :
R <=2 S -> S <=2 star R -> star R =2 star S.

Proof.

intros A B.
split; intros x y C.
- apply (star_mono A), C.

- apply star_idempotent.
apply (star_mono B), C.
Qed.

End Interpolation.

# Evaluation

Section Evaluation_Defs.

Variable X : Type.

Implicit Types R : X -> X -> Prop.

Implicit Types rho : X -> X.

Definition eval R rho x y := exists n, it rho n x = y /\ normal R y.

Definition sound R rho := forall x, star R x (rho x).

Definition cofinal R rho := forall x y, star R x y -> exists n, star R y (it rho n x).

Definition FP rho n x := it rho (S n) x = it rho n x.

Lemma sound_stable rho :
stable (fun R => @sound R rho).

Proof.

intros R S [A B] C x.
apply B, C.
Qed.

Lemma cofinal_stable rho :
stable (fun R => @cofinal R rho).

Proof.

intros R S [A B] C x y D.
apply A in D. apply C in D as [n D]. eauto.
Qed.

End Evaluation_Defs.

Hint Unfold eval.

Section Evaluation.

Variable X : Type.

Variable R : X -> X -> Prop.

Variable rho : X -> X.

Section Triangle.

Variable T : triangle R rho.

Lemma triangle_to_sound :
reflexive R -> sound R rho.

Proof.

intros A x.
specialize (A x). apply T in A. auto.
Qed.

Lemma triangle_rect x y :
R x y -> R (rho x) (rho y).

Proof.

intros A.
apply T. apply T. exact A.
Qed.

Lemma triangle_rect_it x y n :
R x y -> R (it rho n x) (it rho n y).

Proof.

intros A.
induction n. exact A.
apply triangle_rect, IHn.

Qed.

Proof.

intros x y A.
induction A as [y|x x' y B A IH].
- exists 0.
constructor.
- destruct IH as [n IH].

apply (triangle_rect_it n) in B.
apply T in B.
exists (S n).
eauto.
Qed.

End Triangle.

Lemma FP_stat x m n :
FP rho m x -> m <= n -> it rho m x = it rho n x.

Proof.

intros A B.
induction B as [|n _ IH].
- reflexivity.

- hnf in A.
rewrite <- A.
change (rho (it rho m x) = rho (it rho n x)).
congruence.
Qed.

Lemma FP_unique m n x :
FP rho m x -> FP rho n x -> it rho m x = it rho n x.

Proof.

intros A B.
destruct (le_ge_dec m n) as [C|C].
- apply FP_stat; assumption.

- symmetry.
apply FP_stat; assumption.
Qed.

Lemma it_plus m n x :
it rho m (it rho n x) = it rho (m + n) x.

Proof.

revert n.
induction m as [|m]; intros n. reflexivity.
unfold it.
simpl. f_equal. apply IHm.
Qed.

Variable Sound : sound R rho.

Lemma it_sound x n :
star R x (it rho n x).

Proof.

induction n.
now constructor.
change (star R x (rho (it rho n x))).

generalize (Sound (it rho n x)).
eauto.
Qed.

Lemma normal_FP x :
normal R x -> rho x = x.

Proof.

intros A.

assert (B := Sound x).
symmetry. apply (star_normal B A).
Qed.

Lemma it_le m n x :
m <= n -> star R (it rho m x) (it rho n x).

Proof.

intros A.
induction A as [|n _ IH]. now constructor.
apply (star_trans IH).
exact (@it_sound _ 1).
Qed.

Lemma eval_functional :
functional (eval R rho).

Proof.

intros x y y' [m [A' A]] [n [B' B]].
subst y y'.
apply normal_FP in A.
apply normal_FP in B.
apply FP_unique; assumption.

Qed.

Variable Cofinal : cofinal R rho.

Lemma eval_correct :
eval R rho =2 NF R.

Proof.

split; intros x y.

- intros [n [A B]].
subst y. split.
+ apply it_sound.

+ exact B.

- intros [A B].
apply Cofinal in A as [n A].
apply star_normal in A.

+ subst y.
eauto.
+ exact B.

Qed.

Lemma rho_to_confluent :
confluent R.

Proof.

intros x y z B C.

apply Cofinal in B as [m B].

apply Cofinal in C as [n C].

destruct (le_ge_dec m n) as [D|D];
apply (it_le x) in D; eauto.

Qed.

Lemma rho_to_not_WN x :
rho x = x -> reducible R x -> ~ WN R x.

Proof.

intros A B [y C].

cut (x = y).

{ intros D; subst y.
apply C. exact B. }
apply eval_correct in C as [m [C D]].
subst y.
apply normal_FP in D.

exact (@FP_unique 0 m x A D).

Qed.

End Evaluation.