Library CoC_ChurchRosser
Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_BetaStar.
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).
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).
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.