The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2015 12:05 PM, Jonathan Leivent wrote:
> On 01/26/2015 11:48 AM, Jason Gross wrote:
> > A built-in [any] tactical lets you easily build [gprogress] (and many
> > others) in ltac, while otherwise a dedicated [gprogress]-like tactic
> > written in ocaml is needed for each tactic you want to have a global
> > version of.
>
> A case other than for use with [progress] where an [any] tactical 
> would be useful is for solver tactics that fail if they don't solve 
> the goal.  Such as: [any omega] - as that would tell you if omega 
> succeeded in any focused goal or failed in all.
>
> -- Jonathan

If one wants the most general such tactical (and perhaps not to have to 
revisit this) - it would probably be [nany N tac], where N is the number 
of focused goals where tac must succeed.  That way, [any tac] is [nany 1 
tac].  But, there is also then a global try via [nany 0 tac].  And a 
not-any via [let N:=numgoals in nany N (not tac)] - as the normally 
written "not" tactic would lose global focus and so [not any tac] would 
not work.

Alternatively, since there is now the guard tactical, perhaps have 
instead a "numsuc" tactical, which would behave by returning the number 
of focused goals on which it succeeds.  That way, [any tac] is [let 
n:=numsuc tac in guard n=1], numgoals is identical to [numsuc idtac], 
global try is [let x:=numsuc tac in idtac], not any is [let n:=numsuc 
tac in guard n=0].  One can also then do things like [let n:=numsuc tac 
in guard n > 2].

-- Jonathan