Stream: MetaCoq

Topic: Proving typing of `<% ... %>`

Jason Gross (Oct 26 2022 at 12:30):

Suppose I want a proof that <% foo %> is well-typed (MetaCoq.Template.Typing.typing) for some expression foo. I'd like this proof to not depend on any axioms, to universally quantified over config.checker_flags insofar as this is possible, I'd like it to be universally quantified over the context, and I'd like it to be universally quantified over a Σ : global_env_ext subject to some reflectively-checkable constraint about what's present in the global env. Are there any tactics that can help me with this? Is there a fueled axiom-free typechecker for this?

Meven Lennon-Bertrand (Oct 26 2022 at 13:19):

I do not know for tactics, but no, there is no fueled type-checker. We thought about this a bit, but it seems hard to have a unique type-checker that we can use with either fuel and no axiom, or a normalization axiom. And implementing two type-checkers doing basically the same job but with different termination proofs looks like a lot of almost-duplication-but-not-quite, which sounds like a pain to write and maintain…

Meven Lennon-Bertrand (Oct 26 2022 at 13:20):

Basically, we are currently using the standard hack to use well-foundedness as fuel, by adding a large number of constructors on top of the axiom, so as to compute inside of Coq. But while this externally looks like fuel, internally you still rely on the normalization axiom.

Jason Gross (Oct 26 2022 at 13:29):

This should be good enough for tactics, at least; you can compute the typing and the axiom should become unused after reduction, right? (This only exists for PCUIC, though, right, not for Template AST?)

Meven Lennon-Bertrand (Oct 26 2022 at 13:31):

I guess so, yes

Meven Lennon-Bertrand (Oct 26 2022 at 13:31):

But indeed, this only exists for PCUIC, you have to translate back and forth to get Template stuff

Meven Lennon-Bertrand (Oct 26 2022 at 13:32):

(The relevant part is here)

Théo Winterhalter (Oct 26 2022 at 13:38):

Yes, if you reduce things, then the axioms disappear as well:

From Coq Require Import Utf8 Init.Wf.

Axiom (R : nat → nat → Prop).
Axiom (wf_R : well_founded R).
Axiom (prf : R 0 1).

Fixpoint helper (x : nat) (n : nat) : Acc R n :=
  match x with
  | 0 => wf_R n
  | S y => Acc_intro n (λ m h, helper y m)
  end.

Definition foo (n : nat) : nat :=
  Fix_F (λ n, nat) (λ n,
    match n with
    | 0 => λ r, 0
    | 1 => λ r, r 0 prf
    | S m => λ r, 1
    end
  ) (helper 100 n).

Definition foo_1 := foo 1.
Print Assumptions foo_1.

Definition reduced_foo_1 := Eval lazy in foo 1.
Print reduced_foo_1.
Print Assumptions reduced_foo_1.

Jason Gross (Oct 26 2022 at 16:48):

Can I get an example of how to prove something using the safechecker?
e.g., if I want to prove

From MetaCoq.Template Require Import All.
Require Import Coq.Lists.List.
Import ListNotations.

Open Scope bs.
Import MCMonadNotation.

Definition checker_flags_constraint : config.checker_flags -> bool := fun _ => true.
Definition global_env_ext_constraint : global_env_ext -> bool := fun _ => true.

Goal forall {cf : config.checker_flags} Σ Γ,
    checker_flags_constraint cf -> global_env_ext_constraint Σ ->
  Σ;;; Γ
  |- tConstruct
       {|
         inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "True");
         inductive_ind := 0
       |} 0 []
  : tInd
      {|
        inductive_mind := (MPfile ["Logic"; "Init"; "Coq"], "True");
        inductive_ind := 0
      |} []
.

How should I do that with the safechecker?

Théo Winterhalter (Oct 26 2022 at 17:04):

I would apply a lemma saying that the check function is sound—but I cannot find it—and then the proof would be hopefully lazy ; reflexivity or something.

Théo Winterhalter (Oct 26 2022 at 17:05):

Maybe it has to be extracted from there https://github.com/MetaCoq/metacoq/blob/coq-8.16/safechecker/theories/PCUICSafeChecker.v#L2504

Jason Gross (Nov 04 2022 at 13:07):

Is there a version of this that gives unsquashed typing derivations?

Meven Lennon-Bertrand (Nov 07 2022 at 14:22):

No, there is only the one version that should extract to code that does not manage proofs

Matthieu Sozeau (Nov 23 2022 at 12:53):

I think you can only unsquash by running the thing in Ltac or some other metaprogramming language

Jason Gross (Nov 23 2022 at 13:09):

That would be fine, but I can't actually get the normal form in reasonable time because of opacity or function types or something. What's the obstacle to writing an unsquasher in Gallina?

Matthieu Sozeau (Nov 24 2022 at 11:37):

Ah yes, that's tricky unfolding questions...

Yannick Forster (Nov 24 2022 at 12:36):

It's an easy task in t MetaCoq to unfold all opaque occurring constants recursively, using a recursive quote. Do you think that would help? You can then run the obtained term and get the result out of the squashing using ltac or MetaCoq again

Jason Gross (Nov 24 2022 at 18:49):

You're suggesting that I quote the safechecker, recursively perform cbv delta on everything that recursively uses Qed, then unquote the resulting term, and run that through the VM?

I'm concerned this is going to be a truly massive term that will take way too long to do anything with, not to mention that the normal form of the typing derivation is still going to be reduction-blocked in some cases by having witnesses of types like forall v, ...... Do you think it'll perform adequately?

Yannick Forster (Nov 24 2022 at 18:58):

I don't know anything about performance :) I see one other way though: Go through the safe checker with the TemplateMonad and recursively replace every opaque constant by a new, non-opaque one. That is going to take some time running, but in the end it is equivalent to going through everything manually and replacing Qed with Defined. And it can be done once and for all in a file TransparentSafeChecker

Last updated: Oct 13 2024 at 01:02 UTC