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 (eqterm 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