Library CR

Church Rosser Property and Cofinality of Parallel Reduction Operator


Require Import ARS LC_Basis.


Setoid instances for reduction.


Instance red_PreOrder : PreOrder (star step).

Proof.

  constructor; hnf.

  - apply starR.

  - apply star_trans.

Qed.


Instance red_app_proper :
  Proper (star step ==> star step ==> star step) App.

Proof.

  cbv.
intros s s' A t t' B. transitivity (s' t).
  - induction A; eauto using star, step.

  - induction B; eauto using star, step.

Qed.


Instance red_lam_proper :
  Proper (star step ==> star step) Lam.

Proof.

  cbv.
intros s s' A. induction A; eauto using star, step.
Qed.


Parallel Reduction and Cofinality


Fixpoint rho (s : term) : term :=
  match s with
    | Var n => Var n
    | App (Lam s) t => beta (rho t) ! rho s
    | App s t => App (rho s) (rho t)
    | Lam s => Lam (rho s)
  end.


Inductive pstep : term -> term -> Prop :=
| pstepV n :
    pstep (Var n) (Var n)
| pstepA s s' t t' :
    pstep s s' ->
    pstep t t' ->
    pstep (App s t) (App s' t')
| pstepL s s' :
    pstep s s' ->
    pstep (Lam s) (Lam s')
| pstepB s s' t t' :
    pstep s s' ->
    pstep t t' ->
    pstep (App (Lam s) t) (beta t' ! s').


Lemma pstep_refl :
  reflexive pstep.

Proof.

  intros s.
induction s ; auto using pstep.
Qed.


Lemma step_pstep :
  step <=2 pstep.

Proof.

  induction 1; auto using pstep, pstep_refl.

Qed.


Lemma pstep_step :
  pstep <=2 star step.

Proof.

  intros s t A.
induction A.
  - reflexivity.

  - rewrite IHA1, IHA2.
constructor.
  - rewrite IHA.
constructor.
  - rewrite IHA1, IHA2.
eauto using star, step.
Qed.


Lemma red_agrees :
  star step =2 star pstep.

Proof.

  apply interpolation.

  - apply step_pstep.

  - apply pstep_step.

Qed.


Lemma pstep_substitutive sigma s t :
  pstep s t -> pstep (sigma ! s) (sigma ! t).

Proof.

  intros A.
revert sigma.
  induction A as [n | s s' t t' _ IHs _ IHt | s s' _ IHs
                  | s s' t t' _ IHs _ IHt ];
    simpl ; intros sigma.

  - apply pstep_refl.

  - constructor; auto.

  - constructor; auto.

  - rewrite subst_beta_com.
constructor; auto.
Qed.


Definition psstep (sigma tau : substitution) : Prop :=
  forall n, pstep (sigma n) (tau n).


Lemma pstep_up sigma tau :
  psstep sigma tau -> psstep (up sigma) (up tau).

Proof.

  intros A [|n] ; simpl.

  - constructor.

  - do 2 rewrite subst_ren.
apply pstep_substitutive, A.
Qed.


Lemma pstep_compatible sigma tau s s' :
  psstep sigma tau -> pstep s s' -> pstep (sigma ! s) (tau ! s').

Proof.

  intros A B.
revert sigma tau A.
  induction B as [n | s s' t t' _ IHs _ IHt | s s' _ IHs
                  | s s' t t' _ IHs _ IHt ];
    simpl ; intros sigma tau A.

  - apply A.

  - constructor; auto.

  - constructor.
apply IHs. apply pstep_up, A.
  - rewrite subst_beta_com.
constructor.
    + apply IHs.
apply pstep_up, A.
    + auto.

Qed.


Lemma triangle_pstep_rho :
  triangle pstep rho.

Proof.

  intros s s' A.

  induction A as [n | s s' t t' As IHs _ IHt | s s' _ IHs
                  | s s' t t' _ IHs _ IHt ].

  - constructor.

  - destruct s as [n |u v|u].

    + constructor; assumption.

    + constructor; assumption.

    + inv As.
simpl. inv IHs. constructor; assumption.
  - constructor; assumption.

  - simpl.
apply pstep_compatible.
    + intros [|n] ; simpl.
exact IHt. constructor.
    + exact IHs.

Qed.


Lemma rho_sound :
  sound step rho.

Proof.

  apply sound_stable with (S := pstep).

  exact red_agrees.

  apply triangle_to_sound.

  exact triangle_pstep_rho.

  exact pstep_refl.

Qed.


Lemma rho_cofinal :
  cofinal step rho.

Proof.

  apply cofinal_stable with (S := pstep).

  exact red_agrees.

  apply triangle_to_cofinal.

  exact triangle_pstep_rho.

Qed.


Church Rosser Property


Theorem CR :
  church_rosser step.

Proof.

  apply confluent_CR.

  eapply rho_to_confluent.

  exact rho_sound.

  exact rho_cofinal.

Qed.


Alternatively, CR follows directly from the triangle property, but cofinality of rho is a useful property in its own right.