Infer.v


Transparent sumor_rec.
Transparent sumbool_rec.
Transparent sig_rec.


  Definition infer_ppal_type: env->term->Set :=
      [e;t](ppal_dec (typ e t) (le_type e)).

  (* The type-checking module to build *)

  Record
PTS_TC: Set := {
    (* Infer command *)
    ptc_inf_ppal_type: (e:env)(t:term)(wf e)->(
infer_ppal_type e t);
    (* Check command *)
    ptc_chk_typ: (e:env)(t,T:term)(wf e)->(decide (typ e t T));
    (* Axiom command *)
    ptc_add_typ: (e:env)(t:term)(wf e)->(decide (wf (cons (Ax t) e)));
    (* Definition command *)
    ptc_add_def: (e:env)(t,T:term)(wf e)
                        ->(decide (wf (cons (Def t T) e)));

    (* Auxiliary functions. Would be useful to write tactics
       over the kernel. *)

    ptc_chk_wk: (e:env)(t,T:term)(wf e)->(wf_type e T)
                                  ->(decide (typ e t T));
    ptc_chk_wft: (e:env)(t:term)(wf e)->(decide (wf_type e t))
  }.




  Theorem is_a_sort: (t:term)(decide (EX s:sort | t=(Srt s))).
(Destruct t; Intros).
(Left; Exists s; Auto with arith pts).

(Right; Red; Induction 1; Intros).
Discriminate H0.

(Right; Red; Induction 1; Intros).
Discriminate H0.

(Right; Red; Induction 1; Intros).
Discriminate H0.

(Right; Red; Induction 1; Intros).
Discriminate H0.
Save.




  Definition
typed_sort: (relation sort)->sort->Prop :=
      [axiom; s](EX s2 | (axiom s s2)).

  Definition
red_to_sort_dec: env->term->Set :=
      [e;t](ppal_dec [s](le_type e t (Srt s)) le_sort).

  Definition
red_to_wf_prod_dec: env->term->Set :=
      [e;t]
     { p:term*term | let (C,D) = p in
           (wf_type e (Prod C D)) /\ (le_type e t (Prod C D))
             /\ ((A,B:term)(le_type e t (Prod A B))
                    ->(le_type e (Prod C D) (Prod A B))) }
     + { (C,D:term)~(le_type e t (Prod C D)) }.


  (* Algorithms and properties implying the decidability of typing *)
  Record
