CODEWITHSUNDEEP
coqfree-variable
Khan
Khan

Reputation: 303

Free variables in Coq

Is there any function/command to get/check if a free variable, lets say n:U, exists in a term/expression e, using Coq? Please share.

For example, I want to state this "n does not occur in the free names of e" in Coq.

Thanks,

Wilayat

Upvotes: 1

Views: 1134

Answers (1)

Francois G
Francois G

Reputation: 11985

Let's assume you're talking about free variables in Coq terms:

Dealing with an elementary Coq proof (using nothing exterior), what you manipulate is, outside of the proof context, a closed term, i.e. a term with only bound variables. If in proof mode a term ein your goal appears to have a free variable n(meaning the variable n is somewhere in your proof context), you can simply make the binding explicit (and close the goal term) using the generalize tactic.

In more advanced cases, your less-vanilla proof may involve free variables in the form of assumptions or parameters, in which case you can list them using Print Assumptions.

If on the other hand you are talking about using Coq terms to represent the notion of term in a particular language (e.g. you are formalizing such a language), you simply have to give a special treatment to the free variables of your language.

Provided you give them a specific constructor in the inductive definition of your language's terms, it should be easy to state whether some term has free variables or not. If you're unfamiliar with the (not so trivial) notion of representing substitution & the free variables of a language, you'll find pointers at increasing levels of precision from the TAPL to B.C.Pierce's SF course to the results of the POPLMark Challenge.

Upvotes: 2

Related Questions