Infer.v
Require Termes.
Require Conv.
Require Types.
Require Strong_Norm.
Require Conv_Dec.
Lemma
red_to_sort: (t:term)(sn t)->
{ s:sort | (red t (Srt s))}+{(s:sort)~(conv t (Srt s))}.
Realizer [t:term]Cases (compute_nf t) of
(Srt s) => (inleft sort s)
| _ => (inright sort)
end.
Program_all.
(Red; Intros).
(Elim church_rosser with (Srt s) (Ref t0); Intros).
Generalize H1 .
(Elim red_normal with (Ref t0) x0; Auto; Intros).
(Apply red_sort_sort with s (Ref t0); Auto).
Discriminate.
(Apply trans_conv_conv with t; Auto).
(Red; Intros).
(Elim church_rosser with (Srt s) (Abs t0 t1); Intros).
Generalize H1 .
(Elim red_normal with (Abs t0 t1) x0; Auto; Intros).
(Apply red_sort_sort with s (Abs t0 t1); Auto).
Discriminate.
(Apply trans_conv_conv with t; Auto).
(Red; Intros).
(Elim church_rosser with (Srt s) (App t0 t1); Intros).
Generalize H1 .
(Elim red_normal with (App t0 t1) x0; Auto; Intros).
(Apply red_sort_sort with s (App t0 t1); Auto).
Discriminate.
(Apply trans_conv_conv with t; Auto).
(Red; Intros).
(Elim church_rosser with (Srt s) (Prod t0 t1); Intros).
Generalize H1 .
(Elim red_normal with (Prod t0 t1) x0; Auto; Intros).
(Apply red_sort_sort with s (Prod t0 t1); Auto).
Discriminate.
(Apply trans_conv_conv with t; Auto).
Save.
Lemma
red_to_prod: (t:term)(sn t)->
{p:term*term| Cases p of
(u,v) => (red t (Prod u v)) end}
+{(u,v:term)~(conv t (Prod u v))}.
Realizer [t:term]Cases (compute_nf t) of
(Prod a b) => (inleft (term*term) (a,b))
| _ => (inright (term*term))
end.
Program_all.
(Red; Intros).
Apply (conv_sort_prod t0 u v).
(Apply trans_conv_conv with t; Auto).
(Apply sym_conv; Auto).
(Red; Intros).
(Elim church_rosser with (Prod u v) (Ref t0); Intros).
Generalize H1 .
(Elim red_normal with (Ref t0) x0; Auto; Intros).
(Apply red_prod_prod with u v (Ref t0); Auto; Intros).
Discriminate H4.
(Apply trans_conv_conv with t; Auto).
(Red; Intros).
(Elim church_rosser with (Prod u v) (Abs t0 t1); Intros).
Generalize H1 .
(Elim red_normal with (Abs t0 t1) x0; Auto; Intros).
(Apply red_prod_prod with u v (Abs t0 t1); Auto; Intros).
Discriminate H4.
(Apply trans_conv_conv with t; Auto).
(Red; Intros).
(Elim church_rosser with (Prod u v) (App t0 t1); Intros).
Generalize H1 .
(Elim red_normal with (App t0 t1) x0; Auto; Intros).
(Apply red_prod_prod with u v (App t0 t1); Auto; Intros).
Discriminate H4.
(Apply trans_conv_conv with t; Auto).
(Left; Exists (a,b); Intros;Auto).
Save.
Section TypeChecker.
Inductive
type_error: Set :=
Under: term -> type_error -> type_error
| Expected_type: term -> term -> term -> type_error
| Kind_ill_typed: type_error
| Db_error: nat -> type_error
| Lambda_kind: term -> type_error
| Not_a_type: term -> term -> type_error
| Not_a_fun: term -> term -> type_error
| Apply_err: term -> term -> term -> term -> type_error.
(* meaning of errors *)
Inductive
expln: env->type_error->Prop :=
Exp_under: (e:env)(t:term)(err:type_error)
(expln (cons ? t e) err)
->(expln e (Under t err))
| Exp_exp_type: (e:env)(m,at,et:term)(typ e m at)
->~(typ e m et)
->(free_db (length ? e) et)
->(expln e (Expected_type m at et))
| Exp_kind: (e:env)(wf e)
->((t:term)~(typ e (Srt kind) t))
->(expln e Kind_ill_typed)
| Exp_db: (e:env)(n:nat)(wf e)
->(le (length ? e) n)
->(expln e (Db_error n))
| Exp_lam_kind: (e:env)(m,t:term)(typ (cons ? t e) m (Srt kind))
->(expln e (Lambda_kind (Abs t m)))
| Exp_type: (e:env)(m,t:term)(typ e m t)
->((s:sort)~(typ e m (Srt s)))
->(expln e (Not_a_type m t))
| Exp_fun: (e:env)(m,t:term)(typ e m t)
->((a,b:term)~(typ e m (Prod a b)))
->(expln e (Not_a_fun m t))
| Exp_appl_err: (e:env)(u,v,a,b,tv:term)
(typ e u (Prod a b))
->(typ e v tv)
->~(typ e v a)
->(expln e (Apply_err u (Prod a b) v tv)).
Hint Exp_under Exp_exp_type Exp_kind Exp_db Exp_lam_kind
Exp_type Exp_fun Exp_appl_err.
Lemma
expln_wf: (e:env)(err:type_error)(expln e err)->(wf e).
(Induction 1; Intros; Auto).
Inversion_clear H1.
(Apply typ_wf with t (Srt s); Auto).
(Apply typ_wf with m at; Auto).
(Cut (wf (cons ? t e0)); Intros).
Inversion_clear H1.
(Apply typ_wf with t (Srt s); Auto).
(Apply typ_wf with m (Srt kind); Auto).
(Apply typ_wf with m t; Auto).
(Apply typ_wf with m t; Auto).
(Apply typ_wf with v tv; Auto).
Save.
Inductive
inf_error: term -> type_error -> Prop :=
Infe_subt: (m,n:term)(err:type_error)
(subt_nobind m n)
->(inf_error m err)
->(inf_error n err)
| Infe_under: (m,n,T:term)(err:type_error)
(subt_bind T m n)
->(inf_error m err)
->(inf_error n (Under T err))
| Infe_kind: (inf_error (Srt kind) Kind_ill_typed)
| Infe_db: (n:nat)(inf_error (Ref n) (Db_error n))
| Infe_lam_kind: (M,T:term)
(inf_error (Abs T M) (Lambda_kind (Abs T M)))
| Infe_type_abs: (m,n,t:term)
(inf_error (Abs m n) (Not_a_type m t))
| Infe_fun: (m,n,t:term)
(inf_error (App m n) (Not_a_fun m t))
| Infe_appl_err: (m,n,tf,ta:term)
(inf_error (App m n) (Apply_err m tf n ta))
| Infe_type_prod_l: (m,n,t:term)
(inf_error (Prod m n) (Not_a_type m t))
| Infe_type_prod_r: (m,n,t:term)
(inf_error (Prod m n) (Under m (Not_a_type n t))).
Hint Infe_kind Infe_db Infe_lam_kind Infe_type_abs
Infe_fun Infe_appl_err Infe_type_prod_l Infe_type_prod_r.
Lemma
inf_error_no_type: (m:term)(err:type_error)
(inf_error m err)
->(e:env)(expln e err)
->(t:term)~(typ e m t).
(Induction 1; Intros).
(Inversion_clear H0; Red; Intros).
(Apply inv_typ_abs with e m0 n0 t; Intros; Auto).
(Elim H2 with e (Srt s1); Auto).
(Apply inv_typ_app with e m0 v t; Intros; Auto).
(Elim H2 with e (Prod V Ur); Auto).
(Apply inv_typ_app with e u m0 t; Intros; Auto).
(Elim H2 with e V; Auto).
(Apply inv_typ_prod with e m0 n0 t; Intros; Auto).
(Elim H2 with e (Srt s1); Auto).
Inversion_clear H3.
(Inversion_clear H0; Red; Intros).
(Apply inv_typ_abs with e T m0 t; Intros; Auto).
(Elim H2 with (cons term T e) T0; Auto).
(Apply inv_typ_prod with e T m0 t; Intros; Auto).
(Elim H2 with (cons term T e) (Srt s2); Auto).
(Inversion_clear H0; Auto).
(Red; Intros).
(Apply inv_typ_ref with e t n; Intros; Auto).
Inversion_clear H0.
Generalize H5 .
(Elim H2; Simpl; Intros; Auto).
Inversion_clear H0.
Inversion_clear H0.
(Red; Intros).
(Apply inv_typ_abs with e T M t; Intros; Auto).
(Elim inv_typ_conv_kind with (cons term T e) T0 (Srt s2); Auto).
(Apply typ_unique with (cons term T e) M; Auto).
Inversion_clear H0.
(Red; Intros).
(Apply inv_typ_abs with e m0 n t0; Intros; Auto).
(Elim H2 with s1; Auto).
Inversion_clear H0.
(Red; Intros).
(Apply inv_typ_app with e m0 n t0; Intros; Auto).
(Elim H2 with V Ur; Auto).
Inversion_clear H0.
(Red; Intros).
(Apply inv_typ_app with e m0 n t; Intros; Auto).
(Elim type_case with e m0 (Prod a b); Intros; Auto).
Inversion_clear H7.
(Apply inv_typ_prod with e a b (Srt x); Intros; Auto).
Apply H3.
(Apply type_conv with V s1; Auto).
Apply inv_conv_prod_l with Ur b.
(Apply typ_unique with e m0; Auto).
Discriminate H7.
Inversion_clear H0.
(Red; Intros).
(Apply inv_typ_prod with e m0 n t0; Intros; Auto).
(Elim H2 with s1; Auto).
Inversion_clear H0.
Inversion_clear H1.
(Red; Intros).
(Apply inv_typ_prod with e m0 n t0; Intros; Auto).
(Elim H2 with s2; Auto).
Save.
Theorem
infer: (e:env)(t:term)(wf e)
->{ T:term | (typ e t T) }
+{ err:type_error | (expln e err) & (inf_error t err) }.
(*Realizer [e:env][m:term]
(Fix inf_rec {inf_rec/1: term->env->(sum term ty_err) :=
[m:term][e:env]Cases m of
(Srt kind) => (fail (Ill_typed (Srt kind)))
| (Srt prop) => (ok (Srt kind))
| (Ref n) => Cases (list_item term e n) of
(inleft T) => (ok (lift (S n) T))
| _ => (fail (Ill_typed (Ref n)))
end
| (Abs t b) => Cases (inf_rec t e) of
(inl T) => Cases (red_to_sort T)
(inf_rec b (cons term t e)) of
(inleft _) (inl B) => if (eqterm (Srt kind) B)
then (fail (Topsorted b))
else (ok (Prod t B))
| inright _ => (fail (Not_a_type t))
| (inleft _) (inr err) => (bind t err)
end
| (inr err) =>(inr term ? err)
end
| (App t b) => Cases (inf_rec t e) of
(inl T) => Cases (red_to_prod T) of
(inleft (V,Ur)) => Cases (inf_rec b e) of
(inl B) => if (is_conv V B)
then (ok (subst b Ur))
else (fail (Expected_type b B V))
| (inr err) => (inr term ? err)
end
| _ => (fail (Not_a_fun t T))
end
| (inr err) => (inr term ? err)
end
| (Prod t b) => Cases (inf_rec t e) of
(inl T) => Cases (red_to_sort T)
(inf_rec b (cons term t e)) of
(inleft _) (inl B) => Cases (red_to_sort B) of
(inleft s) => (ok (Srt s))
| _ =>(fail (Not_a_type b))
end
| inright _ => (fail (Not_a_type t))
| (inleft _) (inr err) => (bind t err)
end
| (inr err) => (inr term ? err)
end
end} m e).
*)
Do 2 Intro.
Generalize t e .
Clear e t.
Fix 1.
Intros e wfe.
Case t.
Destruct s.
Right.
(Exists Kind_ill_typed; Auto).
(Apply Exp_kind; Intros; Auto).
Apply inv_typ_kind.
Left.
Exists (Srt kind).
(Apply type_prop; Auto).
Intros.
(Elim (list_item term e n); Intros).
Elim y.
Intros T H0.
Left.
Exists (lift (S n) T).
(Apply type_var; Auto).
(Exists T; Auto).
Right.
(Exists (Db_error n); Auto).
(Apply Exp_db; Auto).
Generalize n y .
(Elim e; Simpl; Auto).
(Destruct n; Intros).
(Elim y0 with a; Auto).
(Cut (le (length ? l) n1); Auto).
Apply H.
(Red; Intros).
(Elim y0 with t0; Auto).
Intros a b.
(Elim (infer a e); Intros; Trivial).
Elim y.
Intros T H0.
(Elim (red_to_sort T); Intros; Trivial).
(Elim y0; Intros).
(Cut (wf (cons ? a e)); Intros).
(Elim (infer b (cons ? a e)); Trivial; Intros).
Elim y2.
Intros B H1.
(Elim (eqterm (Srt kind) B); Intros).
Right.
(Exists (Lambda_kind (Abs a b)); Auto).
(Apply Exp_lam_kind; Auto).
(Rewrite -> y3; Auto).
Left.
Exists (Prod a B).
(Elim type_case with (cons term a e) b B; Intros; Auto).
Inversion_clear H2.
(Apply type_abs with x x0; Auto).
(Apply type_reduction with T; Auto).
(Elim y3; Auto).
Right.
Inversion_clear y2.
(Exists (Under a x0); Auto).
(Apply Infe_under with b; Auto).
Apply wf_var with x.
(Apply type_reduction with T; Auto).
Right.
(Exists (Not_a_type a T); Auto).
(Apply Exp_type; Auto).
(Red; Intros).
Elim y0 with s.
(Apply typ_unique with e a; Auto).
(Apply type_sn with e a; Auto).
Right.
Inversion_clear y.
(Exists x; Auto).
(Apply Infe_subt with a; Auto).
Intros u v.
(Elim infer with u e; Trivial; Intros).
Elim y.
Intros T H.
(Elim red_to_prod with T; Intros).
Elim y0.
Destruct x.
Intros V Ur H0.
(Cut (typ e u (Prod V Ur)); Intros).
(Elim infer with v e; Trivial; Intros).
Elim y1.
Intros B H2.
(Elim is_conv with V B; Intros).
Left.
Exists (subst v Ur).
(Apply type_app with V; Auto).
(Elim type_case with e u (Prod V Ur); Intros; Auto).
Inversion_clear H3.
(Apply inv_typ_prod with e V Ur (Srt x0); Intros; Auto).
(Apply type_conv with B s1; Auto).
Discriminate H3.
Right.
(Exists (Apply_err u (Prod V Ur) v B); Auto).
(Apply Exp_appl_err; Auto).
(Red; Intros).
Apply y2.
(Apply typ_unique with e v; Auto).
(Apply subterm_sn with (Prod V Ur); Auto).
(Apply sn_red_sn with T; Auto).
(Apply type_sn with e u; Auto).
(Apply type_sn with e v; Auto).
Right.
Inversion_clear y1.
(Exists x0; Auto).
(Apply Infe_subt with v; Auto).
(Apply type_reduction with T; Auto).
Right.
(Exists (Not_a_fun u T); Auto).
(Apply Exp_fun; Auto).
(Red; Intros).
Elim y0 with a b.
(Apply typ_unique with e u; Auto).
(Apply type_sn with e u; Auto).
Right.
Inversion_clear y.
(Exists x; Auto).
(Apply Infe_subt with u; Auto).
Intros a b.
(Elim infer with a e; Intros; Trivial).
Elim y.
Intros T H.
(Elim red_to_sort with T; Intros).
(Elim y0; Intros).
(Cut (wf (cons ? a e)); Intros).
(Elim infer with b (cons ? a e); Trivial; Intros).
Elim y2.
Intros B H1.
(Elim red_to_sort with B; Intros).
Elim y3.
Intros s H2.
Left.
Exists (Srt s).
(Apply type_prod with x; Auto).
(Apply type_reduction with T; Auto).
(Apply type_reduction with B; Auto).
Right.
(Exists (Under a (Not_a_type b B)); Auto).
(Apply Exp_under; Auto).
(Apply Exp_type; Auto).
(Red; Intros).
Elim y3 with s.
(Apply typ_unique with (cons term a e) b; Auto).
(Apply type_sn with (cons term a e) b; Auto).
Right.
Inversion_clear y2.
(Exists (Under a x0); Auto).
(Apply Infe_under with b; Auto).
Apply wf_var with x.
(Apply type_reduction with T; Auto).
Right.
(Exists (Not_a_type a T); Auto).
(Apply Exp_type; Auto).
(Red; Intros).
Elim y0 with s.
(Apply typ_unique with e a; Auto).
(Apply type_sn with e a; Auto).
Right.
Inversion_clear y.
(Exists x; Auto).
(Apply Infe_subt with a; Auto).
Save.
Inductive
chk_error [m,t:term]: type_error -> Prop :=
Chke_subj: (err:type_error)(inf_error m err)
->(chk_error m t err)
| Chke_type: (err:type_error)(inf_error t err)
->~t=(Srt kind)
->(chk_error m t err)
| Chke_exp: (at:term)(chk_error m t (Expected_type m at t)).
Hint Chke_subj Chke_type Chke_exp.
Lemma
chk_error_no_type: (e:env)(m,t:term)(err:type_error)
(chk_error m t err)
->(expln e err)
->~(typ e m t).
(Destruct 1; Intros).
(Apply inf_error_no_type with err0; Auto).
(Red; Intros).
(Elim type_case with e m t; Intros; Auto).
Inversion_clear H4.
(Elim inf_error_no_type with t err0 e (Srt x); Auto).
(Inversion_clear H0; Auto).
Save.
Lemma
check_typ: (e:env)(t,tp:term)(wf e)
-> { err:type_error | (expln e err) & (chk_error t tp err) }
+ { (typ e t tp) }.
(*
Realizer [e:env][t,tp:term]
Cases (infer e t) (eqterm (Srt kind) tp) of
(inl tp') inleft => if (eqterm (Srt kind) tp')
then (inright type_error)
else (inleft ? (fail t (nil ?)
(Expected_type t tp' (Srt kind))))
| (inl tp') inright => Cases (infer e tp) of
(inl k) => if (is_conv tp tp')
then (inright type_error)
else (inleft ? (fail t (nil ?)
(Expected_type t tp' tp)))
| (inr err) => (inleft type_error err)
end
| (inr err) _ => (inleft type_error err)
end.
*)
Intros.
(Elim infer with e t; Intros; Auto).
(Elim y; Intros tp').
Intros.
(Elim eqterm with (Srt kind) tp; Intros).
(Elim eqterm with (Srt kind) tp'; Intros).
Right.
Elim y1.
(Rewrite -> y2; Auto).
Left.
(Exists (Expected_type t tp' tp); Auto).
(Apply Exp_exp_type; Auto).
(Red; Intros; Apply y2).
Symmetry.
(Apply type_kind_not_conv with e t; Auto).
(Rewrite -> y1; Auto).
(Elim y1; Auto).
(Elim infer with e tp; Intros; Auto).
(Elim y2; Intros k H0).
(Elim is_conv with tp tp'; Intros).
Right.
(Elim red_to_sort with k; Intros; Auto).
Inversion_clear y4.
(Apply type_conv with tp' x; Auto).
(Apply type_reduction with k; Auto).
(Elim type_case with e t tp'; Intros; Auto).
Inversion_clear H1.
Elim y4 with x.
(Apply typ_conv_conv with e tp tp'; Auto).
(Elim inv_typ_conv_kind with e tp k; Auto).
(Elim H1; Auto).
(Apply type_sn with e tp; Auto).
Left.
(Exists (Expected_type t tp' tp); Auto).
(Apply Exp_exp_type; Auto).
(Red; Intros; Apply y3; Apply typ_unique with e t; Auto).
(Apply typ_free_db with k; Auto).
(Apply str_norm with e k; Auto).
(Apply type_sn with e t; Auto).
Left.
Inversion_clear y2.
(Exists x; Auto).
Left.
(Inversion_clear y; Auto).
(Exists x; Auto).
Save.
Inductive
decl_error [m:term]: type_error -> Prop :=
Decax_ill: (err:type_error)(inf_error m err)
->(decl_error m err)
| Decax_type: (t:term)(decl_error m (Not_a_type m t)).
Hint Decax_ill Decax_type.
Lemma
decl_err_not_wf: (e:env)(t:term)(err:type_error)
(decl_error t err)
->(expln e err)
->~(wf (cons ? t e)).
Red.
(Destruct 1; Intros).
Inversion_clear H2.
(Elim inf_error_no_type with t err0 e (Srt s); Auto).
Inversion_clear H0.
Inversion_clear H1.
(Elim H3 with s; Auto).
Save.
Lemma
add_typ: (e:env)(t:term)(wf e)
->{ err:type_error | (expln e err) & (decl_error t err) }
+{ (wf (cons ? t e)) }.
Intros.
(Elim infer with e t; Intros; Auto).
Inversion_clear y.
(Elim red_to_sort with x; Intros).
Inversion_clear y.
Right.
Apply wf_var with x0.
(Apply type_reduction with x; Auto).
Left.
(Exists (Not_a_type t x); Auto).
(Apply Exp_type; Auto).
(Red; Intros).
Elim y with s.
(Apply typ_unique with e t; Auto).
(Apply type_sn with e t; Auto).
Left.
Inversion_clear y.
(Exists x; Auto).
Save.
End TypeChecker.
Section Decidabilite_typage.
Lemma
decide_wf: (e:env){(wf e)}+{~(wf e)}.
Realizer Fix dec_wf { dec_wf/1: env->sumbool :=
[e:env]Cases e of
nil => left
| (cons t f) =>
if (dec_wf f)
then Cases (add_typ f t) of
(inleft err) => right
| inright => left
end
else right
end}.
Program_all.
Apply wf_nil.
(Apply decl_err_not_wf with err0; Auto).
(Red; Intros; Apply n).
Inversion_clear H.
(Apply typ_wf with t (Srt s); Auto).
Save.
Lemma
decide_typ: (e:env)(t,tp:term){(typ e t tp)}+{~(typ e t tp)}.
Realizer [e:env][t,tp:term]
if (decide_wf e)
then Cases (check_typ e t tp) of
(inleft err) => right
| inright => left
end
else right.
Program_all.
(Apply chk_error_no_type with err0; Auto).
(Red; Intros; Apply n).
(Apply typ_wf with t tp; Auto).
Save.
End Decidabilite_typage.
16/04/97, 15:32