Library Lambda_ChurchRosser

Require Import Metatheory Lambda_Definitions Lambda_Infrastructure.

Main Development


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.