The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/24/2015 07:53 PM, Jason Gross wrote:
> Nice!  (The logic might be a bit easier to read with [tryif], perhaps?)

Sure, but then there would be a bunch of [else idtac]'s floating 
around.  Maybe that's better, regardless.

> Remind me what "?[__Any_flag]" means?  Is it "new evar with name
> ?__Any_flag"?  And why [try unify] rather than [unify]?

The truly ugly hack here is related to the hard-coded evar name 
?__Any_flag.  The form ?[__Any_flag] is as you say - it creates an evar 
with that name, but fails if one already exists.  That failure case here 
is key - as that allows this tactic to break symmetry across the goals - 
so that exactly one goal can do some work (in this case, assert another 
trivial goal to have in case tac solves all goals) while the others 
don't bother.  That could also sometimes be done with [> do work | don't 
do work..] - but in this case, the evar is also needed as a way to 
communicate information across goals - so two birds with one stone.  The 
times where [> do work | don't do work..] would fail are if there are no 
goals - and in that case, the hard-coded evar trick can still succeed.  
Also note that allowing Coq to generate a fresh evar name and then get 
it via something like let E:=eval cbv delta [H] in H in ... would fail 
because such a let would lose the global focus - another reason to use a 
hard-coded evar name.

The "try unify" is because, once the first unify succeeds, the evar 
disappears, so subsequent unifies against it will fail.

> -Jason
> On Jan 24, 2015 1:40 PM, "Jonathan Leivent" 
> <jonikelee AT gmail.com>
>  wrote:
>
> > 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