The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Nice!  (The logic might be a bit easier to read with [tryif], perhaps?)

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

-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