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 H.
(Inversion_clear H1; Auto).
(Inversion_clear H1; Auto).
(Inversion_clear H1; 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.
Theorem
compute_nf: (t:term)(sn t)->{u:term|(red t u)&(normal u)}.
Intros.
ElimType (Acc term ord_norm t).
Intros a H0.
Realizer [norm:term->term]
<term>Case a of
[s:sort](Srt s)
[n:nat](Ref n)
[T,t:term](Abs (norm T) (norm t))
[u,v:term]
<term>Case (norm u) of
[s:sort](App (Srt s) (norm v))
[n:nat](App (Ref n) (norm v))
[a,b:term](norm (subst (norm v) b))
[a,b:term](App (App a b) (norm v))
[a,b:term](App (Prod a b) (norm v))
end
[T,U:term](Prod (norm T) (norm U))
end.
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 a0 b) x0); Auto).
(Apply trans_red_red with (subst x0 b); Auto).
(Apply trans_red with (App (Abs a0 b) x0); Auto).
(Red; Red; Intros).
Inversion_clear H2.
(Apply (n N1); Auto).
(Apply (y0 N2); Auto).
(Red; Red; Intros).
Inversion_clear H2.
(Apply (n N1); Auto).
(Apply (y0 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
eqsort: (s,t:sort){s=t}+{~s=t}.
(Induction s;Induction t;(Right;Discriminate) Orelse Auto).
Save.
Lemma
eqterm: (u,v:term){u=v}+{~(u=v)}.
(Induction u;Destruct v;(Right;Discriminate) Orelse (Intros;Auto)).
Elim (eqsort s s0);Intros.
Left.
(Elim y;Auto).
Right.
Red;Intro;Apply y.
Injection H;Auto.
(Elim (eq_nat_dec n n0);Intros).
Left.
(Elim y;Auto).
Right.
(Red;Intro;Apply y).
(Injection H;Auto).
(Elim H with t1 ;Intros).
(Elim H0 with t2 ;Intros).
(Left;Elim y;Elim y0;Auto).
(Right;Unfold not ;Intro;Apply y0).
(Inversion_clear H1;Auto).
(Right;Unfold not ;Intro;Apply y).
(Inversion_clear H1;Auto).
(Elim H with t1 ;Intros).
(Elim H0 with t2 ;Intros).
(Left;Elim y;Elim y0;Auto).
(Right;Unfold not ;Intro;Apply y0).
(Inversion_clear H1;Auto).
(Right;Unfold not ;Intro;Apply y).
(Inversion_clear H1;Auto).
(Elim H with t1 ;Intros).
(Elim H0 with t2 ;Intros).
(Left;Elim y;Elim y0;Auto).
(Right;Unfold not ;Intro;Apply y0).
(Inversion_clear H1;Auto).
(Right;Unfold not ;Intro;Apply y).
(Inversion_clear H1;Auto).
Save.
Theorem
is_conv: (u,v:term)(sn u)->(sn v)->{conv u v}+{~(conv u v)}.
(*Realizer [u,v:term]
<bool>if (eqterm (compute_nf u) (compute_nf v)) then true
else false.
*)
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.
17/10/96, 19:28