Library Conv

Require Export Term.

Section Church_Rosser.

  Definition str_confluent R := commut _ R (transp term R).

  Lemma str_confluence_par_red1 : str_confluent par_red1.
red in |- *; red in |- *.
simple induction 1; intros.
inversion_clear H4.
elim H1 with M'0; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (subst x1 x0); unfold subst in |- *; auto with coc.

inversion_clear H5.
elim H1 with M'1; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (subst x1 x0); auto with coc; unfold subst in |- *; auto with coc.

inversion_clear H0.
exists (Srt s); auto with coc.

inversion_clear H0.
exists (Ref n); auto with coc.

inversion_clear H4.
elim H1 with M'0; auto with coc; intros.
elim H3 with T'0; auto with coc; intros.
exists (Abs x1 x0); auto with coc.

generalize H0 H1.
clear H0 H1.
inversion_clear H4.
intro.
inversion_clear H4.
intros.
elim H4 with (Abs T M'0); auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
apply inv_par_red_abs with T' M'1 x0; intros; auto with coc.
generalize H7 H8.
rewrite H11.
clear H7 H8; intros.
inversion_clear H7.
inversion_clear H8.
exists (subst x1 U'); auto with coc.
unfold subst in |- *; auto with coc.

intros.
elim H5 with M'0; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (App x0 x1); auto with coc.

intros.
inversion_clear H4.
elim H1 with M'0; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (Prod x0 x1); auto with coc.
Qed.

  Lemma strip_lemma : commut _ par_red (transp _ par_red1).
unfold commut, par_red in |- *; simple induction 1; intros.
elim str_confluence_par_red1 with z x0 y0; auto with coc; intros.
exists x1; auto with coc.

elim H1 with z0; auto with coc; intros.
elim H3 with x1; intros; auto with coc.
exists x2; auto with coc.
apply t_trans with x1; auto with coc.
Qed.

  Lemma confluence_par_red : str_confluent par_red.
red in |- *; red in |- *.
simple induction 1; intros.
elim strip_lemma with z x0 y0; intros; auto with coc.
exists x1; auto with coc.

elim H1 with z0; intros; auto with coc.
elim H3 with x1; intros; auto with coc.
exists x2; auto with coc.
red in |- *.
apply t_trans with x1; auto with coc.
Qed.

  Lemma confluence_red : str_confluent red.
red in |- *; red in |- *.
intros.
elim confluence_par_red with x y z; auto with coc; intros.
exists x0; auto with coc.
Qed.

  Theorem church_rosser :
   ∀ u v, conv u v -> exists2 t, red u t & red v t.
simple induction 1; intros.
exists u; auto with coc.

elim H1; intros.
elim confluence_red with x P N; auto with coc; intros.
exists x0; auto with coc.
apply trans_red_red with x; auto with coc.

elim H1; intros.
exists x; auto with coc.
apply trans_red_red with P; auto with coc.
Qed.

  Lemma inv_conv_prod_l :
   ∀ a b c d, conv (Prod a c) (Prod b d) -> conv a b.
intros.
elim church_rosser with (Prod a c) (Prod b d); intros; auto with coc.
apply red_prod_prod with a c x; intros; auto with coc.
apply red_prod_prod with b d x; intros; auto with coc.
apply trans_conv_conv with a0; auto with coc.
apply sym_conv.
generalize H2.
rewrite H5; intro.
injection H8.
simple induction 2; auto with coc.
Qed.

  Lemma inv_conv_prod_r :
   ∀ a b c d, conv (Prod a c) (Prod b d) -> conv c d.
intros.
elim church_rosser with (Prod a c) (Prod b d); intros; auto with coc.
apply red_prod_prod with a c x; intros; auto with coc.
apply red_prod_prod with b d x; intros; auto with coc.
apply trans_conv_conv with b0; auto with coc.
apply sym_conv.
generalize H2.
rewrite H5; intro.
injection H8.
simple induction 1; auto with coc.
Qed.

  Lemma nf_uniqueness : ∀ u v, conv u v -> normal u -> normal v -> u = v.
intros.
elim church_rosser with u v; intros; auto with coc.
rewrite (red_normal u x); auto with coc.
elim red_normal with v x; auto with coc.
Qed.

  Lemma conv_sort : ∀ s1 s2, conv (Srt s1) (Srt s2) -> s1 = s2.
intros.
cut (Srt s1 = Srt s2); intros.
injection H0; auto with coc.

apply nf_uniqueness; auto with coc.
red in |- *; red in |- *; intros.
inversion_clear H0.

red in |- *; red in |- *; intros.
inversion_clear H0.
Qed.

  Lemma conv_kind_prop : ~ conv (Srt kind) (Srt prop).
red in |- *; intro.
absurd (kind = prop).
discriminate.

apply conv_sort; auto with coc.
Qed.

  Lemma conv_sort_prod : ∀ s t u, ~ conv (Srt s) (Prod t u).
red in |- *; intros.
elim church_rosser with (Srt s) (Prod t u); auto with coc.
do 2 intro.
elim red_normal with (Srt s) x; auto with coc.
intro.
apply red_prod_prod with t u (Srt s); auto with coc; intros.
discriminate H2.

red in |- *; red in |- *; intros.
inversion_clear H1.
Qed.

End Church_Rosser.