Timings for PCUICSafeRetyping.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-metacoq-safechecker.dev//./safechecker/theories/PCUICSafeRetyping.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-metacoq-safechecker.dev//./safechecker/theories/PCUICSafeRetyping.v.timing
(* Distributed under the terms of the MIT license. *)
From Coq Require Import ssreflect ssrbool Utf8.
Require Import Equations.Prop.DepElim.
From Equations Require Import Equations.
From Coq Require Import Bool String List Program.
From MetaCoq.Utils Require Import utils monad_utils.
From MetaCoq.Common Require Import config uGraph.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICArities PCUICInduction
PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGlobalEnv
PCUICWeakeningEnv PCUICWeakeningEnvTyp
PCUICReduction
PCUICWeakeningConv PCUICWeakeningTyp
PCUICClosed PCUICClosedTyp
PCUICSafeLemmata PCUICSubstitution PCUICValidity
PCUICGeneration PCUICInversion PCUICValidity PCUICInductives PCUICInductiveInversion PCUICReduction
PCUICSpine PCUICSR PCUICCumulativity PCUICConversion PCUICConfluence PCUICArities
PCUICContexts PCUICContextConversion PCUICContextConversionTyp PCUICOnFreeVars
PCUICWellScopedCumulativity PCUICSafeLemmata PCUICSN PCUICConvCumInversion.
From MetaCoq.PCUIC Require Import BDTyping BDToPCUIC BDFromPCUIC BDUnique.
From MetaCoq.SafeChecker Require Import PCUICErrors PCUICSafeReduce PCUICWfEnv.
(** Allow reduction to run inside Coq *)
Transparent Acc_intro_generator.
Local Open Scope string_scope.
Import monad_utils.MCMonadNotation.
#[global]
Hint Constructors assumption_context : pcuic.
Derive NoConfusion for type_error.
Set Equations Transparent.
Add Search Blacklist "_graph_mut".
Add Search Blacklist "obligation".
Require Import ssreflect.
Lemma into_ws_cumul_pb_terms_Algo {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ l l'} :
All2 (convAlgo Σ Γ) l l' ->
is_closed_context Γ ->
forallb (is_open_term Γ) l ->
forallb (is_open_term Γ) l' ->
ws_cumul_pb_terms Σ Γ l l'.
now eapply into_ws_cumul_pb.
Lemma on_free_vars_ind_predicate_context {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {ind mdecl idecl} :
declared_inductive Σ ind mdecl idecl →
on_free_vars_ctx (closedP (context_assumptions (ind_params mdecl)) xpredT)
(ind_predicate_context ind mdecl idecl).
rewrite <- closedn_ctx_on_free_vars.
eapply closed_ind_predicate_context; tea.
eapply (declared_minductive_closed decli).
Inductive wellinferred {cf: checker_flags} Σ Γ t : Prop :=
| iswellinferred T : Σ ;;; Γ |- t ▹ T -> wellinferred Σ Γ t.
Definition well_sorted {cf:checker_flags} Σ Γ T :=
∥ ∑ u, Σ ;;; Γ |- T ▹□ u ∥.
Lemma well_sorted_wellinferred {cf:checker_flags} {Σ Γ T} :
well_sorted Σ Γ T -> wellinferred Σ Γ T.
Coercion well_sorted_wellinferred : well_sorted >-> wellinferred.
Lemma spine_subst_smash_inv {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ}
{Γ inst Δ s} :
wf_local Σ (Γ ,,, Δ) ->
spine_subst Σ Γ inst s (smash_context [] Δ) ->
∑ s', spine_subst Σ Γ inst s' Δ.
move/spine_subst_ctx_inst.
eapply ctx_inst_smash in c.
unshelve epose proof (ctx_inst_spine_subst _ c); auto.
(** Smashed variant that is easier to use *)
Lemma inductive_cumulative_indices_smash {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} :
forall {ind mdecl idecl u u' napp},
declared_inductive Σ ind mdecl idecl ->
on_udecl_prop Σ (ind_universes mdecl) ->
consistent_instance_ext Σ (ind_universes mdecl) u ->
consistent_instance_ext Σ (ind_universes mdecl) u' ->
PCUICEquality.cmp_ind_universes Σ ind napp u u' ->
forall Γ pars pars',
spine_subst Σ Γ pars (List.rev pars) (smash_context [] (subst_instance u (ind_params mdecl))) ->
spine_subst Σ Γ pars' (List.rev pars') (smash_context [] (subst_instance u' (ind_params mdecl))) ->
ws_cumul_pb_terms Σ Γ pars pars' ->
let indctx := idecl.(ind_indices)@[u] in
let indctx' := idecl.(ind_indices)@[u'] in
let pindctx := subst_context_let_expand (List.rev pars) (ind_params mdecl)@[u] (smash_context [] indctx) in
let pindctx' := subst_context_let_expand (List.rev pars') (ind_params mdecl)@[u'] (smash_context [] indctx') in
ws_cumul_ctx_pb_rel Cumul Σ Γ pindctx pindctx'.
intros ind mdecl idecl u u' napp isdecl up cu cu' hR Γ pars pars' sppars sppars' eq.
unshelve epose proof (spine_subst_smash_inv _ sppars) as [parsubst sppars2].
eapply weaken_wf_local; tea.
eapply (on_minductive_wf_params isdecl cu).
unshelve epose proof (spine_subst_smash_inv _ sppars') as [parsubst' sppars3].
eapply weaken_wf_local; tea.
eapply (on_minductive_wf_params isdecl cu').
epose proof (inductive_cumulative_indices isdecl cu cu' hR Γ pars pars' _ _ sppars2 sppars3 eq).
rewrite (spine_subst_inst_subst sppars2) in X.
rewrite (spine_subst_inst_subst sppars3) in X.
rewrite /pindctx /pindctx'.
rewrite - !smash_context_subst_context_let_expand.
(** * Retyping
The [infer] function provides a fast (and loose) type inference
function which assumes that the provided term is already well-typed in
the given context and recomputes its type. Only reduction (for
head-reducing types to uncover dependent products or inductives) and
substitution are costly here. No universe checking or conversion is done
in particular. *)
Context {cf : checker_flags} {nor : normalizing_flags}.
Context (X_type : abstract_env_impl).
Context (X : X_type.π2.π1).
Context {normalization_in : forall Σ, wf_ext Σ -> Σ ∼_ext X -> NormalizationIn Σ}.
Local Definition heΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
∥ wf_ext Σ ∥ := abstract_env_ext_wf _ wfΣ.
Local Definition hΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
∥ wf Σ ∥ := abstract_env_ext_sq_wf _ _ _ wfΣ.
Ltac specialize_Σ wfΣ :=
repeat match goal with | h : _ |- _ => specialize (h _ wfΣ) end.
Definition on_subterm P Pty Γ t : Type :=
match t with
| tProd na t b => Pty Γ t * Pty (Γ ,, vass na t) b
| tLetIn na d t t' =>
Pty Γ t * P Γ d * P (Γ ,, vdef na d t) t'
| tLambda na t b => Pty Γ t * P (Γ ,, vass na t) b
| _ => True
end.
Lemma welltyped_subterm {Σ Γ t} :
wellinferred Σ Γ t -> on_subterm (wellinferred Σ) (well_sorted Σ) Γ t.
destruct t; simpl; auto; intros [T HT]; sq.
apply unlift_TypUniv in X0.
split; now do 2 econstructor.
destruct X0 as (_ & ? & ? & _); cbn in *.
split; econstructor ; [econstructor|..]; eassumption.
destruct X0 as (X0' & ? & ? & _); cbn in *.
split; [split|]; econstructor ; [econstructor|..]; eassumption.
#[local] Notation ret t := (t; _).
#[local] Definition principal_type Γ t :=
∑ T : term, forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ |- t ▹ T ∥.
#[local] Definition principal_sort Γ T :=
∑ u, forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ |- T ▹□ u ∥.
#[local] Definition principal_type_type {Γ t} (wt : principal_type Γ t) : term
:= projT1 wt.
#[local] Definition principal_sort_sort {Γ T} (ps : principal_sort Γ T) : sort
:= projT1 ps.
#[local] Coercion principal_type_type : principal_type >-> term.
#[local] Coercion principal_sort_sort : principal_sort >-> sort.
Program Definition infer_as_sort {Γ T}
(wfΓ : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ wf_local Σ Γ ∥)
(wf : forall Σ (wfΣ : abstract_env_ext_rel X Σ), well_sorted Σ Γ T)
(tx : principal_type Γ T) : principal_sort Γ T :=
match @reduce_to_sort cf nor _ X _ Γ tx _ with
| Checked_comp (u;_) => (u;_)
| TypeError_comp e _ => !
end.
destruct (wf _ wfΣ) as [[]], (hΣ _ wfΣ) as [wΣ].
eapply infering_typing, validity in s as (_ & s & Hs & _); eauto.
pose proof (s Σ wfΣ) as s'.
now eapply closed_red_red.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
pose proof (s Σ wfΣ) as s'.
destruct wf as [[? i]], (hΣ _ wfΣ) as [wΣ].
eapply infering_sort_infering in i ; eauto.
erewrite(abstract_env_ext_irr _ _ wfΣ); eauto.
Program Definition infer_as_prod Γ T
(wfΓ : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ wf_local Σ Γ ∥)
(wf : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ T)
(isprod : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ ∑ na A B, red Σ Γ T (tProd na A B) ∥) :
∑ na' A' B', forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ ⊢ T ⇝ tProd na' A' B' ∥ :=
match @reduce_to_prod cf nor _ X _ Γ T wf with
| Checked_comp p => p
| TypeError_comp e _ => !
end.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct isprod as (?&?&?&?).
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
eapply into_closed_red ; tea.
now eapply subject_is_open_term.
Equations lookup_ind_decl ind : typing_result
(∑ decl body, forall Σ (wfΣ : abstract_env_ext_rel X Σ), declared_inductive (fst Σ) ind decl body) :=
lookup_ind_decl ind with inspect (abstract_env_lookup X ind.(inductive_mind)) :=
{ | exist (Some (InductiveDecl decl)) look with inspect (nth_error decl.(ind_bodies) ind.(inductive_ind)) :=
{ | exist (Some body) eqnth => Checked (decl; body; _);
| exist None _ => raise (UndeclaredInductive ind) };
| _ => raise (UndeclaredInductive ind) }.
eapply declared_minductive_from_gen.
erewrite (abstract_env_lookup_correct' X); eauto.
Lemma lookup_ind_decl_complete Σ (wfΣ : abstract_env_ext_rel X Σ) ind e : lookup_ind_decl ind = TypeError e ->
((∑ mdecl idecl, declared_inductive Σ ind mdecl idecl) -> False).
pose proof (abstract_env_ext_wf _ wfΣ) as [[? ?]].
apply_funelim (lookup_ind_decl ind).
1-2: intros * _ her [mdecl [idecl [declm decli]]];
unshelve eapply declared_minductive_to_gen in declm; eauto;
red in declm;
erewrite <- abstract_env_lookup_correct', declm in e0; eauto;
congruence.
1-2:intros * _ _ => // => _ [mdecl [idecl [declm /= decli]]].
unshelve eapply declared_minductive_to_gen in declm; eauto;
red in declm.
erewrite <- abstract_env_lookup_correct', declm in look; eauto.
Obligation Tactic := intros ;
try match goal with
| infer : context [wellinferred _ _ _ -> principal_type _ _ ],
wt : wellinferred _ _ _ |- _ =>
try clear infer ; destruct wt as [T HT]
end.
Equations infer (Γ : context) (wfΓ : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ wf_local Σ Γ ∥) (t : term)
(wt : forall Σ (wfΣ : abstract_env_ext_rel X Σ), wellinferred Σ Γ t) :
principal_type Γ t
by struct t :=
infer Γ wfΓ (tRel n) wt with
inspect (option_map (lift0 (S n) ∘ decl_type) (nth_error Γ n)) :=
{ | exist None _ => !
| exist (Some t) _ => ret t };
infer Γ wfΓ (tVar n) wt := !;
infer Γ wfΓ (tEvar ev args) wt := !;
infer Γ wfΓ (tSort s) wt := ret (tSort (Sort.super s));
infer Γ wfΓ (tProd n ty b) wt :=
let wfΓ' : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ wf_local Σ (Γ ,, vass n ty) ∥ := _ in
let ty1 := infer Γ wfΓ ty (fun a b => (welltyped_subterm (wt a b)).1) in
let s1 := infer_as_sort wfΓ (fun a b => (welltyped_subterm (wt a b)).1) ty1 in
let ty2 := infer (Γ ,, vass n ty) wfΓ' b (fun a b => (welltyped_subterm (wt a b)).2) in
let s2 := infer_as_sort wfΓ' (fun a b => (welltyped_subterm (wt a b)).2) ty2 in
ret (tSort (Sort.sort_of_product s1 s2));
infer Γ wfΓ (tLambda n t b) wt :=
let t2 := infer (Γ ,, vass n t) _ b (fun a b => (welltyped_subterm (wt a b)).2) in
ret (tProd n t t2);
infer Γ wfΓ (tLetIn n b b_ty b') wt :=
let b'_ty := infer (Γ ,, vdef n b b_ty) _ b' (fun a b => (welltyped_subterm (wt a b)).2) in
ret (tLetIn n b b_ty b'_ty);
infer Γ wfΓ (tApp t a) wt :=
let ty := infer Γ wfΓ t _ in
let pi := infer_as_prod Γ ty wfΓ _ _ in
ret (subst10 a pi.π2.π2.π1);
infer Γ wfΓ (tConst cst u) wt with inspect (abstract_env_lookup X cst) :=
{ | exist (Some (ConstantDecl d)) _ := ret (subst_instance u d.(cst_type))
| _ := ! };
infer Γ wfΓ (tInd ind u) wt with inspect (lookup_ind_decl ind) :=
{ | exist (Checked decl) _ := ret (subst_instance u decl.π2.π1.(ind_type))
| exist (TypeError e) _ := ! };
infer Γ wfΓ (tConstruct ind k u) wt with inspect (lookup_ind_decl ind) :=
{ | exist (Checked decl) _ with inspect (nth_error decl.π2.π1.(ind_ctors) k) :=
{ | exist (Some cdecl) _ => ret (type_of_constructor decl.π1 cdecl (ind, k) u)
| exist None _ => ! }
| exist (TypeError e) _ => ! };
infer Γ wfΓ (tCase ci p c brs) wt
with inspect (reduce_to_ind Γ (infer Γ wfΓ c _) _) :=
{ | exist (Checked_comp indargs) _ =>
let ptm := it_mkLambda_or_LetIn (inst_case_predicate_context p) p.(preturn) in
ret (mkApps ptm (List.skipn ci.(ci_npar) indargs.π2.π2.π1 ++ [c]));
| exist (TypeError_comp _ _) _ => ! };
infer Γ wfΓ (tProj p c) wt with inspect (@lookup_ind_decl p.(proj_ind)) :=
{ | exist (Checked d) _ with inspect (nth_error d.π2.π1.(ind_projs) p.(proj_arg)) :=
{ | exist (Some pdecl) _ with inspect (reduce_to_ind Γ (infer Γ wfΓ c _) _) :=
{ | exist (Checked_comp indargs) _ =>
let ty := pdecl.(proj_type) in
ret (subst0 (c :: List.rev (indargs.π2.π2.π1)) (subst_instance indargs.π2.π1 ty))
| exist (TypeError_comp _ _) _ => ! }
| exist None _ => ! }
| exist (TypeError e) _ => ! };
infer Γ wfΓ (tFix mfix n) wt with inspect (nth_error mfix n) :=
{ | exist (Some f) _ => ret f.(dtype)
| exist None _ => ! };
infer Γ wfΓ (tCoFix mfix n) wt with inspect (nth_error mfix n) :=
{ | exist (Some f) _ => ret f.(dtype)
| exist None _ => ! };
infer Γ wfΓ (tPrim p) wt with inspect (abstract_primitive_constant X p.π1) :=
{ | exist (Some prim_ty) eqp => ret (prim_type p prim_ty)
| exist None _ => ! }.
destruct (nth_error Γ n) eqn:hnth => //.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
now eapply isTypebd_isType in X1.
now eapply lift_sorting_lift_typing.
now eapply lift_sorting_lift_typing.
cbn; intros; case b'_ty as [].
apply wat_welltyped ; tea.
eapply validity, infering_typing ; eauto.
eapply infering_prod_infering in X1 as (?&?&[]); eauto.
now apply closed_red_red.
apply infering_prod_typing, validity, isType_tProd in tyt as [] ; eauto.
eapply infering_prod_prod in X1 as (?&?&[]).
2: now apply closed_red_red.
1: now apply closed_red_red.
eapply ws_cumul_pb_forget_cumul.
eapply into_ws_cumul_pb ; tea.
now eapply type_is_open_term, infering_typing.
1: now eapply red_ws_cumul_pb.
now eapply red_ws_cumul_pb_inv.
erewrite <- abstract_env_lookup_correct' in e; eauto.
unshelve eapply declared_constant_to_gen in isdecl; eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
erewrite <- abstract_env_lookup_correct' in e; eauto.
unshelve eapply declared_constant_to_gen in isdecl; eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
erewrite <- abstract_env_lookup_correct' in e; eauto.
unshelve eapply declared_constant_to_gen in isdecl; eauto.
destruct decl as (?&?&isdecl').
unshelve eapply declared_inductive_to_gen in isdecl, isdecl'; eauto.
eapply declared_inductive_inj in isdecl' as [].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
eapply lookup_ind_decl_complete.
destruct decl as (?&?&isdecl').
unshelve eapply declared_constructor_to_gen in isdecl; eauto.
pose proof (isdecl'_ := isdecl').
unshelve eapply declared_inductive_to_gen in isdecl'; eauto.
eapply declared_constructor_inj in isdecl as (?&[]).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct decl as (?&?&isdecl').
unshelve eapply declared_constructor_to_gen in isdecl; eauto.
pose proof (isdecl'_ := isdecl').
unshelve eapply declared_inductive_to_gen in isdecl'; eauto.
destruct isdecl as [isdecl]; cbn -[lookup_ind_decl] in *.
eapply declared_inductive_inj in isdecl' as [].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
eapply lookup_ind_decl_complete.
eapply infering_typing, validity in s as (_ & ? & ? & _) ; eauto.
set (H := λ (Σ0 : global_env_ext) (wfΣ0 : abstract_env_ext_rel X Σ0),
infer_obligations_obligation_24 Γ ci p c brs wt Σ0
wfΣ0) in indargs.
set (infer _ wfΓ c H) in *.
destruct indargs as (?&?&?&?).
pose proof wt; pose proof wfΓ
; pose proof s as s'.
eapply infering_ind_ind in inf as [? []].
2: now econstructor ; tea; eapply closed_red_red.
erewrite <- PCUICCasesContexts.inst_case_predicate_context_eq ; tea.
now apply closed_red_red.
replace #|x1| with #|args| ; tea.
all: eapply All2_length ; eassumption.
2:intros; now eapply ws_cumul_pb_forget_conv.
1: now eapply red_terms_ws_cumul_pb_terms.
1: now eapply red_terms_ws_cumul_pb_terms.
eapply PCUICConvCumInversion.alt_into_ws_cumul_pb_terms ; tea.
eapply infering_ind_typing, validity, isType_open in X1 ; auto.
rewrite on_free_vars_mkApps in X1.
move: X1 => /andP [] _ /forallb_All ?.
now eapply All_forallb, All_firstn.
apply infering_typing, subject_is_open_term in X0 ; auto.
move: X0 => /= /andP [] //.
set (H := λ (Σ : global_env_ext) (wfΣ : abstract_env_ext_rel X Σ),
infer_obligations_obligation_24 Γ ci p c brs wt Σ wfΣ) in a0.
set (infer _ wfΓ c H) in *.
pose proof wt; pose proof wfΓ.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
eapply infering_ind_infering in i as [? []] ; eauto.
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
pose proof s as s'; pose proof wfΓ as wfΓ'.
eapply infering_typing, validity in s' as (_ & ? & ? & _); eauto.
set (H := λ (Σ0 : global_env_ext) (wfΣ0 : abstract_env_ext_rel X Σ0),
infer_obligations_obligation_28 Γ p c wt Σ0 wfΣ0) in indargs.
set (infer _ wfΓ c H) in *.
destruct indargs as (?&?&?&?).
destruct d as (?&?&isdecl).
cbn -[lookup_ind_decl] in *.
pose proof wt; pose proof wfΓ
; pose proof s as s'.
destruct H3 as [[isdecl' ] []].
unshelve eapply declared_inductive_to_gen in isdecl, isdecl'; eauto.
eapply declared_inductive_inj in isdecl' as [].
eapply infering_ind_ind in X1 as [? []].
2: now econstructor ; tea ; apply closed_red_red.
eapply declared_inductive_from_gen; eauto.
now apply closed_red_red.
2: symmetry; eapply All2_length ; eassumption.
set (H := (λ (Σ0 : global_env_ext)
(wfΣ0 : abstract_env_ext_rel X Σ0),
infer_obligations_obligation_28 Γ p c wt Σ0 wfΣ0)) in a0.
set (infer _ wfΓ c H) in *.
cbn -[lookup_ind_decl] in *.
pose proof wt; pose proof wfΓ.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
eapply infering_ind_infering in s as [? []] ; eauto.
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
destruct d as (?&?&isdecl).
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
cbn -[lookup_ind_decl nth_error] in *.
unshelve eapply declared_inductive_to_gen in isdecl, H1; eauto.
eapply declared_inductive_inj in isdecl as [].
cbn -[lookup_ind_decl] in *.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
eapply lookup_ind_decl_complete ; eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
intros; erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
intros; erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
rewrite (abstract_primitive_constant_correct _ _ Σ) // in eqp.
intros; erewrite (abstract_env_ext_irr _ wfΣ0 wfΣ); eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
rewrite (abstract_primitive_constant_correct _ _ Σ) // in e.
Definition type_of Γ wfΓ t wt : term := (infer Γ wfΓ t wt).
Definition principal_typing Σ Γ t P :=
forall T, Σ ;;; Γ |- t : T -> Σ ;;; Γ ⊢ P ≤ T.
Program Definition type_of_typing Γ t (wt : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t) : ∑ T, forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ (Σ ;;; Γ |- t : T) × principal_typing Σ Γ t T ∥ :=
let it := infer Γ _ t _ in
(it.π1; _).
eapply BDFromPCUIC.typing_infering in Ht as [T' [inf _]].
destruct (hΣ _ wfΣ) as [wΣ].
destruct infer as []; cbn.
destruct wt' as [T' HT'].
eapply BDToPCUIC.infering_typing in s; pcuic.
apply typing_infering in HT'' as [P [HP HP']].
eapply infering_checking;tea.
now eapply ws_cumul_pb_forget in HP'.
Lemma squash_isType_welltyped :
forall {Σ : global_env_ext} {Γ : context} {T : term},
∥ isType Σ Γ T ∥ -> welltyped Σ Γ T.
now eapply isType_welltyped.
Equations? sort_of_type (Γ : context) (t : PCUICAst.term)
(wt : forall Σ : global_env_ext, abstract_env_ext_rel X Σ -> ∥ isType Σ Γ t ∥) :
(∑ u : sort, forall Σ : global_env_ext, abstract_env_ext_rel X Σ ->
∥ Σ ;;; Γ |- t : tSort u ∥) :=
sort_of_type Γ t wt with (@type_of_typing Γ t _) :=
{ | T with inspect (reduce_to_sort (X:=X) Γ T.π1 _) :=
{ | exist (Checked_comp (u; Hu)) hr => (u; _)
| exist (TypeError_comp _ _) ns => False_rect _ _ } }.
eapply squash_isType_welltyped, wt; eauto.
specialize (wt _ wfΣ) as [wt].
destruct (HT _ wfΣ) as [[Ht _]].
pose proof (abstract_env_ext_wf _ wfΣ) as [wf].
now eapply isType_welltyped.
pose proof (abstract_env_ext_wf _ H) as [wf].
specialize (Hu _ H) as [Hred].
destruct (HT _ H) as [[Ht _]].
eapply type_reduction_closed; tea.
epose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
epose proof (abstract_env_ext_wf X wfΣ) as [hwfΣ].
pose proof (reduce_to_sort_complete _ wfΣ _ _ ns).
destruct (HT _ wfΣ) as [[hty hp]].
destruct wt as [(_ & s & Hs & _)].
eapply ws_cumul_pb_Sort_r_inv in hp as [s' [hs' _]].
Transparent type_of_typing.
Definition map_typing_result {A B} (f : A -> B) (e : typing_result A) : typing_result B :=
match e with
| Checked a => Checked (f a)
| TypeError e => TypeError e
end.
Arguments iswelltyped {cf Σ Γ t A}.
Equations? type_of_subtype {Γ t T} (wt : forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ |- t : T ∥) :
forall Σ (wfΣ : abstract_env_ext_rel X Σ), ∥ Σ ;;; Γ ⊢ type_of Γ _ t _ ≤ T ∥ :=
type_of_subtype wt := _.
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
now exact (typing_wf_local wt').
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
case (hΣ _ wfΣ) as [hΣ'].
apply typing_infering in wt'.
destruct infer as [P HP].
eapply infering_checking ; eauto.
now eapply typing_wf_local.
now eapply type_is_open_term.
now eapply typing_checking.
(* Note the careful use of squashing here: the principal type is accessible
computationally but the proof it is principal is squashed (in Prop).
The [PCUICPrincipality.principal_type] proof gives an unsquashed version of the same theorem. *)
Theorem principal_types {Γ t} (wt : forall Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t) :
∑ P, ∥ forall T Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ |- t : T -> (Σ ;;; Γ |- t : P) * (Σ ;;; Γ ⊢ P ≤ T) ∥.
Proof using nor normalization_in.
unshelve eexists (infer Γ _ t _); intros.
now eapply typing_wf_local.
destruct (wt _ wfΣ) as [? wt'].
eapply typing_infering in wt' as [? []].
set (H := (λ (Σ0 : global_env_ext) (wfΣ0 : abstract_env_ext_rel X Σ0),
match hΣ Σ0 wfΣ0 with
| sq H =>
match wt Σ0 wfΣ0 with
| @iswelltyped _ _ _ _ A H0 =>
let (x, p) := typing_infering H0 in
let (a, _) := p in iswellinferred Σ0 Γ t x a
end
end)).
set (H' := (fun (Σ : _)
(wfΣ : _ X Σ)
=> match
wt Σ wfΣ
with
| @iswelltyped _ _ _ _ A x =>
match
hΣ Σ wfΣ
with
| sq _ =>
@sq (All_local_env (lift_typing (@typing cf) Σ) Γ)
(@typing_wf_local cf Σ Γ t A x)
end
end)).
destruct p as [T i]; eauto.
destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
apply infering_typing ; eauto.
now eapply typing_wf_local.
eapply infering_checking ; eauto.
now eapply typing_wf_local.
now eapply type_is_open_term.
now eapply typing_checking.