Conv.v

Require Termes.

Section Church_Rosser.

  Definition str_confluent := [R:term->term->Prop](commut ? R (transp ? R)).

  Lemma str_confluence_par_red1: (str_confluent par_red1).
Red;Red.
(Induction 1;Intros).
Inversion_clear H4.
(Elim H1 with M'0 ;Auto;Intros).
(Elim H3 with N'0 ;Auto;Intros).
(Exists (subst x1 x0);Unfold subst ;Auto).

Inversion_clear H5.
(Elim H1 with M'1 ;Auto;Intros).
(Elim H3 with N'0 ;Auto;Intros).
(Exists (subst x1 x0);Auto;Unfold subst ;Auto).

Inversion_clear H0.
(Exists (Srt s);Auto).

Inversion_clear H0.
Exists (Ref n);Auto.

Inversion_clear H4.
(Elim H1 with M'0 ;Auto;Intros).
(Elim H3 with T'0 ;Auto;Intros).
(Exists (Abs x1 x0);Auto).

Generalize H0 H1 .
Clear H0 H1.
Inversion_clear H4.
Intro.
Inversion_clear H4.
Intros.
(Elim H4 with (Abs T M'0) ;Auto;Intros).
(Elim H3 with N'0 ;Auto;Intros).
Apply inv_par_red_abs with T' M'1 x0 ;Intros;Auto.
Generalize H7 H8 .
Rewrite -> H11.
(Clear H7 H8;Intros).
Inversion_clear H7.
Inversion_clear H8.
(Exists (subst x1 U');Auto).
(Unfold subst ;Auto).

Intros.
(Elim H5 with M'0 ;Auto;Intros).
(Elim H3 with N'0 ;Auto;Intros).
(Exists (App x0 x1);Auto).

Intros.
Inversion_clear H4.
(Elim H1 with M'0 ;Auto;Intros).
(Elim H3 with N'0 ;Auto;Intros).
(Exists (Prod x0 x1);Auto).
Save.

  Lemma strip_lemma: (commut ? par_red (transp ? par_red1)).
(Unfold commut par_red; Induction 1; Intros).
(Elim str_confluence_par_red1 with z x0 y0; Auto; Intros).
(Exists x1; Auto).

(Elim H1 with z0; Auto; Intros).
(Elim H3 with x1; Intros; Auto).
(Exists x2; Auto).
(Apply t_trans with x1; Auto).
Save.

  Lemma confluence_par_red: (str_confluent par_red).
(Red; Red).
(Induction 1; Intros).
(Elim strip_lemma with z x0 y0; Intros; Auto).
(Exists x1; Auto).

(Elim H1 with z0; Intros; Auto).
(Elim H3 with x1; Intros; Auto).
(Exists x2; Auto).
Red.
(Apply t_trans with x1; Auto).
Save.

  Lemma confluence_red: (str_confluent red).
Red;Red.
Intros.
Elim confluence_par_red with x y z ;Auto;Intros.
(Exists x0;Auto).
Save.

  Theorem church_rosser: (u,v:term)(conv u v)
                ->(Ex2 [t:term](red u t) [t:term](red v t)).
(Induction 1; Intros).
(Exists u; Auto).

(Elim H1; Intros).
(Elim confluence_red with x P N; Auto; Intros).
(Exists x0; Auto).
(Apply trans_red_red with x; Auto).

(Elim H1; Intros).
(Exists x; Auto).
(Apply trans_red_red with P; Auto).
Save.

  Lemma inv_conv_prod_l: (a,b,c,d:term)(conv (Prod a c)(Prod b d))->(conv a b).
Intros.
Elim church_rosser with (Prod a c) (Prod b d) ;Intros;Auto.
Apply red_prod_prod with a c x ;Intros;Auto.
Apply red_prod_prod with b d x ;Intros;Auto.
(Apply trans_conv_conv with a0 ;Auto).
Apply sym_conv.
Generalize H2 .
(Rewrite -> H5;Intro).
Injection H8.
(Induction 2;Auto).
Save.

  Lemma inv_conv_prod_r: (a,b,c,d:term)(conv (Prod a c)(Prod b d))->(conv c d).
Intros.
(Elim church_rosser with (Prod a c) (Prod b d) ;Intros;Auto).
(Apply red_prod_prod with a c x ;Intros;Auto).
(Apply red_prod_prod with b d x ;Intros;Auto).
Apply trans_conv_conv with b0 ;Auto.
Apply sym_conv.
Generalize H2 .
Rewrite -> H5;Intro.
Injection H8.
(Induction 1;Auto).
Save.

  Lemma nf_uniqueness: (u,v:term)(conv u v)->(normal u)->(normal v)->u=v.
Intros.
(Elim church_rosser with u v; Intros; Auto).
(Rewrite -> (red_normal u x); Auto).
(Elim red_normal with v x; Auto).
Save.

  Lemma conv_sort: (s1,s2:sort)(conv (Srt s1) (Srt s2))->s1=s2.
Intros.
(Cut (Srt s1)=(Srt s2); Intros).
(Injection H0; Auto).

(Apply nf_uniqueness; Auto).
(Red; Red; Intros).
Inversion_clear H0.

(Red; Red; Intros).
Inversion_clear H0.
Save.

  Lemma conv_kind_prop: ~(conv (Srt kind) (Srt prop)).
(Red;Intro).
Absurd kind=prop.
Discriminate.

(Apply conv_sort;Auto).
Save.

  Lemma conv_sort_prod: (s:sort)(t,u:term)~(conv (Srt s) (Prod t u)).
Red;Intros.
Elim church_rosser with (Srt s) (Prod t u) ;Auto.
Do 2 Intro.
Elim red_normal with (Srt s) x ;Auto.
Intro.
(Apply red_prod_prod with t u (Srt s) ;Auto;Intros).
Discriminate H2.

(Red;Red;Intros).
Inversion_clear H1.
Save.

End Church_Rosser.

13/02/97, 13:18