The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

The reason why is looks weird is because you are misunderstanding what existential var instances are: they are not the context of the existential variable, but an explicit substitution which must be applied when the existential variable takes a value.

In your case, [rewrite aeqb] makes it so that every [a] in the [?9] of the conclusion must be replaced by [b]. Which is what happens. It may be confusing because both [a] and [b] are variable, but they need not be:

Goal forall a b:nat, a=2*b+a -> exists c:nat, c = c.
intros a b aeqb.
eexists. (*make an evar*)
match goal with |- ?V = ?V => remember V as e eqn:Q end. (*clone the evar*)
rewrite Q at 2. (*make the consequent and Q look really similar*)
rewrite aeqb. (* e = ?9 (* [2 * b + a, b, aeqb] *) *)
instantiate (1:=a). (* e=2*b+a *)

On 4 September 2014 03:19, Jonathan <jonikelee AT gmail.com> wrote:

When experimenting with the evars, using a recent trunk version of Coq, I noticed the following:

Set Printing Existential Instances. (*Or, if in CoqIde, use View->Display existential variable instances*)
Require Setoid.

Goal forall a b:nat, a=b -> exists c:nat, c = c.
intros a b aeqb.
eexists. (*make an evar*)
match goal with |- ?V = ?V => remember V as e eqn:Q end. (*clone the evar*)
rewrite Q at 2. (*make the consequent and Q look really similar*)
rewrite aeqb. (*rewrite works!  And the two evar contexts for the same "e" evar no longer match!*)
Fail exact Q. (*?*)
instantiate (1:=a) in Q. (*??*)


I don't know if this is a bug or a feature.  I guess it could be a feature, but then it points out something quite unexpected: that a single evar can have multiple different contexts, even within the same goal.  I was under the impression that all copies of the same evar shared the same single context.

If this is a bug - is the bug that "rewrite aeqb" does anything at all, or that it only rewrites one of the contexts?

If this is a feature:

Are all instances of an evar separable this way, or just some? Which ones?

What tactics other than rewrite can be used to modify a specific version of an evar's context without modifying the others?  How does one target the context with a tactic?

-- Jonathan