The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/31/2015 02:38 PM, Jason Gross wrote:
> 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.

There are "hacks" that purposefully share evars that aren't even in 
goals to begin with, using tricks that name evars explicitly like 
"pose(x:=?E)".  That "any" tactical I wrote is an example.  However, in 
such cases, one would know that one was doing such "evar hacks", and if 
there was some "sync" tactical, would use that - like tac1; sync; tac2 
to force the sequence to not be [> tac1; tac2..], but instead be 
[>tac1..];[>tac2..].  Or, maybe just repurpose the [>tac1..];[>tac2..] 
form to be the case where no backtracking optimization pruning is done.

Another point about the importance of this problem: automation tactics 
such as (e)auto perform backtracking (in 8.5) as if the tactic hints 
they use are strung together with the normal sequencing tactical: tac1; 
tac2; tac3.  So this is a problem for proof automation as well as 
explicit proof scripts.  Maybe even more so, as one would perhaps be 
more likely to use tactics with multiple successes as hints than in 
explicit proof scripts, as well as to be less informed of the 
possibility of combinatorial explosion as a result (since the hints are 
scattered).

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

Yes - maybe have Coq do some very simple testing.  The naive case would 
be: if there is no ?E for which ?E appears in both goals (or if ?E is 
one of those goals), then assume that they can be backtracked 
independently.  In the case where ?E is one of the goals - that goal 
might need to be backtracked from others that mention ?E, but not vice 
versa.

A more advanced version that might still be easy to implement:  If a 
tactic doesn't instantiate an evar, then even though an evar is present 
that is shared with some other goal, backtracking of that tactic on a 
goal can be done independently of other goals at least until some 
alternative success of that tactic does instantiate the evar.  (In 
general, tactics that don't instantiate evars are "friendlier" to proof 
search - a motivation for enhancement request #3872.).  On the 
"receiving" side, if a tactic "consumes" an evar without referring to 
its instantiation - as referring to evar(n:nat) as a nat regardless of 
its value would do - then backtracking across to goals that do the 
instantiation is useless.

Even more refinement is possible - because the issue is really with 
identical instances of the same evar, not with distinguishable instances 
of the same evar - however, in 8.5, Coq doesn't seem to handle this in 
the most rigorous way (see bug #3918).  Ideally, Coq should not force an 
instance of an evar to be a possibly translated instantiation from a 
different instance of the same evar if there is some discriminable 
difference between the two instances - in other words, if one could 
instead instantiate the evar with a match expression that has different 
values for the branches that represent those two instances.  If Coq 
behaved that way, then there would be no need to backtrack across goals 
that shared evars and even instantiated them, as long as the instances 
were discriminably different.

[there seems to be some similarity in this problem to those in 
concurrent databases, which was my previous profession - or maybe all 
problems just look alike after a while]

-- Jonathan