PTS_algos : Set := {
    pa_lift: (n:nat)(t:term){ u:term | u=(lift n t) };
    pa_subst: (u,v:term){ t:term | t=(subst u v) };
    pa_infer_axiom: (s:sort)(ppal_dec (axiom s) le_sort);
    pa_least_sort: (e:env)(t:term)(wf_type e t) -> (
red_to_sort_dec e t);
    pa_infer_rule: (x1,x2:sort){ x3:sort | (ppal (rule_sat x1 x2) le_sort x3)};
    pa_least_prod: (e:env)(t:term)(wf_type e t) -> (red_to_wf_prod_dec e t);
    pa_le_type_prod: (e:env)(T,A,B:term)(le_type (cons (Ax T) e) A B)
                  ->(le_type e (Prod T A) (Prod T B));
    pa_inv_prod: (product_inversion le_type);
    pa_topsort_untyped: (e:env)(s,s':sort)(t:term)
        (le_type e (Srt s) t)->(typ e t (Srt s'))->(typed_sort axiom s);
    pa_le_type_dec: (e:env)(u,v:term)(wf_type e u)->(wf_type e v)
                        ->(decide (le_type e u v))
  }.


  Variable the_algos: PTS_algos.


  Lemma not_topsort: (t:term)
      (decide (s:sort)t=(Srt s)->(
typed_sort axiom s)).
Realizer [t:term]
  Cases t of
    (Srt s) => Cases (pa_infer_axiom the_algos s) of
                 (inleft _) => true
               | _ => false
               end
  | _ => true
  end.
(Program_all; Try ((Intros s' eqs'; Discriminate eqs'))).
(Intros s' eqss'; Injection eqss').
(Induction 1; Split with a0).
Apply (pp_ok p).

(Red; Intros).
(Elim H with s; Intros; Trivial with arith pts).
(Elim n with x; Trivial with arith pts).
Save.



Section Fixpoint_Body.

  (* Useful for the mutual recursion  type inference <-> type checking *)

  Hypothesis fix_inference: (t:term)(e:env)(wf e) -> (infer_ppal_type e t).


  Theorem fix_chk_wk: (e:env)(t,T:term)(wf e)->(wf_type e T)
                                  ->(decide (typ e t T)).
Realizer [e:env][t,T:term]Cases (fix_inference t e) of
     (inleft T') =>(pa_le_type_dec the_algos e T' T)
   | _ => false
   end.
Program_all.
(Apply type_correctness with 1:=(pp_ok p); Auto with arith pts).

(Apply typ_conv_wf with T'0; Auto with arith pts).
Apply (pp_ok p).

(Red; Intros; Apply n).
(Apply pp_least with 1:=p; Trivial with arith pts).
Defined.


  Theorem
fix_add_typ: (e:env)(t:term)(wf e)
                              ->(decide (wf (cons (Ax t) e))).
Realizer [e:env][t:term]
  Cases (fix_inference t e) of
    (inleft T) => Cases (pa_least_sort the_algos e T) of
                    (inleft s) => true
                  | _ => false
                  end
  | _ => false
  end.
Program_all.
(Apply type_correctness with 1:=(pp_ok p); Auto with arith pts).

Apply wf_var with s0.
(Apply typ_conv_wf with T0; Auto with arith pts).
Apply (pp_ok p).

(Red; Intros).
Generalize (pp_ok p0).
Trivial with arith pts.

(Red; Intros).
Inversion_clear H0.
(Elim n with s; Auto with arith pts).
Apply (pp_least p) with 1:=H1.

(Red; Intros).
Inversion_clear H0.
(Elim n with (Srt s); Auto with arith pts).
Defined.



Section Infer_Ref.


  Theorem
infer_ref: (e:env)(n:nat)(wf e) -> (infer_ppal_type e (Ref n)).
Realizer [e:env][n:nat]
  Cases (list_item decl e n) of
    (inleft d) => (inleft ? (pa_lift the_algos (S n) (typ_of_decl d)))
  | _ => (inright term)
  end.
Program_all.
Rewrite e0.
(Split; Intros).
(Apply type_var; Auto with arith pts).
(Split with d0; Auto with arith pts).

(Red; Intros).
Inversion_typ H0.
(Elim fun_item with decl x0 d0 e n; Auto with arith pts).

(Red; Intros).
Inversion_typ H0.
(Elim n0 with x0; Auto with arith pts).
Save.

End Infer_Ref.


Section Infer_Application.

  Local le_type_prod_l:= (inv_prod_l ? (pa_inv_prod the_algos)).
  Local le_type_prod_r:= (inv_prod_r ? (pa_inv_prod the_algos)).


  Theorem infer_app: (e:env)(u,v:term)(wf e)->(infer_ppal_type e (App u v)).
Realizer [e:env][u,v:term]
  Cases (fix_inference u e) of
    (inleft y) => Cases (pa_least_prod the_algos e y) of
                    (inleft (t,t0)) =>
                          if (fix_chk_wk e v t)
                          then (inleft ? (pa_subst the_algos v t0))
                          else (inright term)
                  | _ => (inright term)
                  end
  | _ => (inright term)
  end.
Program_all.
(Apply type_correctness with 1:=(pp_ok p); Auto with arith pts).

Inversion_clear y1.
(Apply wf_type_prod_l with t0; Auto with arith pts).

Rewrite e0.
(Split; Intros).
(Apply type_app with t; Auto with arith pts).
Inversion_clear y1.
Inversion_clear H1.
(Apply typ_conv_wf with y0; Auto with arith pts).
Apply (pp_ok p).

Inversion_typ H0.
(Apply le_type_trans with (subst v Ur); Auto with arith pts).
Unfold subst.
(Apply le_type_subst with e (Ax V) (cons (Ax V) e); Auto with arith pts).
(Apply le_type_prod_r with t; Auto with arith pts).
Inversion_clear y1.
(Inversion_clear H5; Auto with arith pts).
Apply H7.
Apply (pp_least p) with 1:=H2.

(Red; Intros).
Inversion_typ H0.
Apply n.
Inversion_clear y1.
Inversion_clear H5.
(Apply typ_conv_wf with V; Auto with arith pts).
(Apply wf_type_prod_l with t0; Auto with arith pts).

(Apply le_type_prod_l with t0 Ur; Auto with arith pts).
Apply H7.
Apply (pp_least p) with 1:=H2.

(Red; Intros).
Inversion_typ H0.
(Elim n with V Ur; Auto with arith pts).
Apply (pp_least p) with 1:=H2.

(Red; Intros).
Inversion_typ H0.
(Elim n with (Prod V Ur); Auto with arith pts).
Defined.


End Infer_Application.



  Theorem infer_sort: (e:env)(s:sort)(wf e) -> (infer_ppal_type e (Srt s)).
Unfold infer_ppal_type.
Intros.
(Elim (pa_infer_axiom the_algos) with s; Intros).
Left.
Inversion_clear y.
Split with (Srt x).
(Split; Intros).
(Constructor; Auto with arith pts).
Apply (pp_ok H0).

(Generalize (pp_least H0); Intros).
Red in H2.
Inversion_typ H1.
(Apply le_type_trans with 2:=H4; Auto with arith pts).

(Right; Red; Intros).
Inversion_typ H0.
(Elim y with s2; Trivial with arith pts).
Defined.


  Theorem infer_abs: (e:env)(A,M:term)(wf e)
                              -> (
infer_ppal_type e (Abs A M)).
Realizer [e:env][A,M:term]
  if (fix_add_typ e A)
  then Cases (fix_inference M (cons ? (Ax A) e)) of
         (inleft TM) =>
            if (not_topsort TM) then (inleft ? (Prod A TM))
            else (inright term)
       | _ => (inright term)
       end
  else (inright term).
Program_all.
(Split; Intros).
(ElimType (EX s':sort | (typ (cons (Ax A) e) TM0 (Srt s'))); Intros).
Inversion_clear w.
(Elim (pa_infer_rule the_algos) with s x; Intros).
(Apply type_abs with x0; Auto with arith pts).
(Apply type_prod_sat with s x; Auto with arith pts).
Apply (pp_ok y).

Apply (pp_ok p).

Generalize t.
(Elim type_correctness with 1:=(pp_ok p); Intros).
(Split with s; Trivial with arith pts).

(Elim t0 with s; Trivial with arith pts; Intros).
Split with x.
(Constructor; Auto with arith pts).

Inversion_typ H0.
Apply le_type_trans with 2:=H3.
(Apply (pa_le_type_prod the_algos); Auto with arith pts).
Apply (pp_least p) with 1:=H1.

(Red; Intros).
Inversion_typ H0.
(Apply n; Intros).
Inversion_typ H2.
Apply (pa_topsort_untyped the_algos) with 2:=H7.
Elim H4.
Apply (pp_least p) with 1:=H1.

(Red; Intros).
Inversion_typ H0.
(Elim n with U; Trivial with arith pts).

(Red; Intros).
Inversion_typ H0.
Apply n.
Apply typ_wf with 1:=H1.
Defined.


  Theorem infer_prod: (e:env)(A,B:term)(wf e)
                       -> (
infer_ppal_type e (Prod A B)).
Intros.
(Elim fix_inference with A e; Intros).
Inversion_clear y.
(Elim (pa_least_sort the_algos) with e x; Intros).
Inversion_clear y.
(Cut (wf (cons (Ax A) e)); Intros).
(Elim fix_inference with B (cons (Ax A) e); Intros).
Inversion_clear y.
(Elim (pa_least_sort the_algos) with (cons (Ax A) e) x1; Intros).
Inversion_clear y.
Left.
(Elim (pa_infer_rule the_algos) with x0 x2; Intros).
(Split with (Srt x3); Split; Intros).
(Apply type_prod_sat with x0 x2; Auto with arith pts).
(Apply typ_conv_wf with x; Auto with arith pts).
Apply (pp_ok H0).

Apply (pp_ok H1).

(Apply typ_conv_wf with x1; Auto with arith pts).
Apply (pp_ok H3).

Apply (pp_ok H4).

Apply (pp_ok y).

Inversion_typ H5.
Apply le_type_trans with 2:=H9.
Unfold le_sort in y.
Apply (pp_least y).
Split with s1.
Apply (pp_least H1).
(Apply (pp_least H0); Trivial with arith pts).

(Split with s2; Trivial with arith pts).
Apply (pp_least H4).
(Apply (pp_least H3); Trivial with arith pts).

(Right; Red; Intros).
Inversion_typ H4.
(Elim y with s2; Auto with arith pts).
(Apply (pp_least H3); Trivial with arith pts).

(Apply type_correctness with 1:=(pp_ok H3); Auto with arith pts).

(Right; Red; Intros).
Inversion_typ H3.
(Elim y with (Srt s2); Auto with arith pts).

Trivial with arith pts.

(Apply wf_var with x0; Auto with arith pts).
(Apply typ_conv_wf with x; Auto with arith pts).
Apply (pp_ok H0).

Apply (pp_ok H1).

(Right; Red; Intros).
Inversion_typ H1.
(Elim y with s1; Auto with arith pts).
Apply (pp_least H0) with 1:=H3.

(Apply type_correctness with 1:=(pp_ok H0); Auto with arith pts).

(Right; Red; Intros).
Inversion_typ H0.
(Elim y with (Srt s1); Auto with arith pts).

Auto with arith pts.
Defined.


End Fixpoint_Body.



Section Infer_Full_PTS.

  Fixpoint full_ppal_type [t:term]:
               (e:env)(wf e)->(
infer_ppal_type e t) :=
   [e;H]<[t:term](infer_ppal_type e t)>Cases t of
     (Srt s) => (infer_sort e s H)
   | (Ref n) => (infer_ref e n H)
   | (Abs A M) => (infer_abs full_ppal_type e A M H)
   | (App u v) => (infer_app full_ppal_type e u v H)
   | (Prod A B) => (infer_prod full_ppal_type e A B H)
   end.


  Local add_typ := (fix_add_typ full_ppal_type).

  Local check_typ_when_wf := (fix_chk_wk full_ppal_type).

  Local add_cst: (e:env)(t,T:term)(wf e)
                            ->(decide (wf (cons (Def t T) e))).
Realizer [e:env; t,T:term]
  (andb (add_typ e T) (check_typ_when_wf e t T)).
Program_all.
Inversion_clear w.
(Left with s; Trivial with arith pts).

Inversion_clear w.
(Apply wf_cst with s; Trivial with arith pts).

(Red; Intro; Apply n).
(Inversion_clear H0; Trivial with arith pts).

(Red; Intro; Apply n).
Inversion_clear H0.
(Apply wf_var with s; Trivial with arith pts).
Save.



  Local check_wf_type: (e:env)(t:term)(wf e)->(decide (wf_type e t)).
Realizer [e:env; t:term](orb (is_a_sort t) (add_typ e t)).
Program_all.
Inversion_clear e0.
(Rewrite -> H0; Auto with arith pts).

(Inversion_clear w; Auto with arith pts).
(Apply wft_typed with s; Auto with arith pts).

(Red; Intros).
Inversion H0.
Apply n0.
(Apply wf_var with s; Auto with arith pts).

Apply n.
(Exists s; Auto with arith pts).
Save.


  Local check_type: (e:env)(t,T:term)(wf e)->(decide (typ e t T)).
Realizer [e:env; t,T:term](andb (check_wf_type e T) (check_typ_when_wf e t T)).
Program_all.
(Red; Intros; Apply n).
(Apply type_correctness with t; Auto with arith pts).
Save.




  Definition full_type_checker: PTS_TC :=
    (Build_PTS_TC [e;t](full_ppal_type t e) check_type
                        add_typ add_cst check_typ_when_wf check_wf_type).


  (* Decidability of judgements *)
  Theorem decide_wf: (e:env)(decide (wf e)).
(Induction e; Intros; Auto with arith pts).
(Elim H; Intros).
(Elim a; Intros).
(Apply add_typ; Auto with arith pts).

(Apply add_cst; Auto with arith pts).

(Right; Red; Intros).
Apply y.
(Apply inv_wf with a; Auto with arith pts).
Save.


  Theorem
decide_typ: (e:env)(t,T:term)(decide (typ e t T)).
Intros.
(Elim
decide_wf with e; Intros).
(Apply check_type; Auto with arith pts).

(Right; Red; Intros).
Apply y.
(Apply typ_wf with t T; Auto with arith pts).
Save.

End Infer_Full_PTS.


23/12/98, 14:32