The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 12/02/2014 10:08 AM, Frédéric Besson wrote:
> Hi,
>
> What about redefining a do like tactic ?
>
> Ltac mydo x tac :=
>    match x with
>      | O => idtac
>      | S ?n => tac ; (mydo n tac)
>    end.
>
> Goal True.
>    let N := eval compute in (1 + 2) in
>        let tac := idtac 0 in
>        mydo N tac.
> Abort.
>
> Best,
> —
> Frédéric

Amusingly, I was trying to use "do N ..." to avoid doing recursion in a 
case where I can calculate the number of iterations of a tactic I need.

So, my options appear to be:
1. write a plugin
2. try ssreflect
3. just do everything in Ltac via recursion

I've looked through the existing plugins and tactics, but it isn't 
obvious how to write a tactic that would convert from a numeric Gallina 
term into an Ltac number (ocaml integer?).

I will look at ssreflect - provided I can get one built and working for 
the trunk version of Coq.

In the meantime, just stick to recursion and avoid math in Ltac.

-- Jonathan

> > On 1 déc. 2014, at 22:22, Jonathan 
> > <jonikelee AT gmail.com>
> >  wrote:
> >
> > The following works:
> >
> > Goal True.
> > let N := 3 in do N idtac 0.
> > Abort.
> >
> > It produces 3 lines of "0".
> >
> > So, why doesn't the following work?:
> >
> > Goal True.
> > let N := eval compute in (1 + 2) in do N idtac 0.
> > Abort.
> >
> > It produces the error: "Error: Ltac variable N is bound to a term which cannot be coerced to 
> > an integer.", with CoqIDE underlining the N in "do N idtac 0" as the source of the 
> > error.
> >
> > How does one compute with integers in Ltac?
> >
> > -- Jonathan