The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Indeed ltac delays argument evaluation some of the time. This is one of the 
less well understood part of ltac.

If you dislike this, other languages such as ltac2 exist.

Gaëtan Gilbert

On 09/08/2021 20:35, Grant Jurgensen wrote:
> Hi all,
>
> I have been having trouble with higher-order Ltac and hoping someone here 
> might be able to illuminate the issue or point me in the right direction. I 
> have repeatedly run into unexpected behavior when passing Ltac to another 
> tactic. My best guess is that I am misunderstanding when Ltac arguments are 
> evaluated.
>
> Here is an example:
>
> ```
> Ltac hyp_eq H H' :=
>    match H with
>    | H' => idtac
>    end.
>
> Ltac revert_all_but H :=
>    repeat (match goal with
>    | H': _ |- _ =>
>        assert_fails (hyp_eq H H');
>        revert H'
>    end).
>
> Ltac revert_all_but2 H :=
>    repeat (match goal with
>    | H': _ |- _ =>
>        assert_fails (idtac; hyp_eq H H');
>        revert H'
>    end).
>
> Goal forall n m, n + m = m + n.
> Proof.
>    intros *.
>    (* This one does nothing *)
>    Fail progress revert_all_but m.
>    (* This one acts as expected *)
>    revert_all_but2 m.
> Abort.
> ```
>
> In this snippet, `revert_all_but H` is expected to revert all hypotheses 
> except `H`. However, the real behavior is that it does nothing. The alternate 
> tactic `revert_all_but2` adds an `idtac` statement to the Ltac passed to 
> `assert_fails`, and somehow this manages to fix the problem.
>
> I would have expected the two definitions to be equivalent, and I'm unsure 
> why adding the `idtac` statement changes its behavior. My best guess is that 
> in the original definition, the Ltac is executed before the function call in 
> a call-by-value style, whereas in the second, it is essentially being called 
> by name. Is this true? If so, why is some Ltac executed immediately, and some 
> not?
>
> Thanks,
> Grant Jurgensen