The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/04/2014 09:20 AM, Arnaud Spiwack wrote:
> 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 *)

That is very illuminating!  I completely misunderstood those lists. But, 
how does one know, for each substitution in an evar instance list, what 
is being substituted for?  Would it be more helpful if each such 
substitution was shown as a pair?

Note that the order of hypotheses in the focused goal can't be used to 
determine what is being substituted for, because of cases like:

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*)
set (d:=0).
move d at top.

where the order of hypotheses is now d, a, b, aeqb but the evar 
instances are [a, b, aeqb].

OH - that's something that evar dependent subgoals provide!  Now this is 
making more sense:

Goal forall a b:nat, a=2*b+a -> exists c:nat, c = c.
intros a b aeqb.
refine (ex_intro _ _ _); shelve_unifiable.
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*)
Unshelve.
(*watch the context lists while doing:*)
2:set (d:=0).
2:move d at top.

So, an evar instance list, as displayed by Set Printing Existential 
Instances, is an instance-of-that-evar-specific list of substitutions 
applied to the similarly-ordered hypotheses in the evar's matching 
subgoal.  Modifying the order of hypotheses in the evar's matching 
subgoal similarly modifies the order in all of its instance lists.  But, 
each substitution can be modified independently (using rewrite).  When 
the evar is instantiated, the substitutions occur independently at each 
instance location.  The context of the evar is the evar's dependent 
subgoal - implying that when the evar is instantiated with a term, that 
term is interpreted within the evar's subgoal, and not within the 
subgoal where the instantiation took place (the substitutions are 
interpreted there).

Each evar acts like a function.  The evar's dependent subgoal is that 
function's signature (hypotheses are formal parameters, consequent is 
result type).  The term (eventually) used to instantiate the evar 
becomes that function's "body".  The instance lists are the actual 
parameter lists at each "call site". Instantiating the evar both 
provides the body term for the function and causes the function 
applications to be reduced at all call sites (instances).

Is that correct?

If so, that wasn't complicated, but it was mysterious.

What else besides rewrite can be used to directly alter a substitution?  
I determined that setoid_rewrite doesn't work.  I don't know how to 
target a substitution with a tactic "at" occurrence.

One can revert all hypotheses in the evar dependent subgoal, which 
induces skolemization of all of the instances, which then allows normal 
tactic targeting of those instance lists substitutions, because it makes 
them into visible actual parameter terms.  One can later do "intros" in 
the evar's dependent subgoal, and undo the skolemization.  But the fact 
that "rewrite aeqb" somehow managed direct access to the instance list 
seems to suggest that one might avoid skolemization in other ways as well?

-- Jonathan