What am I supposed to call if I want to get `option ∥ wf_ext Σ × wf_local Σ Γ × (Σ ;;; Γ |- t : T) ∥`

? (for non-nil `Γ`

)

I see `PCUICSafeChecker.typecheck_program`

gives

```
EnvCheck_X_env_ext_type X_impl
(∑ A : term,
{X : X_env_ext_type X_impl
| ∥ PCUICWfEnv.abstract_env_ext_rel X (p.1, φ)
× wf_ext (p.1, φ) × BDTyping.infering (p.1, φ) [] p.2 A ∥})
```

which is almost what I want, but it produces the type rather than consuming/checking it, and it only works on an empty context, and it gives `BDTyping.infering`

instead of `typing`

...

I guess part of what I want is `PCUICTypeChecker.check`

This seems to work

```
Definition quotation_check (cf : config.checker_flags) (Σ : global_env_ext) (Γ : context) (t T : term) : option quotation_check_error.
Proof.
destruct (dec_normalizing cf); [ | exact (Some (QConfigNotNormalizing cf)) ].
simple refine (let cwf := @check_wf_ext cf _ optimized_abstract_env_impl Σ _ in
match cwf with
| CorrectDecl (exist A pf)
=> let wfΣ := abstract_env_ext_wf (abstract_env_prop:=optimized_abstract_env_prop) _ pf in
let X := @build_wf_env_ext cf _ Σ wfΣ in
let cwfΓ := @check_wf_local cf _ optimized_abstract_env_impl X _ Γ in
match cwfΓ with
| Checked wfΓ
=> let c := typing_error_forget (@check cf _ optimized_abstract_env_impl X _ Γ wfΓ t T) in
match c with
| Checked _ => None
| TypeError t => Some (QTypeError t)
end
| TypeError t => Some (QContextTypeError t)
end
| EnvError st err
=> Some (QEnvError (*st*) err)
end).
Defined.
Lemma quotation_check_valid {cf Σ Γ t T} : quotation_check cf Σ Γ t T = None -> @wf_ext cf Σ * wf_local Σ Γ * @typing cf Σ Γ t T.
Proof.
cbv [quotation_check].
repeat destruct ?; subst;
lazymatch goal with
| [ |- None = None -> _ ] => intros _
| [ |- Some _ = None -> _ ] => congruence
end.
match goal with
| [ |- ?P ] => cut (∥ @wf_ext cf Σ * wf_local Σ Γ * @typing cf Σ Γ t T ∥)
end.
{ todo "Find a way to get the safechecker to produce unsquashed judgments". }
lazymatch goal with
| [ H : _ = CorrectDecl _ (exist _ ?pf) |- _ ]
=> pose proof (abstract_env_ext_wf (abstract_env_prop:=optimized_abstract_env_prop) _ pf)
end.
repeat match goal with
| [ H : _ |- _ ] => unique pose proof (H _ eq_refl)
end.
sq; auto.
Qed.
```

Would it be worth sticking most of this definition somewhere in the safechecker proper?

Yes, sounds like the API is not giving you what you want although it could

I guess there is part of a general question on whether we use `typing`

or `infering`

. Using `infering`

rather than `typing`

is more precise, because it means the type is not just any type but a most general one. Also, using `infering`

in the core functions `infer`

/`retyping`

makes the proof obligations much saner. But in principle we could provide "degraded" versions that use `typing`

, so that it is easier to interface the return of the functions with the rest of the library…

We should have both indeed, with wrappers to define the less precise versions

Although in proofs I got used to do things like `intros * ?%infering_typing`

in the logrel development, to go from one version of typing to another on the fly. It's not perfect, but at least in proof mode it is bearable. Although it would probably be nicer to be as consistent as possible to avoid this yoga when possible

I think fundamentally what I need is an invocation of the safechecker that interfaces well with `PCUICSubstitution.substitution`

The variant I'm using is

```
Lemma closed_substitution {cf : config.checker_flags} {Σ : global_env_ext}
(s : list term)
(Γ' : list term)
(t T : term)
(wfΣ : wf Σ)
(Hs : All2_fold (fun s0 Γ'0 t T => Σ ;;; [] |- t : subst0 s0 T) s Γ')
(Γ'' := List.map (fun ty => {| BasicAst.decl_name := {| binder_name := nAnon; binder_relevance := Relevant |} ; BasicAst.decl_body := None ; BasicAst.decl_type := ty |}) Γ')
(Ht : Σ ;;; Γ'' |- t : T)
: Σ ;;; [] |- subst0 s t : subst0 s T.
Proof.
```

Is this true if I use `infering`

rather than `typing? (Is it proven somewhere?)

The way I'm using the safechecker is that I process a `typing`

goal so that it is closed in the global context, moving Gallina-level context variables and global constants to live in the local context of the term, and then use the safechecker to discharge the `Ht`

premise.

I don't think infering is closed under substitution by typeable terms, because you might have the typing of a variable being replaced by a checkeable term. I guess it's closed under substitution by inferable terms.

Isn't that actually the big theorem for bidirectional typing ? That if `t`

infers a type `T`

in context `Γ`

and `s : Γ' -> Γ`

is a well typed substitution then `t[s]`

still infer a type `T'`

that might be more precise than `T[s]`

(wrt cumulativity)

You are both right: in general it is only easy to show that bidirectional typing is stable by substituting variables with terms that *infer* the same types. In our setting where every typable term infers, you can still show stability by substitution with terms that only checks, but it's much less trivial (I guess it relies on confluence/injectivity of type constructors, transitivity and stability by substitution of conversion). I don't think we show directly the theorem Kenji mentions, but once we have established the back and forth implications between inference and typing, it should be an easy corollary of stability of typing by substitution.

And so I guess that a correct theorem would be

```
Lemma closed_substitution_bidir {cf : config.checker_flags} {Σ : global_env_ext}
(s : list term)
(Γ' : list term)
(t T : term)
(wfΣ : wf Σ)
(Hs : All2_fold (fun s0 Γ'0 t T => Σ ;;; [] |- t ◃ subst0 s0 T) s Γ')
(Γ'' := List.map (fun ty => {| BasicAst.decl_name := {| binder_name := nAnon; binder_relevance := Relevant |} ; BasicAst.decl_body := None ; BasicAst.decl_type := ty |}) Γ')
(Ht : Σ ;;; Γ'' |- t ▹ T)
: Σ ;;; [] |- subst0 s t ◃ subst0 s T.
```

Which you should be able to show from the one on typing by using `infering_typing`

, `checking_typing`

and `typing_checking`

. You can get a conclusion that uses `infering`

instead of `checking`

too by using `typing_infering`

instead of `typing_checking`

.

Last updated: Jul 23 2024 at 20:01 UTC