The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/09/2014 01:19 PM, Jonathan wrote:
> ...
> 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.

The confusion in the error messages is really not that confusing after 
realizing that by using "all:", the apply tactic is sequentially applied 
to each focused subgoal in order.  With that in mind, the first "Error: 
No such hypothesis: H" is due to H being removed from the second subgoal 
by the apply in the first - as the example demonstrates.  The second 
"Error: Cannot change H, it is used in conclusion" is because applying 
eq_sym in H in the evar subgoal correspondingly alters the evar 
instantiation in the first such that H does appear in its conclusion.  
So, these are not bugs.

Still, having the ability to lock down hypotheses like H due to the evar 
dependencies would be nice...

-- Jonathan