CumulInfer.v
Record
norm_sound_CTS: Prop := {
ncts_sr: (rule_sound cts_pts_functor hdr);
ncts_typ_sn: (e:env)(t,T:term)(typ cts_pts_functor e t T)
->(sn red_step e t)
}.
Variable the_ncts: norm_sound_CTS.
(* open *)
Local subj_red: (rule_sound cts_pts_functor hdr) := (ncts_sr the_ncts).
Local typ_sn: (e:env)(t,T:term)(typ cts_pts_functor e t T)
->(sn red_step e t) :=
(ncts_typ_sn the_ncts).
Lemma
cumul_type_sn: (e:env)(t:term)(wf_type cts_pts_functor e t)
->(sn red_step e t).
(Induction 1; Intros).
(Apply typ_sn with (Srt s); Auto with arith pts).
Red.
(Apply Acc_intro; Intros).
Inversion_clear H0.
(Elim shn_sort with e s (Srt s) y; Auto with arith pts).
Save.
Hints Resolve cumul_type_sn : pts.
Lemma
subject_reduction_cumul: (rule_sound cts_pts_functor (red hdr)).
Unfold red hdr .
Apply clos_refl_trans_sound.
(Apply ctxt_sound; Simpl; Auto 10 with arith pts).
Exact subj_red.
Save.
Lemma
sound_wf_type_cumul: (e:env)(T,U:term)(wf_type cts_pts_functor e T)
->(red hdr e T U)
->(wf_type cts_pts_functor e U).
(Induction 1; Intros).
Apply wft_typed with s.
(Apply subject_reduction_cumul with T0; Auto with arith pts).
(Cut (conv_hn_inv hd_rule e (Srt s) U); Intros).
(Inversion_clear H1; Auto with arith pts).
(Apply inv_red_hn; Auto with arith pts).
Save.
Lemma
cumul_least_sort: (e:env)(t:term)(wf_type cts_pts_functor e t)
-> (red_to_sort_dec cts_pts_functor e t).
Realizer [e:env; t:term]
Cases (whnf e t) of
(Srt s) => (inleft ? s)
| _ => (inright sort)
end.
(Program_all; Simpl).
Try Exists s.
(Split; Intros).
Auto with arith pts.
(Replace (R_rt cumul)
with (Rule (Le_type (pts_le_type cts_pts_functor))); Trivial with arith pts).
(Apply sub_sort_env_indep with e; Simpl).
(Apply cumul_trans with t; Auto 10 with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (Ref t0) (Srt x0)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Srt x0); Auto with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (Abs t0 t1) (Srt x0)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Srt x0); Auto with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (App t0 t1) (Srt x0)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Srt x0); Auto with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (Prod t0 t1) (Srt x0)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Srt x0); Auto with arith pts).
Save.
Lemma
cumul_least_prod: (e:env)(t:term)(wf_type cts_pts_functor e t)
-> (red_to_wf_prod_dec cts_pts_functor e t).
Realizer [e:env; t:term]
Cases (whnf e t) of
(Prod C D) => (inleft ? (pair ? ? C D))
| _ => (inright (prod term term))
end.
(Program_all; Simpl).
(Red; Intros).
(Cut (cumul_hn_inv e (Srt t0) (Prod C D)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Prod C D); Auto with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (Ref t0) (Prod C D)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Prod C D); Auto with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (Abs t0 t1) (Prod C D)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Prod C D); Auto with arith pts).
(Red; Intros).
(Cut (cumul_hn_inv e (App t0 t1) (Prod C D)); Intros).
Inversion_clear H1.
(Apply inv_cumul_hn with t (Prod C D); Auto with arith pts).
Left.
Exists (C,D).
Split.
(Apply sound_wf_type_cumul with t; Auto with arith pts).
Simpl.
(Split; Intros; Auto 10 with arith pts).
(Apply cumul_trans with t; Auto 10 with arith pts).
Save.
Hypothesis inf_axiom: (s:sort)(ppal_dec (axiom s) rt_univ).
Hypothesis inf_rule: (x1,x2:sort)
{ x3:sort | (rule x1 x2 x3) & (s1,s2,s3:sort)(rule s1 s2 s3)
->(rt_univ x1 s1)->(rt_univ x2 s2)->(rt_univ x3 s3) }.
Lemma
cumul_infer_axiom: (s:sort)
(ppal_dec (axiom s) [s1,s2](e:env)(rt_cumul e (Srt s1) (Srt s2))).
Intros.
(Elim inf_axiom with s; Intros).
Inversion_clear y.
Left.
(Split with x; Auto with arith pts).
(Split; Intros).
Apply (pp_ok H).
Fold rt_cumul.
Generalize (pp_least H).
Auto with arith pts.
(Right; Red; Intros).
(Elim y with x; Trivial with arith pts).
Save.
Lemma
cumul_infer_rule: (x1,x2:sort)
{ x3:sort | (ppal (rule_sat cts_pts_functor x1 x2)
[s1,s2](e:env)(rt_cumul e (Srt s1) (Srt s2)) x3)}.
Intros.
(Elim inf_rule with x1 x2; Intros; Auto with arith pts).
Split with x.
(Split; Intros).
(Split with x1; Simpl; Auto with arith pts).
(Split with x2; Simpl; Auto with arith pts).
(Cut (rt_univ x y1); Auto with arith pts).
Inversion_clear H.
Inversion_clear H1.
Simpl in H0 H H2.
(Apply y0 with x0 x3; Auto with arith pts).
(Cut (cumul_hn_inv e (Srt x1) (Srt x0)); Intros).
(Inversion_clear H1; Trivial with arith pts).
(Apply inv_cumul_hn with (Srt x1) (Srt x0); Auto with arith pts).
(Cut (cumul_hn_inv e (Srt x2) (Srt x3)); Intros).
(Inversion_clear H1; Trivial with arith pts).
(Apply inv_cumul_hn with (Srt x2) (Srt x3); Auto with arith pts).
Save.
Hypothesis univ_hierarchy: (s1,s2:sort)
(rt_univ s1 s2)->(typed_sort axiom s2)
->(typed_sort axiom s1).
Lemma
cumul_topsort_untyped: (e:env)(s,s':sort)(t:term)
(rt_cumul e (Srt s) t)
->(typ cts_pts_functor e t (Srt s'))->(typed_sort axiom s).
Intros.
(Elim whnf with e t; Intros).
(Cut (cumul_hn_inv e (Srt s) x); Intros).
Cut (typ cts_pts_functor e x (Srt s')).
Inversion_clear H1.
Intros.
Apply univ_hierarchy with 1:=H2.
Inversion_typ H1.
(Split with s2; Trivial with arith pts).
(Apply subject_reduction_cumul with t; Trivial with arith pts).
(Apply inv_cumul_hn with (Srt s) t; Auto with arith pts).
Apply typ_sn with 1:=H0.
Save.
Theorem
cts_prim_algos: (PTS_algos cts_pts_functor).
Apply Build_PTS_algos.
Exact lift_naif.
Exact subst_naif.
Exact cumul_infer_axiom.
Exact cumul_least_sort.
Exact cumul_infer_rule.
Exact cumul_least_prod.
Exact cumul_prod.
Exact cumul_inv_prod.
Exact cumul_topsort_untyped.
Intros.
Simpl.
(Apply CR_WHNF_cumul_dec; Auto with arith pts).
Save.
Theorem
full_cts_type_checker: (PTS_TC cts_pts_functor).
Proof (full_type_checker cts_pts_functor cts_prim_algos).
23/12/98, 14:29