Library variables

Require Export list.

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.

Inductive NVar : Set :=
| nvar : natNVar.

Here are some examples of variables.

Definition nvarx := nvar 0.
Definition nvary := nvar 1.
Definition nvarz := nvar 2.

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.

Theorem eq_var_dec: x y : NVar, {x = y} + {x y}.

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.

Lemma fresh_vars :
   (n: nat) (lv : list NVar),
    {lvn : (list NVar) × no_repeats lvn × disjoint lvn lv × length lvn = n}.
  intros. (fresh_distinct_vars n lv).
  apply fresh_distinct_vars_spec.