The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

After more experimentation with the evar dependent subgoals (via refine) 
feature in the trunk...

I noticed that when a hypothesis in one subgoal with evars is modified 
as by a rewrite .. in hyp or apply .. in hyp, such that instance lists 
(via Set Printing Existential Instances) mention that hypothesis, the 
hypothesis is removed from the corresponding evar subgoals (and 
obviously also the instance lists).  This makes some sense, as Coq would 
otherwise need to know how to reverse that modification to create an 
adequate substitution (in the case of a rewrite-in that is often 
possible, but not an apply-in).  But it is surprising, and unfortunately 
could lead to an inability to solve those evars later.

Since I have no documentation on the evar dependent subgoals feature (is 
there any?), this might be a bug or just a temporary measure that isn't 
the eventual desired behavior.  Assuming however that it is the desired 
behavior:  in order to prevent proof automation from accidentally making 
such modifications to hypotheses (without making the identical 
modifications in the evar subgoals themselves), how about adding a 
command like Set Lock Existential Dependent Hypotheses - which would 
then cause Coq to fail in such cases - similarly to how it currently 
fails if an attempt is made to alter a hypotheses on which another in 
the same subgoal (or the consequent) depends (at least for 
non-"dependent" variations of tactics)?

Example:

Set Printing Existential Instances. (*or View->Display existential 
variable instances*)
Goal forall a b:nat, a=b -> exists c:nat, c>a.
intros a b H.
refine (ex_intro _ _ _).
all:cycle 1.
apply eq_sym in H. (*removes H from evar subgoal and instances*)

With the requested Set Lock Existential Dependent Hypotheses turned on, 
that last apply would fail (unless it was applied in the evar subgoal as 
well).

Oh - that points out some bugs.   If you instead do "all:apply eq_sym in 
H", it fails with "Error: No such hypothesis: H" - even though H exists 
in both subgoals.  And if you try the "all:apply eq_sym in H" without 
first doing "all:cycle 1", it also fails, but this time with "Error: 
Cannot change H, it is used in conclusion." - even though H is not used 
in the conclusion.

Should I report these, or are evar dependent subgoals under active 
development and the above are just temporary behaviors?

-- Jonathan