The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

Unfortunately, neither suggestion solves the problem. (I think "repeat" becomes local, and for the other suggestion, repeating within the "do" block doesn't help - type_check_once either solves the goal immediately or recognizes that it can't and does nothing.)

The thread linked to is very interesting - unfortunately, the suggestion at the end (below), no longer seems to be true in Coq 8.6. We'd stumbled upon the same approach in the tactic we were using (save that recursing proved unnecessary since we don't generate new goals) but it fails in Coq 8.6. (It works perfectly well in 8.5). 

Jonathan Leivent 2016-05-17 23:41:53 CEST

Just for the record.  There is a wasteful way in 8.5 to do terminating recursion that does not lose global focus:

Ltac grecur tac := let n:=numgoals in do n (tac; grecur tac).

So long as tac eventually prunes the number of goals down to 0, a call to grecur tac will eventually terminate.  However it will recurse more often than needed.

Were any of the global variants of tactics discussed in those threads implemented in subsequent Coq versions?

Thanks,

Robert

On Sat, Apr 1, 2017 at 8:22 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

What about

repeat progress type_check_once.

?

Best

P

Le sam. 1 avr. 2017 à 01:38, Jonathan Leivent <jonikelee AT gmail.com> a écrit :

On 03/31/2017 05:59 PM, Robert Rand wrote:
> Hi all,
>
> I'm trying to use Ltac to apply a tactic called type_check_once to all
> goals until no further progress can be made. Often this requires a cascade:
> type_check_once might instantiate a existential variable in goal #6 which
> then allows us to solve goal #3. No new goals are generated in this process.
>
> The problem is that the tactics seem to focus on a single goal, and does
> not cascade properly.
>
> In Coq 8.5 the following code worked but it fails in 8.6 (that is, we now
> have to call "all: type_check" multiple times in a row to solve all goals).
>
> Ltac type_check := let n := numgoals in do n type_check_once.
>
> (I've also tried using [> type_check_once..] in place of type_check, but
> this doesn't seem to buy us anything.)
>
> The following two approaches seemed to show promise, but both fail in some
> cases, for reasons unclear to me:
>
> Ltac type_check_num :=
>    let pre := numgoals in
>    type_check_once;
>    let post := numgoals in
>    tryif (guard post < pre) then type_check_num else idtac.
>
> Ltac type_check_circ :=
>    intros; compute;
>    try (progress [> type_check_once ..]; type_check_circ)
>
> Any suggestions?

Robert,

Have you tried:

Ltac type_check := let n := numgoals in do n repeat type_check_once.

You also might be interested in the lengthy discussion in
https://coq.inria.fr/bugs/show_bug.cgi?id=3878

-- Jonathan