In Coq's logic, is there a clear notion of the grammaticity of an expression with unification variables?

In the paper "Proof-term synthesis in dependent type systems via explicit substitution", Cesar Munoz gives a formal system for incremental construction of proof terms.

typed open terms are built incrementally at the same time as proofs are done. This way, every construction step, not just the last one, may be type checked. The method is based on a suitable calculus where substitutions as well as meta-variables are first-class objects

My question is, in Coq can we comfortably say that substitutions and/or meta-variables are first class objects? Does Coq's kernel contain anything like this?

I remember reading unification variables don't belong in Coq's kernel (which makes sense to me, because of trustworthiness arguments). Some kernel checks aren't even modular

Specifically, the fixpoint guard condition isn't modular, which would likely interfere with the goal described

As far as I know, Coq's kernel only handles completely solved metavariables, ie terms where there are no "goals left", exactly in order to be able to perform non-modular checks like guard checking. But there are still some weak form of meta-variables allowed there

It depends on exactly what you call the kernel.

On the one hand, there are functions defined on the kernel/ directory like the kernel reduction machine which can handle existential variables a little (eg kernel reduction by taking an optional closure which says how to unfold evars, treats them as neutrals when they don't unfold)

On the other hand the type checking and environment extension interface exposed in safe_typing does not accept evars (raises an exception if it encounters them)

Last updated: Oct 04 2023 at 21:01 UTC