Why don't I have some sort of combinator that says "this type was constructed using
Inductive" or "this type was constructed using
In what language? Gallina or Ltac?
i'm guessing in ltac i just call
induction foo and if it fails it's not
Well, that would break every nice property of CIC then.
In theory you can add such a type-case primitive
(it's implementable as a syntactic model using induction recursion)
but then you get a language that behaves like Python and lots of stuff become dead wrong
there was a thread on Coq-club mildly related to that a few days ago
with such a combinator it becomes trivial to break e.g. univalence
since Inductive Box (A : Type) := box : A -> Box A is not equivalent to A anymore
so, in a nutshell: yes you can, but you probably don't want that
coq-club is the email list?
list of all resources like mailing lists and forums: https://github.com/coq-community/awesome-coq#community
https://sympa.inria.fr/sympa/arc/coq-club/2021-11/msg00003.html for the thread
(the original question was about an axiom that makes equality of types commute with forall in the wrong direction)
Note that we perform an additional check if v 2 is a constructor of an inductive type (possibly applied to some arguments)
ConCert paper keeps suggesting to me that I am allowed to infer if a type was built using
Inductive. Is there some MetaCoq facility that's throwing me off?
This kind of analysis is indeed conceptually possible in metaprogramming — the “no” above was restricted to _normal_ programming (Gallina).
and the paragraph with your quote appears to talk about an interpreter* — and interpreters are metaprograms for the language they are interpreting.
*It starts with:
The outline of the most interesting parts of our interpreter is given in Figure 2. Specifically, we show the evaluation of fixpoints and case-expressions.
and it’s not even an interpreter for Coq, but for another language, embedded into Coq:
As an instance of our approach, we develop an embedding of the “core” of the Acorn smart contract language into Coq. We call this core language λsmart. This language contains all the essential features of a realistic functional language: System F type system, inductive types,
I haven’t read much of the rest, but this much can be explained as follows: one can “embed an object language” (here lambda_smart) into another one (here Coq) — that is, define a type of ASTs, and functions that manipulate the AST.
The semantics of λsmart is given as a definitional interpreter . This gives us an executable semantics for the language. Moreover, since the core language we consider is sufficiently close to Acorn, our interpreter can serve as a reference interpreter. The interpreter is implemented in an environment-passing style and works both with named and nameless representations of variables.
In this case, the inductive types of lambda_smart are presumably separate from the inductive types of Coq… and that’s why a Gallina program _can_ inspect them: if you embed lambda_smart in Coq, Gallina then can play the role of a metaprogramming language for lambda_smart programs.
Last updated: Sep 23 2023 at 08:01 UTC