Hi,

I am trying to define a tactical that performs some operations on the proof environment before applying the argument (a tactic) to the (modified) goal. But I cannot manage to delay the execution of the (tactic) argument.

Here is an example:

```
Ltac combine tac1 :=
match goal with
H:nat |- _ => revert H; tac1
end.
Ltac mytac :=
(match goal with
| H:nat |- _ => idtac "AAA"
| _ => idtac "BBB"
end).
(* Tactic Notation (at level 4) tactic4(tac1) ";;" tactic4(tac2) := combine tac1 tac2. *)
Goal forall n:nat, True.
Proof.
intro.
(* Set Ltac Debug. *)
combine ltac:(mytac).
```

Since combine does "revert" before applying tac, I expect to see "BBB", but I get "AAA".

Is it possible to force the delay of the tactic taken in argument?

You can change the definition of `mytac`

from `match goal`

to `idtac; match goal`

to modify its status.

what we usually do is explicit thunking

so that would mean calling `combine ltac:(fun _ => mytac)`

and invoking `tac1`

in `combine`

via `tac1 ()`

but yeah, ltac also has completely bonkers evaluation order and it can be made more sane by using `idtac; match`

instead of `match`

Thanks! But how can I have a nice tactic notation which hides the `idtac;`

trick? So that for instance people would write `combine intro`

for instance?

```
Tactic Notation "combine" tactic3(tac) :=
idtac; match goal with
H:nat |- _ => revert H; tac
end.
```

I think stuff like this works for us (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v).

and you might not need the `idtac`

here, not sure. I often add "defensive `idtac`

" because you never know when ltac is out to screw you.

note that `Ltac :=`

and `Tactic Notation :=`

can behave very differently

If you are using `Tactic Notation`

, I don't think you even need `idtac`

, since `tac`

will be substituted in the notation before being evaluated.

My experience is that Tactic notation triggers evaluation more than Ltac. Example below with combine and combine_app that are supposed to first revert H *and then* perform print_goal. I could not find a way to delay with notations.

```
Ltac print_goal :=
match goal with
| H: _ |- _ => idtac H; fail
| |- ?g => idtac "======"; idtac g
end.
Ltac combine tac1 tac2 :=
match goal with
H: _ < _ |- _ => revert H ; tac1 ; tac2
end.
Ltac combine_app tac1 tac2 :=
match goal with
H: _ < _ |- _ => revert H ; tac1 () ; tac2 ()
end.
Tactic Notation (at level 4) tactic4(tac1) ";;" tactic4(tac2) := combine ltac:(tac1) tac2.
Tactic Notation (at level 4) tactic4(tac1) ";;;" tactic4(tac2) :=
combine ltac:(idtac;tac1) ltac:(idtac;tac2).
Tactic Notation (at level 4) tactic4(tac1) ";;;;" tactic4(tac2) :=
combine_app ltac:(fun _ => tac1) ltac:(fun _ => tac2).
Goal forall n m:nat, n<m -> True.
Proof.
intros n m H.
print_goal ;; print_goal. (* ==> n m H*)
intros H.
print_goal ;;; print_goal. (* ==> n m H*)
intros H.
print_goal ;;;; print_goal. (* ==> n m H*)
intros H.
(idtac;print_goal) ;;;; (idtac;print_goal). (* n m *)
```
```

That is quite surprising. And there is even worse: `(idtac; print_goal) ;; print_goal`

. The first tactic is still broken, but it magically fixes the second one. This is crazy.

Indeed. I really don't see any way around this.

basuically, this does what I want:

```
combine_app ltac:(fun _ => print_goal) ltac:(fun _ => print_goal).
```

but it seems impossible to have a nice syntax for it.

Maybe Ltac2 would have a way to delay?

No. Or rather, it would be the same as in Ltac, that is, define `Ltac print_goal _ := ...`

.

Yes but this is not acceptable for my use case: I want people to write `destruct H ;; intro h`

and not `fun () => destruct H; fun () => intro h`

.

I need a `Tactic Notation delayedtactic(x) ";;" delayedTactic(Y) := ..`

:'-(

Ltac2 should let you write notation like

```
Notation "combine a b" := combine_app (fun _ => a) (fun _ => b)
```

at least I'd expect that from any sensible system^^

also Ltac2 fixes all the evaluation order craziness

For the record, `Tactic Notation`

in Ltac is *not* a notation system.

It does much more than that.

Last updated: Jan 31 2023 at 13:02 UTC