Set Implicit Arguments.
Require Import Metatheory CoC_Definitions CoC_Infrastructure CoC_BetaStar.
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').
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_.
Lemma red_regular_para : red_regular para.
Proof.
introz. induction* H.
Qed.
Lemma red_regular_para_iter : red_regular (para iter).
Proof.
introz. induction* H. apply* red_regular_para.
Qed.
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.
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.
Section ParaProperties.
Hint Extern 1 (para (if _ == _ then _ else _) _) => case_var.
Lemma para_red_all : red_all para.
Proof.
intros x t t' H. induction H; intros; simpl*.
rewrite* subst_open. apply_fresh* para_red as y. cross*.
apply_fresh* para_abs as y. cross*.
apply_fresh* para_prod as y. cross*.
Qed.
Lemma para_red_refl : red_refl para.
Proof.
introz. induction* H.
Qed.
Lemma para_red_out : red_out para.
Proof.
apply* (red_all_to_out para_red_all para_red_refl).
Qed.
Lemma para_red_rename : red_rename para.
Proof.
apply* (red_out_to_rename para_red_out).
Qed.
Lemma para_red_through : red_through para.
Proof.
apply* (red_all_to_through red_regular_para para_red_all).
Qed.
Lemma para_iter_red_refl : red_refl (para iter).
Proof.
introz. use para_red_refl.
Qed.
End ParaProperties.
Lemma beta_star_to_para_iter :
(beta star) simulated_by (para iter).
Proof.
introz. induction* H.
apply* para_iter_red_refl.
apply iter_step. induction H; use para_red_refl.
Qed.
Lemma para_iter_to_beta_star :
(para iter) simulated_by (beta star).
Proof.
introz. induction H; eauto.
induction H.
apply~ (@star_trans beta (t2 ^^ u)).
pick_fresh x. apply* (@beta_star_red_through x).
apply* star_refl.
apply* star_refl.
apply~ (@star_trans beta (trm_app t1' t2)).
apply* beta_star_app1. apply* beta_star_app2.
apply~ (@star_trans beta (trm_abs t1' t2)).
apply* beta_star_abs1. apply* beta_star_abs2.
apply~ (@star_trans beta (trm_prod t1' t2)).
apply* beta_star_prod1. apply* beta_star_prod2.
Qed.
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).
intros. inversion H. exists* L.
Qed.
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).
Proof.
intros. inversion H. exists* L.
Qed.
Lemma para_confluence : confluence para.
Proof.
introv HS. gen T. induction HS; intros T HT; inversions HT.
destructi~ (IHHS u'0) as [u2 [U2a U2b]].
pick_fresh x. forward~ (H1 x) as K.
destruct~ (K (t2'0 ^ x)) as [u1x [U1a U1b]].
destruct~ (@close_var_spec u1x x) as [u1 [EQu1 termu1]].
rewrite EQu1 in U1a, U1b.
exists (u1 ^^ u2). split; apply* (@para_red_through x).
destructi~ (IHHS t2'0) as [u2 [U2a U2b]].
destruct (para_abs_inv H4) as [L2 [t1'0x [t2'0x [EQ [Ht1'0 Ht2'0]]]]].
rewrite EQ in H4 |- *.
pick_fresh x. forward~ (H1 x) as K.
destruct~ (K (t2'0x ^ x)) as [u1x [U1a U1b]].
destruct~ (@close_var_spec u1x x) as [u1 [EQu1 termu1]].
rewrite EQu1 in U1a, U1b.
exists (u1 ^^ u2). split.
apply* (@para_red_through x).
apply_fresh para_red as y; auto.
apply* (@para_red_rename x).
auto*.
auto*.
destruct~ (IHHS2 u') as [u2 [U2a U2b]].
destruct (para_abs_inv HS1) as [L2 [t1'x [t2'x [EQ [Ht1'x Ht2'x]]]]].
destruct (IHHS1 (trm_abs t1'x t2'0)) as [u1x [U1a U1b]]. auto.
rewrite EQ in HS1, U1a |- *.
destruct (para_abs_inv U1b) as [L1 [v1 [v2 [EQ' [Hv1 Hv2]]]]].
rewrite EQ' in U1a, U1b.
exists (v2 ^^ u2). split.
inversion U1a. clear IHHS1 IHHS2 Hv2 U1a U1b.
apply* (@para_red L0).
pick_fresh x. apply* (@para_red_through x).
destructi~ (IHHS1 t1'0) as [P1 [HP11 HP12]].
destructi~ (IHHS2 t2'0) as [P2 [HP21 HP22]].
exists* (trm_app P1 P2).
pick_fresh x. forward~ (H0 x) as K.
destruct~ (K (t2'0 ^ x)) as [px [P0 P1]].
destructi~ (IHHS t1'0) as [u1 [HP1 HP2]].
destruct~ (@close_var_spec px x) as [p [EQP termp]].
rewrite EQP in P0, P1.
exists (trm_abs u1 p). split;
apply_fresh* para_abs as y; apply* (@para_red_rename x).
pick_fresh x. forward~ (H0 x) as K.
destruct~ (K (t2'0 ^ x)) as [px [P0 P1]].
destructi~ (IHHS t1'0) as [u1 [HP1 HP2]].
destruct~ (@close_var_spec px x) as [p [EQP termp]].
rewrite EQP in P0, P1.
exists (trm_prod u1 p). split;
apply_fresh* para_prod as y; apply* (@para_red_rename x).
Qed.
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.
Proof.
introv H. induction H; intros T MtoT.
destructi~ (IHiter_1 T) as [P [HP1 HP2]].
destructi~ (IHiter_2 P) as [Q [HQ1 HQ2]].
exists Q. use (@iter_trans para P).
destruct* (para_confluence H MtoT).
Qed.
Lemma para_iter_confluence : confluence (para iter).
Proof.
introv MtoS MtoT. gen T.
induction MtoS; intros T MtoT.
destructi~ (IHMtoS1 T) as [P [HP1 HP2]].
destructi~ (IHMtoS2 P) as [Q [HQ1 HQ2]]. exists* Q.
destruct* (para_iter_parallelogram MtoT H).
Qed.
Lemma confluence_beta_star : confluence (beta star).
Proof.
introz. destruct (@para_iter_confluence M S T).
use beta_star_to_para_iter.
use beta_star_to_para_iter.
use para_iter_to_beta_star.
Qed.
Lemma church_rosser_beta : church_rosser beta.
Proof.
introz. induction H.
exists* t.
destruct* IHequiv_.
destruct IHequiv_1 as [u [Pu Qu]].
destruct IHequiv_2 as [v [Pv Qv]].
destruct (confluence_beta_star Qu Pv) as [w [Pw Qw]].
exists w. split.
apply* (@star_trans beta u).
apply* (@star_trans beta v).
exists* t'.
Qed.