The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I encourage you to comment to that effect in bugzilla.  However, I 
suspect that nobody will address this the proper way until Ltac2.

-- Jonathan


On 04/03/2017 05:02 PM, Robert Rand wrote:
> 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 
> <jonikelee AT gmail.com>
>  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