Require Import Arith.
Require Import Lt.
Require Import Bool.
Require Import Omega.
Require Import pseudo_term.

(* from Barendregt's book*)
(* General facts about confluency *)
Section Confluency.
Variable R1 : Term -> Term -> Prop.
Variable R2 : Term -> Term -> Prop.

Variable R1comm : forall x y y', R1 x y -> R1 x y' -> exists z, R1 y z /\ R1  y' z.
Variable R2comm : forall x y y', R2 x y -> R2 x y' -> exists z, R2 y z /\ R2  y' z.
Variable R1R2 : forall x y y', R1 x y -> R2 x y' -> exists z, R2 y z /\ R1  y' z.

Inductive union : Term -> Term -> Prop :=
 | uR1 : forall x y, R1 x y -> union x y
 | uR2 : forall x y, R2 x y -> union x y.

Inductive cloture : nat -> Term -> Term -> Prop :=
 | clot_refl : forall x, cloture 0 x x
 | clot_one : forall x y, union x y -> cloture 1 x y
 | clot_trans : forall n x y z, union x y -> cloture n y z -> cloture (S n) x z.

Hint Constructors union cloture.
Hint Resolve R1comm R2comm R1R2.

Theorem comm_union : forall x y y', union x y -> union x y' -> 
  exists z,union y z /\ union y' z.
intros.
destruct H; destruct H0.
destruct (R1comm x y y0 H H0) as (z & ? & ?); exists z; intuition.
destruct (R1R2 x y y0 H H0) as (z & ? & ?); exists z; intuition.
destruct (R1R2 x y0 y H0 H) as (z & ? & ?); exists z; intuition.
destruct (R2comm x y y0 H H0) as (z & ? & ?); exists z; intuition.
Qed.


Theorem comm_cloture_onestep : forall x y y' n, union x y -> cloture n x y' -> 
  exists z,cloture n y z /\ union y' z.
intros x y y' n H H'; generalize y H; clear y H. 
induction H'; intros.
exists y; intuition.
destruct (comm_union x y y0 H H0) as (z & ? & ?).
exists z; intuition.
destruct (comm_union x y y0 H H0) as (w & ? & ?).
destruct (IHH' w  H1) as (w' & ? & ?).
eauto.
Qed.



Theorem comm_cloture : forall n p x y y', cloture n x y -> cloture p x y' -> 
  exists z,cloture p y z /\ cloture n y' z.
induction n; intros.
inversion H; subst; clear H.
exists y'; intuition.
inversion H; subst; clear H.
destruct (comm_cloture_onestep x y y' p H2 H0) as (w & ? & ?).
exists w;  intuition.
destruct (comm_cloture_onestep x y0 y' p H2 H0) as (w & ? & ?).
destruct (IHn p y0 y w H3 H) as (w' & ? & ?).
exists w'; eauto.
Qed.

End Confluency.

(* Instantiate the previous section with R1 == Betas R1comm = Betas_diamond
 R2 == Etas   R2comm == Etas_diamond R1R2 = switch

and we get what we wanted *)