The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

How does one determine when goals can share an evar?  You gave a tactic that constructs an evar shared by all the goals, so you could presumably construct a tactic that requires backtracking across goals.

I agree, though, Coq should not backtrack across goals that naively share no evars.  Perhaps there should be a setting that disables this pruning?

On Sat, Jan 31, 2015 at 12:00 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Is there anything other than the existence of one or more existential variables shared by the goals that would require backtracking across goal boundaries?

If not, maybe this indicates a possible way Coq could optimize the backtracking search space by pruning out parts that can be easily shown to be redundant.

The issue may not be limited to top-level global-vs-local focus - in other words - just the proper use of "[>...]".  The backtracking across goals can also be an issue for subgoals of a multiple-subgoal-producing tactic - so that things like "tac0; [tac1; tac2; tac3..]"  where tac0 produces multiple subgoals from one goal (case analysis tactics, for example) might run much faster than "tac0; tac1; tac2; tac3".  And of course that pattern nests. But, it soon becomes quite cumbersome to write the thoroughly nested: "tac0; [tac1; [tac2; [tac3 ..]..]..]" intead of "tac0; tac1; tac2; tac3".  Also, it might be difficult for proof script writers to tell whether the faster form is sufficient for finding the solution - or, in general, which parts of the script can be put into the faster form without loss of solution.

-- Jonathan

On 01/31/2015 12:30 AM, Jason Gross wrote:

I think "[ > tac1; tac2; tac3 ]" is preferred when some tactics in the
sequence "tac1; tac2; tac3" have multiple successes, but you can guarantee
that all backtracking that needs to happen can happen within a single goal,
rather than needing to backtrack across goal boundaries.

-Jason
On Jan 30, 2015 9:48 PM, "Jonathan Leivent" <jonikelee AT gmail.com> wrote:

When one has several backtracking-capable tactics with multiple successes
- say tac1, tac2, and tac3 - when is it preferable to write "tac1; tac2;
tac3" instead of "[> tac1; tac2; tac3 ..]"?

-- Jonathan