Coq programming frequently asked question

• How do I obtain the type of term?
• How do I obtain the value associated to an identifier?
• How do I get rid of unbound de Bruijn indices?
• How do I obtain a type_judgement?

Answers

• How do I obtain the type of term? To type a term of the calculus of the construction, you need to use Mach.type_of. The arguments to provide to this function usually are Evd.mt_evd() and (initial_sign()), if all free identifiers in the term are declared in the global environment. If you have some free identifiers, for which you know the expected type, you can add them in the signature given by (intial_sign()), using Mach.fexecute_type to create a type_judgement and add_sign to add a binding in the signature.

  This does not work if there are "unbound" de Bruijn indices.

• How do I obtain the value associated to an identifier? Use Machops.global. The first argument should usually be gLOB (initial_sign()). Now if this identifier is itself a definition, getting the value is done by applying const_value. The first argument should usually be Evd.mt_evd().
• How do I get rid of unbound de Bruijn indices? When working on a term, you often need to pass as argument a signature that will contain bindings for named variables that appear in the term. When crossing a binder, you need to replace all instances of the de Bruijn indices corresponding to this binder with a named variable, which you add in the signature, with its type (under the form of a type judgement), using the function Names.add_sign
• How do I obtain a type_judgement? When you already know the type of the expression as a value of type constr (see for instance, how do I obtain the type of term?), you simply need to convert it to a type_judgement using Mach.fexecute_type.
keep the possibility to manipulate terms of the calculus of constructions, to build new ones and to type or convert the result, you need to make sure the terms that you manipulate never contain unbound de Bruijn indices. What you need to do is to substitute de Bruijn indices with named variables as you cross binders. When you cross a binder, you have access to the type of the bound variable, you can use Mach.fexecute_type to get a type judgement