## Stream: Coq users

### Topic: Delayed execution of tactic

#### Pierre Courtieu (Jun 24 2021 at 12:10):

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?

#### Guillaume Melquiond (Jun 24 2021 at 12:40):

You can change the definition of `mytac` from `match goal` to `idtac; match goal` to modify its status.

#### Ralf Jung (Jun 24 2021 at 13:15):

what we usually do is explicit thunking

#### Ralf Jung (Jun 24 2021 at 13:15):

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

#### Ralf Jung (Jun 24 2021 at 13:15):

and invoking `tac1` in `combine` via `tac1 ()`

#### Ralf Jung (Jun 24 2021 at 13:16):

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

#### Pierre Courtieu (Jun 24 2021 at 13:36):

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?

#### Ralf Jung (Jun 24 2021 at 13:43):

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

#### Ralf Jung (Jun 24 2021 at 13:44):

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.

#### Ralf Jung (Jun 24 2021 at 13:44):

note that `Ltac :=` and `Tactic Notation :=` can behave very differently

#### Guillaume Melquiond (Jun 24 2021 at 13:55):

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.

#### Pierre Courtieu (Jun 24 2021 at 14:38):

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 *)

```
``````

#### Guillaume Melquiond (Jun 24 2021 at 15:10):

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.

#### Pierre Courtieu (Jun 24 2021 at 15:15):

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?

#### Guillaume Melquiond (Jun 24 2021 at 15:17):

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

#### Pierre Courtieu (Jun 24 2021 at 15:18):

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`.

#### Pierre Courtieu (Jun 24 2021 at 15:19):

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

:'-(

#### Ralf Jung (Jun 24 2021 at 16:48):

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^^

#### Ralf Jung (Jun 24 2021 at 16:48):

also Ltac2 fixes all the evaluation order craziness

#### Pierre-Marie Pédrot (Jun 24 2021 at 17:24):

For the record, `Tactic Notation` in Ltac is not a notation system.

#### Pierre-Marie Pédrot (Jun 24 2021 at 17:24):

It does much more than that.

Last updated: Jun 14 2024 at 19:02 UTC