Conv.v

Require Termes.

Section Church_Rosser.

  Definition confluent :=
       [R:term->term->Prop](x,y:term)(R x y)->(y':term)(R x y')
         ->(Ex2 [z:term](R y z) [z:term](R y' z)).

  Lemma confluence_par_red1: (confluent par_red1).
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: (x,y:term)(par_red x y)->(y':term)(par_red1 x y')
     ->(Ex2 [z:term](par_red1 y z) [z:term](par_red y' z)).
(Unfold par_red ;Induction 1;Intros).
Elim confluence_par_red1 with x0 y0 y' ;Auto;Intros.
Elim confluence_par_red1 with x0 y0 y' ;Auto;Intros.
(Exists x1 ;Auto).

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

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

Elim H1 with y' ;Intros;Auto.
Elim H3 with x1 ;Intros;Auto.
Exists x2 ;Auto.
Red.
Apply t_trans with x1 ;Auto.
Save.

  Lemma confluence_red: (confluent red).
Red.
Intros.
Elim confluence_par_red with x y y' ;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 P x 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_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 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 conv_sort: (s1,s2:sort)(conv (Srt s1) (Srt s2))->s1=s2.
Intros.
(Elim church_rosser with (Srt s1) (Srt s2) ;Intros;Auto).
Cut (eq ? (Srt s1) (Srt s2)).
Intro.
(Injection H2;Auto).

(Rewrite -> (red_normal (Srt s1) x);Auto).
(Rewrite -> (red_normal (Srt s2) x);Auto).
(Red;Red;Intros).
Inversion_clear H2.

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

  Lemma conv_kind_prop: ~(conv (Srt kind) (Srt prop)).
(Red;Intro).
Absurd (eq ? 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.

17/10/96, 14:12