The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Joachim,

> in my context, I can always undo the effect of [clear x] with [set x := e], 
> right?

theoretically yes. How practical this is depends on how much effort it is to 
construct the term "e". In Coq every proof is just a term with a given type. 
In many cases it is fairly non-trivial to come up with the term. This is what 
I meant with "trivial to construct". In case "e" is a simple term, fine. In 
case "e" is a rather complicated term, it is not a good idea to throw it away.

Let's dig into this a bit deeper. I would say (experts please correct me if I 
got it wrong) there are four kinds of variables in Coq:

<var> : <Type>  where <var> is parameter, that is a parameter or precondition 
of a Lemma or an introduced forall variable. These variables truly have no 
associated terms with them - all you do in the current context is under the 
assumption that you can find instances for these parameters some time later.

<var> := <instance> : <Type> where <instance> is a term, possibly depending 
on parameters, where Coq confirmed that the term for <instance> has type 
<Type>.

<var> : <Type> where <var> is NOT a parameter but also refers to some term 
exactly as in the second case, just that Coq doesn't show the term, because 
it is usually complicated and uninteresting. For this kind of variable it is 
usually just interesting that an instance of the type exists. It is not 
interesting how the term looks, because you are not going to manipulate it.

Evars which are written as ?name and are bound to a goal that you must supply 
a term (eventually just depending on parameters) of the type of the evar. 
Evars are similar to the 3rd kind, just that you don't know yet if you 
actually can construct a term with this type.

The first case are only direct parameters of the lemma (everything before the 
first : ) and everything which introduced with the intro tactic. Everything 
else which is shown as <var> : <Type> is actually of the third kind. This 
means that most of your <var> : <Type> things are very similar to the second 
kind.

It is true that everything of the 2nd and 3rd kind can be constructed from 
everything of the first kind (the parameters). So you are right, everything 
of the 2nd kind can always be thrown away and reconstructed from the 
parameters. I was wrong in my original mail that throwing away variables of 
the 2nd kind can influence the provability of the goal - It can't, at least 
not theoretically.

On the other hand this also applies to everything of the 3rd kind. What I am 
saying is that the distinction between the 2nd and 3rd kind is more a 
convenience feature - don't show long and uninteresting terms. I guess you 
wouldn't suggest to throw everything of the third kind away, because you 
usually put in quite some effort to construct these terms. The same can in 
many cases apply to terms of the second type. Using evars, especially when 
the type of the evar is itself an evar, is just one example, because the evar 
tactic produces a defined term. A more common example are instances of 
dependent types. Dependent types can mix computable values with propositions, 
so they usually are assigned to variables of 2nd kind but might need 
intricate proofs, so it is not a good idea to throw them away.

I don't think that you can find a practical distinction between variables of 
2nd or 3rd time which will justify to throw some away and others not. One 
could say keep things with dependent types, but then False is not a dependent 
type. Also use of evars is not a good criteria, because at some point the 
evars will be gone and you can't see from the term if was constructed using 
evars. What might be a reasonable criteria is the size of the term. My main 
point is that the distinction between 2nd and 1st/3rd kind is not a good 
criteria. Variables of 2nd kind be as complicate to construct as variables of 
3rd kind.

A question to the experts: is there a way to distinguish variables of 1st 
kind (parameters) and 3rd kind (derived terms with term not shown)?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928