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)
                        (c(k_grror 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