Stream: MetaCoq

Topic: SafeChecker invocation?


view this post on Zulip Jason Gross (Apr 24 2023 at 19:48):

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...

view this post on Zulip Jason Gross (Apr 24 2023 at 20:18):

I guess part of what I want is PCUICTypeChecker.check

view this post on Zulip Jason Gross (Apr 24 2023 at 21:24):

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.

view this post on Zulip Jason Gross (Apr 24 2023 at 21:24):

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

view this post on Zulip Matthieu Sozeau (Apr 25 2023 at 09:10):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:16):

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…

view this post on Zulip Matthieu Sozeau (Apr 25 2023 at 09:17):

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

view this post on Zulip Meven Lennon-Bertrand (Apr 25 2023 at 09:20):

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

view this post on Zulip Jason Gross (Apr 25 2023 at 23:09):

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.

view this post on Zulip Matthieu Sozeau (Apr 26 2023 at 07:07):

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.

view this post on Zulip Kenji Maillard (Apr 26 2023 at 08:28):

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)

view this post on Zulip Meven Lennon-Bertrand (Apr 26 2023 at 08:54):

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.

view this post on Zulip Meven Lennon-Bertrand (Apr 26 2023 at 08:58):

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.

view this post on Zulip Meven Lennon-Bertrand (Apr 26 2023 at 09:01):

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