The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/24/2015 03:27 PM, Jonathan Leivent wrote:
> On 01/24/2015 10:29 AM, Jonathan Leivent wrote:
> > On 01/24/2015 02:43 AM, Jason Gross wrote:
> > > Hi,
> > >
> > > In trunk/8.5, is there a tactical that means "progresses in at least 
> > > one
> > > goal"?  I tried `progress [> intros ]`, but this fails if any of the 
> > > goals
> > > has no hypotheses to introduce, and I want it to fail only if all of 
> > > the
> > > goals have no hypotheses to introduce.
> > >
> > > Thanks,
> > > Jason
> >
> > I learned recently from Arnaud, by way of bug 3878, that attempting 
> > to keep a global focus in tactic expressions is very difficult. None 
> > of the tacticals - progress, once, try, etc.. - will keep a global 
> > focus.  Hence 'progress [> intros ..]' is equivalent to '[> progress 
> > intros..]'.
> >
> > -- Jonathan
>
> A more general request: an "any" tactical which retains global focus 
> and succeeds if its arg tactic succeeds in at least one subgoal.  In 
> which case, you could do: any (progress intros).
>
> Actually - I might be able to write such an "any" tactical in Ltac - 
> let me work on it...
>
> -- Jonathan

Ltac any tac :=
  try (is_evar ?__Any_flag;
       fail 1 "any: the evar name ?__Any_flag is being used");
  try (let A:=fresh in
       refine (let A:=?[__Any_flag]:bool in _);[shelve|];
       assert True as _; clear A);
  [> | try (try unify ?__Any_flag true; tac) ..];
  [> try (is_evar ?__Any_flag;
          fail 1 tac "failed on all subgoals");
     exact I | ..].

Goal True.
pose proof 0 as n.
destruct n.
all: any ltac:(idtac).
all: any ltac:(revert n).
all: any ltac:(progress intros).
Fail all: any ltac:(progress intros).
all: any ltac:(exact I).
Qed.

Note - you can't make "any" into a Tactic Notation (or wrap a Tactic 
Notation around it), as Tactic Notations always abandon global focus.  
[Requesting a fix to this will result in some Coq developer informing 
you that Tactic Notation is an abomination.]

-- Jonathan