Library variables

We define our variables exactly as that in Software Foundations . Basically, variables are wrappers around numbers. We could have defined them as wrappers around any (countably) infinite type with decidable equality.

Here are some examples of variables.

We need decidable equality on variables so that many useful relations on our future definitions of Terms, like equality, alpha equality, etc. will be decidable. Also our substitution function will need this decidable equality to decide whether it needs to come up with fresh variables. Decidable equality on variables is a straightforward consequence of decidable equality on the underlying type.

Another key requirement for a sensible formalization of variables is to have an unbounded supply of fresh variables. Hence, we prove the following lemma. To those who are unfamiliar with constructive logic, the following lemma might just say that that for any n and lv, there exists a list lvn of length n of distinct variables such that the members of lvn are disjoint from the members of lv. However, because of the propositions as types principle, We are actually defining a function fresh_vars that takes a number n and a list lv of variables and returns a 4-tuple. The first member of that tuple is lvn, a list of variables with the above mentioned properties. The next three members are proofs of the desired properties of lvn. An important use free_vars of it will be in defining the substitution function.