Library Lambda_ChurchRosser
Require Import Metatheory Lambda_Definitions Lambda_Infrastructure.
Putting constructors as hints for auto
Hint Constructors beta star_ equiv_ iter_.
Hint Resolve para_var 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_app (trm_abs _) _) (_ ^^ _)) =>
let y := fresh "y" in apply_fresh para_red as y.
Some relations between the properties of relations
Lemma red_all_to_out : forall (R : relation),
red_all R -> red_refl R -> red_out R.
Lemma red_out_to_rename : forall (R : relation),
red_out R -> red_rename R.
Lemma red_all_to_through : forall (R : relation),
red_regular R -> red_all R -> red_through R.
Properties of beta relation
Lemma beta_red_out : red_out beta.
Lemma beta_red_rename : red_rename beta.
Properties of beta star relation
Lemma beta_star_app1 : forall t1 t1' t2,
(beta star) t1 t1' -> term t2 ->
(beta star) (trm_app t1 t2) (trm_app t1' t2).
Lemma beta_star_app2 : forall t1 t2 t2',
(beta star) t2 t2' -> term t1 ->
(beta star) (trm_app t1 t2) (trm_app t1 t2').
Lemma beta_star_abs : forall L t1 t1',
(forall x, x \notin L -> (beta star) (t1 ^ x) (t1' ^ x)) ->
(beta star) (trm_abs t1) (trm_abs t1').
Lemma beta_star_red_in : red_in (beta star).
Lemma beta_star_red_all : red_all (beta star).
Lemma beta_star_red_through : red_through (beta star).
Properties of parallel relation 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.
Confluence of parallel relation
Lemma para_abs_inv : forall t1 u,
para (trm_abs t1) u -> exists L, exists t2, u = (trm_abs t2) /\
forall x : var, x \notin L -> para (t1 ^ x) (t2 ^ x).
Lemma para_confluence : confluence para.
Confluence of iterated parallel relation
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).
Equality of beta star and iterated parallel relations
Lemma beta_star_to_para_iter :
(beta star) simulated_by (para iter).
Lemma para_iter_to_beta_star :
(para iter) simulated_by (beta star).
Church-Rosser property of beta relation
Lemma beta_star_confluence : confluence (beta star).
Lemma beta_church_rosser : church_rosser beta.