The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/24/2014 11:57 AM, Arnaud Spiwack wrote:
> Well, you are not forced to solve two subgoals. It's just that the
> existential variable which is introduced is materialised as a goal. You can
> use tactics in the first subgoal to give (partially) solve it such as in:
>
> Goal exists n, n=0.
> Proof.
>     refine (ex_intro _ _ _);[refine (S _) |].
>
> (of course [refine] is not that interesting as you could use [instantiate],
> but you are really free to use any tactic). The existential is not
> identified by a place in a term but by the corresponding goal. On the other
> hand, the goal can be solved by side effects as in:
>
> Goal exists n, n=0.
> Proof.
>     refine (ex_intro _ _ _);[|reflexivity].
>
> Nothing has been done in the first goal, but you may check that the proof
> engine sees it has been solved.

Oh - that's somewhat interesting.  The subgoals are linked.

But I still don't understand what the benefit of this new first subgoal 
that I get via refine (ex_intro _ _ _), but not via eexists.  It's 
weaker than the second subgoal, since it is solvable without the "=0" 
constraint.  Solving the second subgoal solves the first, but nothing 
done in the first subgoal aids in solving the second - quite the 
opposite - most solutions of the first subgoal make the second unsolvable.

When are these extra subgoals produced by refine useful?

-- Jonathan