Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] gprogress tactical?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] gprogress tactical?


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] gprogress tactical?
  • Date: Sat, 24 Jan 2015 16:38:52 -0500


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




Archive powered by MHonArc 2.6.18.

Top of Page