The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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