Patrick Nicodemus (Apr 10 2023 at 19:25): Patrick Nicodemus (Apr 10 2023 at 19:25):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?
Paolo Giarrusso (Apr 10 2023 at 19:34):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
Paolo Giarrusso (Apr 10 2023 at 19:36):Specifically, the fixpoint guard condition isn't modular, which would likely interfere with the goal described
Meven Lennon-Bertrand (Apr 12 2023 at 14:39):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
Gaëtan Gilbert (Apr 12 2023 at 14:54):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 13 2024 at 01:02 UTC