Library CoC_ChurchRosser

Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_BetaStar.

Additional Definitions Used in this Proof


Definition of parallel reduction

Inductive para : relation :=
  | para_red : forall L t1 t2 t2' u u',
      term t1 ->
      (forall x, x \notin L -> para (t2 ^ x) (t2' ^ x) ) ->
      para u u' ->
      para (trm_app (trm_abs t1 t2) u) (t2' ^^ u')
  | para_var : forall x,
      para (trm_fvar x) (trm_fvar x)
  | para_srt : forall n,
      para (trm_type n) (trm_type n)
  | para_app : forall t1 t1' t2 t2',
      para t1 t1' ->
      para t2 t2' ->
      para (trm_app t1 t2) (trm_app t1' t2')
  | para_abs : forall L t1 t1' t2 t2',
     para t1 t1' ->
     (forall x, x \notin L -> para (t2 ^ x) (t2' ^ x) ) ->
     para (trm_abs t1 t2) (trm_abs t1' t2')
  | para_prod : forall L t1 t1' t2 t2',
     para t1 t1' ->
     (forall x, x \notin L -> para (t2 ^ x) (t2' ^ x) ) ->
     para (trm_prod t1 t2) (trm_prod t1' t2').

Definition of the transitive closure of a relation

Inductive iter_ (R : relation) : relation :=
  | iter_trans : forall t2 t1 t3,
      iter_ R t1 t2 -> iter_ R t2 t3 -> iter_ R t1 t3
  | iter_step : forall t t',
      R t t' -> iter_ R t t'.

Notation "R 'iter'" := (iter_ R) (at level 69).

Lemmas Associated to Additional Definitions


Hint Constructors para iter_.

Regularity

Lemma red_regular_para : red_regular para.

Lemma red_regular_para_iter : red_regular (para iter).

Hint Extern 1 (term ?t) => match goal with
  | H: para t _ |- _ => apply (proj1 (red_regular_para H))
  | H: para _ t |- _ => apply (proj2 (red_regular_para H))
  | H: (para iter) t _ |- _ => apply (proj1 (red_regular_para_iter))
  | H: (para iter) _ t |- _ => apply (proj2 (red_regular_para_iter))
  end.

Automation

Hint Resolve para_var para_srt para_app.

Hint Extern 1 (para (trm_abs _ _) (trm_abs _ _)) =>
  let y := fresh "y" in apply_fresh para_abs as y.
Hint Extern 1 (para (trm_prod _ _) (trm_prod _ _)) =>
  let y := fresh "y" in apply_fresh para_prod as y.
Hint Extern 1 (para (trm_app (trm_abs _ _) _) (_ ^^ _)) =>
  let y := fresh "y" in apply_fresh para_red as y.

Properties of parallel reduction and its iterated version

Section ParaProperties.

Hint Extern 1 (para (if _ == _ then _ else _) _) => case_var.

Lemma para_red_all : red_all para.

Lemma para_red_refl : red_refl para.

Lemma para_red_out : red_out para.

Lemma para_red_rename : red_rename para.

Lemma para_red_through : red_through para.

Lemma para_iter_red_refl : red_refl (para iter).

End ParaProperties.

Equality of beta star and iterated parallel reductions

Lemma beta_star_to_para_iter :
  (beta star) simulated_by (para iter).

Lemma para_iter_to_beta_star :
  (para iter) simulated_by (beta star).

Proof of Church-Rosser Property for Beta Reduction


Confluence of parallel reduction

Lemma para_abs_inv : forall t1 t2 u,
  para (trm_abs t1 t2) u -> exists L, exists t1' : trm, exists t2' : trm,
  u = (trm_abs t1' t2') /\ para t1 t1' /\
  forall x : var, x \notin L -> para (t2 ^ x) (t2' ^ x).

Lemma para_prod_inv : forall t1 t2 u,
  para (trm_prod t1 t2) u -> exists L, exists t1' : trm, exists t2' : trm,
  u = (trm_prod t1' t2') /\ para t1 t1' /\
  forall x : var, x \notin L -> para (t2 ^ x) (t2' ^ x).

Lemma para_confluence : confluence para.

Confluence of iterated parallel reduction

Lemma para_iter_parallelogram :
  forall M S, (para iter) M S -> forall T, para M T ->
  exists P : trm, para S P /\ (para iter) T P.

Lemma para_iter_confluence : confluence (para iter).

Church-Rosser property of beta reduction

Lemma confluence_beta_star : confluence (beta star).

Lemma church_rosser_beta : church_rosser beta.