The Coq mailing list

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

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:

Since this very morning. And thanks to Hugo Herbelin, the substitutions of existential variables are systematically printed (in fact, only the part which is not the identity). The printed substitution tells you by name what is substituted. This should help users figure how they work.

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.

Correct.
 

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).

Indeed. And the instance can be seen as the relation between the two contexts.
 

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?

It is a way to think about it yes. Though, there are good reasons for evars not to be actual functions and have formal parameters like they do currently.

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.

Setoid rewrite could work depending on the particulars. Anything which my replace a variable would do just as well. The destruct and induction tactic would be significant offenders.

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?

Maybe. Let us know what works for you.