The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

They are useful because I can use tactics to solve them interactively.  If the interesting bit is the first subgoal, and the constraint is something that should be solvable by some general tactic that isn't good enough to fill in evars, then you can first construct your term, and then later prove the laws.  For example, this means that I can construct a category interactively, rather than having to first construct the objects, morphisms, composition, and identity, all in one go, and then only getting to prove the laws interactively.

-Jason

On Thu, Jul 24, 2014 at 5:43 PM, Jonathan <jonikelee AT gmail.com> wrote:

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