Conv_Dec.v



Require Peano_dec.
Require Transitive_Closure.
Require Union.
Require Termes.
Require Conv.



  Definition ord_norm1:= (union ? subterm (transp ? red1)).
  Definition ord_norm:= (clos_trans ? ord_norm1).

  Hint Unfold ord_norm1 ord_norm.


  Lemma subterm_ord_norm: (a,b:term)(subterm a b)->(ord_norm a b).
Auto 10.
Save.

  Hint subterm_ord_norm.


  Lemma red_red1_ord_norm: (a,b:term)(red a b)->(c:term)(red1 b c)
         ->(ord_norm c a).
Red.
(Induction 1; Intros; Auto).
(Apply t_trans with N; Auto).
Save.



  Lemma wf_subterm: (well_founded ? subterm).
Red.
(Induction a; Intros; Apply Acc_intro; Intros).
(Inversion_clear H; Inversion_clear H0).

(Inversion_clear H; Inversion_clear H0).

(Inversion_clear H1; Inversion_clear H2; Auto).

(Inversion_clear H1; Inversion_clear H2; Auto).

(Inversion_clear H1; Inversion_clear H2; Auto).
Save.


  Lemma wf_ord_norm1: (t:term)(sn t)->(Acc ? ord_norm1 t).
Unfold ord_norm1 .
Intros.
(Apply Acc_union; Auto).
Exact commut_red1_subterm.

Intros.
Apply wf_subterm.
Save.


  Theorem wf_ord_norm: (t:term)(sn t)->(Acc ? ord_norm t).
Unfold ord_norm .
Intros.
Apply Acc_clos_trans.
(Apply wf_ord_norm1; Auto).
Save.




  Definition norm_body := [a:term][norm:term->term]
          Cases a of
              (Srt s) => (Srt s)
           | (Ref n) => (Ref n)
           | (Abs T t) => (Abs (norm T) (norm t))
           | (App u v) =>
               <[_:term]term>Cases (norm u) of
                   (Abs _ b) => (norm (
subst (norm v) b))
                | t => (App t (norm v))
               end
           | (Prod T U) => (Prod (norm T) (norm U))
          end.

  Theorem compute_nf: (t:term)(sn t)->{u:term|(red t u)&(normal u)}.
Intros.
ElimType (Acc term ord_norm t).
Realizer norm_body.
Do 3 Program.
Program_all.
(Red; Red; Intros).
Inversion_clear H2.

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

Program_all.
(Red; Red; Intros).
Inversion_clear H2.
(Apply (y2 M'); Auto).

(Apply (y0 M'); Auto).

Program_all.
(Red; Red; Intros).
Inversion_clear H2.
Inversion_clear H3.

(Apply (y0 N2); Auto).

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

(Apply (y0 N2); Auto).

Change (ord_norm (subst x0 b) (App u v)).
(Apply red_red1_ord_norm with (App (Abs t0 b) x0); Auto).

(Apply trans_red_red with (subst x0 b); Auto).
(Apply trans_red with (App (Abs t0 b) x0); Auto).

(Red; Red; Intros).
Inversion_clear H2.
(Elim n with N1; Auto).

(Elim y0 with N2; Auto).

(Red; Red; Intros).
Inversion_clear H2.
(Elim n with N1; Auto).

(Elim y0 with N2; Auto).

Program_all.
(Red; Red; Intros).
Inversion_clear H2.
(Apply (y2 N1); Auto).

(Apply (y0 N2); Auto).

(Apply wf_ord_norm; Auto).
Save.



  Lemma eqterm: (u,v:term){u=v}+{~(u=v)}.
Realizer Fix
eqterm {eqterm/1: term->term->sumbool :=
  [u,v:term]Cases u v of
    (Srt kind) (Srt kind) => true
  | (Srt prop) (Srt prop) => true
  | (Ref n1) (Ref n2) => (eq_nat_dec n1 n2)
  | (Abs a1 b1) (Abs a2 b2) => Cases (eqvebm a1 a2) (eqterm b1 b2) of
                                 left left => true
                               | _ _ => false
                               end
  | (App a1 b1) (App a2 b2) => Cases (eqterm a1 a2) (eqterm b1 b2) of
                                 left left => true
                               | _ _ => false
                               end
  | (Prod a1 b1) (Prod a2 b2) => Cases (eqterm a1 a2) (eqterm b1 b2) of
                                 left left => true
                               | _ _ => false
                               end
  | _ _ => false
  end}.
(Program_all; Discriminate Orelse (Intros; Auto)).
(Elim e; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).

(Elim e; Elim e0; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).

(Elim e; Elim e0; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).

(Elim e; Elim e0; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).

(Red; Intro; Apply n).
(Injection H; Auto).
Save.



  Theorem is_conv: (u,v:term)(sn u)->(sn v)->{conv u v}+{~(conv u v)}.
(*
Realizer [u,v:term](eqterm (compute_nf u) (compute_nf v)).
Program_all.
*)

Intros.
(Elim compute_nf with u ;Auto;Intros).
(Elim compute_nf with v ;Auto;Intros).
(Elim eqterm with x x0 ;Intros).
Left.
(Apply trans_conv_conv with x ;Auto).
Apply sym_conv.
(Rewrite -> y3;Auto).

Right.
(Red;Intro;Apply y3).
Elim church_rosser with x x0 ;Auto;Intros.
Rewrite -> (red_normal x x1);Auto.
Rewrite -> (red_normal x0 x1);Auto.

(Apply trans_conv_conv with v ;Auto).
(Apply trans_conv_conv with u ;Auto).
(Apply sym_conv;Auto).
Save.

07/03/97, 15:05