Infer.v
Require Termes.
Require Conv.
Require Types.
Require Strong_Norm.
Require Conv_Dec.
Lemma
red_to_prod: (t:term)(sn t)->
{p:term*term|(u,v:term)(p=(u,v))->(red t (Prod u v))}
+{(u,v:term)~(conv t (Prod u v))}.
Realizer [t:term]<sumor (term*term)>Case (compute_nf t) of
[_:sort](inright (term*term))
[_:nat](inright (term*term))
[_,_:term](inright (term*term))
[_,_:term](inright (term*term))
[u,v:term](inleft (term*term) (u,v))
end.
Program_all.
(Red;Intros).
Apply (conv_sort_prod _ u v).
(Apply trans_conv_conv with t ;Auto).
(Apply sym_conv;Auto).
(Red;Intros).
Elim church_rosser with (Prod u v) (Ref _) ;Intros.
Generalize H1 .
Elim red_normal with (Ref _) x0 ;Auto;Intros.
Apply red_prod_prod with u v (Ref _) ;Auto;Intros.
Discriminate H4.
Apply trans_conv_conv with t ;Auto.
Red;Intros.
Elim church_rosser with (Prod u v) (Abs _ _0) ;Intros.
Generalize H1 .
Elim red_normal with (Abs _ _0) x0 ;Auto;Intros.
Apply red_prod_prod with u v (Abs _ _0) ;Auto;Intros.
Discriminate H4.
Apply trans_conv_conv with t ;Auto.
Red;Intros.
Elim church_rosser with (Prod u v) (App _ _0) ;Intros.
Generalize H1 .
Elim red_normal with (App _ _0) x0 ;Auto;Intros.
Apply red_prod_prod with u v (App _ _0) ;Auto;Intros.
Discriminate H4.
Apply trans_conv_conv with t ;Auto.
(Left;Exists (u,v) ;Intros).
Injection H0.
(Induction 1;Induction 1;Auto).
Save.
Lemma
red_to_sort: (T:term)(sn T)
->{(e:env)(t:term)(typ e t T)->(Ex [s:sort](typ e t (Srt s)))}
+{(e:env)(t:term)(typ e t T)->(s:sort)~(typ e t (Srt s))}.
Realizer [t:term]
<bool>if (eqterm (Srt kind) t) then true
else <bool>if (is_conv (Srt prop) t) then true
else false.
Program_all.
(Exists kind ;Rewrite -> e;Auto).
(Red;Apply Acc_intro;Intros).
Inversion_clear H0.
Exists prop .
(Apply type_conv with t kind ;Auto).
Apply type_prop.
(Apply typ_wf with t0 t ;Auto).
(Induction s;Intros).
(Red;Intro;Apply n).
Symmetry.
(Apply type_kind_not_conv with e t0 ;Auto).
(Red;Intro;Apply n0).
(Apply typ_unique with e t0 ;Auto).
Save.
Section Decidabilite_typage.
Theorem
infer: (e:env)(t:term)
(wf e)->{T:term|(typ e t T)}+{(T:term)~(typ e t T)}.
Realizer [e:env][t:term](<env->(sumor term)>Match t with
[s,f]<sumor term>Case s of
(inright term)
(inleft term (Srt kind))
end
[n,e]<sumor term>Case (list_item term e n) of
[T](inleft term (lift (S n) T))
(inright term)
end
[t,tt,b,tb,e]<sumor term>Case (tt e) of
[T]<sumor term>if (red_to_sort T) then
<sumor term>Case (tb (cons term t e)) of
[B]<sumor term>if (eqterm (Srt kind) B)
then (inright term)
else (inleft term (Prod t B))
(inright term)
end
else (inright term)
(inright term)
end
[t,tt,b,tb,e]<sumor term>Case (tt e) of
[T]<sumor term>Case (red_to_prod T) of
[p]<sumor term>let (V,Ur:term)=p in
<sumor term>Case (tb e) of
[B]<sumor term>if (is_conv V B)
then (inleft term (subst b Ur))
else (inright term)
(inright term)
end
(inright term)
end
(inright term)
end
[t,tt,b,tb,e]<(sumor term)>Case (tt e) of
[T]<(sumor term)>Case (red_to_sort T) of
<(sumor term)>Case (tb (cons term t e)) of
[B]<(sumor term)>Case (eqterm (Srt kind) B) of
(inleft term (Srt kind))
<(sumor term)>Case (is_conv (Srt prop) B) of
(inleft term (Srt prop))
(inright term)
end
end
(inright term)
end
(inright term)
end
(inright term)
end
end e).
Do 6 Program.
Do 3 Program.
Program_all.
Red;Intros.
Elim inv_typ_kind with f T ;Auto.
Left.
Exists (Srt kind) .
(Apply type_prop;Auto).
Program_all.
(Apply type_var;Auto).
(Exists T0 ;Auto).
Red;Intros.
(Apply inv_typ_ref with e0 T n ;Auto;Intros).
(Elim n0 with U ;Auto).
Do 4 Program.
Auto.
Do 3 Program.
Apply type_sn with e0 t1 ;Auto.
Program.
(Elim e1 with e0 t1 ;Auto;Intros).
(Apply wf_var with x ;Auto).
Do 3 Program.
Program_all.
(Red;Intros).
(Apply inv_typ_abs with e0 t1 t2 T1 ;Auto;Intros).
(Elim inv_typ_conv_kind with (cons ? t1 e0) T2 (Srt s2) ;Auto).
Rewrite -> e2.
(Apply typ_unique with (cons ? t1 e0) t2 ;Auto).
Program_all.
(Elim type_case with (cons ? t1 e0) t2 B0 ;Intros;Auto).
Inversion_clear H0.
(Elim e1 with e0 t1 ;Intros;Auto).
(Apply type_abs with x0 x ;Auto).
(Elim n;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_abs with e0 t1 t2 T1 ;Auto;Intros).
(Elim n with T2 ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_abs with e0 t1 t2 T1 ;Auto;Intros).
(Elim n with e0 t1 s1 ;Auto).
(Right;Red;Intros).
(Apply inv_typ_abs with e0 t1 t2 T ;Auto;Intros).
(Elim n with (Srt s1) ;Auto).
Do 4 Program.
Auto.
Do 3 Program.
Apply type_sn with e0 t1 ;Auto.
Do 6 Program.
Auto.
Do 3 Program.
Apply subterm_sn with (Prod V Ur);Auto.
Apply sn_red_sn with T0 ;Auto.
Apply type_sn with e0 t1 ;Auto.
Apply type_sn with e0 t2 ;Auto.
Program_all.
(Elim type_case with e0 t1 T0 ;Intros;Auto).
Elim H0.
Intros.
(Cut (typ e0 (Prod V Ur) (Srt x));Intros).
Change (typ e0 (App t1 t2) (subst t2 Ur)).
(Apply type_app with V ;Auto).
(Apply inv_typ_prod with e0 V Ur (Srt x) ;Auto;Intros).
(Apply type_conv with B0 s1 ;Auto).
(Apply type_conv with T0 x ;Auto).
Apply subject_reduction with T0 ;Auto.
Elim conv_sort_prod with kind V Ur .
(Elim H0;Auto).
Program_all.
(Red;Intros).
Apply n.
(Apply inv_typ_app with e0 t1 t2 T1 ;Auto;Intros).
Apply trans_conv_conv with V0 .
Apply inv_conv_prod_l with Ur Ur0 .
(Apply typ_unique with e0 t1 ;Auto).
(Elim type_case with e0 t1 T0 ;Intros;Auto).
(Elim H4;Intros).
Apply type_conv with T0 x ;Auto.
(Apply subject_reduction with T0 ;Auto).
Elim conv_sort_prod with kind V Ur .
(Elim H4;Auto).
(Apply typ_unique with e0 t2 ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_app with e0 t1 t2 T1 ;Auto;Intros).
(Elim n with V0 ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_app with e0 t1 t2 T1 ;Auto;Intros).
Elim n with V Ur .
(Apply typ_unique with e0 t1 ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_app with e0 t1 t2 T ;Auto;Intros).
(Elim n with (Prod V Ur) ;Auto).
Do 4 Program.
Auto.
Do 3 Program.
Apply type_sn with e0 t1 ;Auto.
Program.
Elim e1 with e0 t1 ;Auto;Intros.
Apply wf_var with x ;Auto.
Do 3 Program.
Left.
Program_all.
Elim e1 with e0 t1 ;Auto;Intros.
Apply type_prod with x ;Auto.
Rewrite -> e2;Auto.
Program.
(Red;Apply Acc_intro;Intros).
Inversion_clear H0.
Apply type_sn with (cons ? t1 e0) t2 ;Auto.
Left.
Program_all.
Elim e1 with e0 t1 ;Auto;Intros.
Apply type_prod with x ;Auto.
Apply type_conv with B0 kind ;Auto.
Apply type_prop.
(Apply wf_var with x ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_prod with e0 t1 t2 T1 ;Auto).
(Destruct s2;Intros).
Apply n.
(Elim type_kind_not_conv with (cons term t1 e0) t2 B0 ;Auto).
Apply n0.
(Apply typ_unique with (cons ? t1 e0) t2 ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_prod with e0 t1 t2 T1 ;Auto;Intros).
(Elim n with (Srt s2) ;Auto).
Program_all.
(Red;Intros).
(Apply inv_typ_prod with e0 t1 t2 T1 ;Auto).
Intros.
Elim n with e0 t1 s1 ;Auto.
Program_all.
(Red;Intros).
(Apply inv_typ_prod with e0 t1 t2 T ;Auto;Intros).
(Elim n with (Srt s1) ;Auto).
Save.
Lemma
check_typ: (e:env)(t,tp:term)(wf e)->{(typ e t tp)}+{~(typ e t tp)}.
Realizer [e:env][t,tp:term]<bool>Case (infer e t) of
[tp':term]<bool>if (eqterm (Srt kind) tp')
then <bool>if (eqterm (Srt kind) tp) then true
else false
else <bool>Case (infer e tp) of
[s:term]<bool>if (is_conv tp tp') then true
else false
false
end
false
end.
Program_all.
Elim e1;Rewrite -> e0;Auto.
Red;Intro;Apply n.
Symmetry;Apply type_kind_not_conv with e t ;Auto.
Rewrite -> e0;Auto.
Apply fort_norm with e s0 ;Auto.
Apply type_sn with e t ;Auto.
Elim type_case with e t tp'0 ;Auto;Intros.
Elim H0.
(Induction x;Intros).
(Apply type_conv with tp'0 kind ;Auto).
(Replace (Srt kind) with s0;Auto).
(Elim type_case with e tp s0 ;Auto;Intros).
Inversion_clear H2.
(Elim inv_typ_conv_kind with e s0 (Srt x0) ;Auto).
(Apply typ_conv_conv with e tp tp'0 ;Auto).
(Apply type_conv with tp'0 prop ;Auto).
(Apply type_conv with s0 kind ;Auto).
(Apply typ_conv_conv with e tp tp'0 ;Auto).
Apply type_prop.
(Apply typ_wf with tp s0 ;Auto).
Elim n;Auto.
Red;Intro.
Apply n0.
Apply typ_unique with e t ;Auto.
Red;Intro.
Elim type_case with e t tp ;Auto;Intros.
Elim H1;Intros.
Elim n0 with (Srt x) ;Auto.
Apply n.
Symmetry.
Apply type_kind_not_conv with e t ;Auto.
Elim H1;Auto.
Save.
Lemma
add_typ: (e:env)(t:term)(wf e)
->{(wf (cons ? t e))}+{~(wf (cons ? t e))}.
Realizer [e:env][t:term]<bool>Case (infer e t) of
[tp:term]<bool>if (red_to_sort tp) then true
else false
false
end.
Program_all.
Apply type_sn with e t ;Auto.
(Elim e0 with e t ;Auto;Intros).
(Apply wf_var with x ;Auto).
(Red;Intros).
Inversion_clear H0.
(Elim n with e t s ;Auto).
(Red;Intros).
Inversion_clear H0.
Elim n with (Srt s) ;Auto.
Save.
Lemma
decide_wf: (e:env){(wf e)}+{~(wf e)}.
(Induction e;Intros).
(Left;Apply wf_nil).
(Elim H;Intros).
(Elim add_typ with l a ;Auto;Intros).
(Right;Red;Intros;Apply y).
Inversion_clear H0.
(Apply typ_wf with a (Srt s) ;Auto).
Save.
Lemma
decide_typ: (e:env)(t,tp:term){(typ e t tp)}+{~(typ e t tp)}.
Intros.
(Elim decide_wf with e ;Intros).
(Apply check_typ;Auto).
(Right;Red;Intros;Apply y).
(Apply typ_wf with t tp ;Auto).
Save.
End Decidabilite_typage.
17/10/96, 13:59