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?

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…

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.

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?)

I guess so, yes

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

(The relevant part is here)

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

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?

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.

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

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

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

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

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?

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

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

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?

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: Jun 20 2024 at 12:02 UTC