The Coq mailing list

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

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.

If you know in advance that you will solve the goal by unification (or [instantiate]), you can use the [shelve] tactic put the goal out of the way (and you get back more or less the behaviour of [eexists]):

Goal exists n, n=0.
Proof.
   refine (ex_intro _ _ _);[ shelve |].

If you are going to solve every existential variable by unification, you can put them globally out of the way with the [shelve_unifiable] tactic (which calls [shelve] on every goal which appears as an existential variable in another goal).

Goal exists n, n=0.
Proof.
   refine (ex_intro _ _ _); shelve_unifiable.

That's how it works. I don't know if it is something you need for your use case, though.

On 24 July 2014 16:42, Jonathan <jonikelee AT gmail.com> wrote:

On 07/24/2014 10:28 AM, Arnaud Spiwack wrote:

Try this in trunk. It will hopefully explain better than words:

Goal exists n, n=0.
Proof.
   refine (ex_intro _ _ _).

Currently the only way to introduce dependent subgoal is to use the
[refine] tactic.

I still don't get it.  If I use "eexists" instead of that refine, I get only the second subgoal that refine produces, not the first. How is being forced to solve two subgoals better than one?

Maybe exists/ex_intro is a poor example - but wouldn't econstructor work in the general case?

-- Jonathan

On 24 July 2014 15:05, Jonathan <jonikelee AT gmail.com> wrote:

On 07/24/2014 05:27 AM, Arnaud Spiwack wrote:

... the new dependent subgoal feature

What is the new dependent subgoal feature?

-- Jonathan