Why don't I have some sort of combinator that says "this type was constructed using `Inductive`

" or "this type was constructed using `CoInductive`

"?

In what language? Gallina or Ltac?

gallina

i'm guessing in ltac i just call `induction foo`

and if it fails it's not `Inductive`

haha

Well, that would break every nice property of CIC then.

In theory you can add such a type-case primitive

intriguing!

also, what?

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

yep

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)

The `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 [18]. 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: Jun 25 2024 at 19:01 UTC