Hello, I’m having some trouble with Ltac2. I have a tactic definition in Ltac1 that I want to use from Ltac2. The exact definition doesn’t really matter, but it’s difficult to port to Ltac2 because of missing features.
From Stdlib Require Import Lia.
From Ltac2 Require Control Ltac1.
From Ltac2 Require Import Ltac2.
Ltac do_thing_impl int_param :=
match int_param with
| 0 => lia (* do one thing *)
| S _ => lia (* do another thing *)
end
.
Now I want to wrap this in an Ltac2 notation. I want the int_param to be optional and have a default value of 0 if it is left out, so I define two notations:
Ltac2 Notation "do_thing" param(constr) := Control.enter (fun () =>
ltac1:(int_param |- do_thing_impl int_param) (Ltac1.of_constr param)
).
(* default value of 0 *)
Ltac2 Notation "do_thing" := Control.enter (fun () =>
ltac1:(int_param |- do_thing_impl int_param) (Ltac1.of_constr constr:(0))
).
From my understanding of how goals are focused in Ltac2, if I want the tactic to focus on each goal individually, I’m supposed to wrap the tactic in Control.enter, so I can use it in a context like split; do_thing.
Indeed by wrapping it like this, the second notation works just fine, it solves every goal separately.
Lemma test : 1 + 1 = 2 /\ 2 - 1 = 1.
split; do_thing.
Qed.
However, when I use the notation that has additional parameters, it gives me error “Uncaught Ltac2 exception: Not_focussed”. If I substitute the right-hand side of the notation directly however, it works just fine.
Lemma test' : 1 + 1 = 2 /\ 2 - 1 = 1.
Fail split; do_thing 1.
(* works even though it should be totally equivalent: *)
split; Control.enter (fun () =>
ltac1:(int_param |- do_thing_impl int_param) (Ltac1.of_constr constr:(1))
).
Qed.
I’d like to figure out why it does this and if there’s a way to make the notation work. I think it might have something to do with “abbreviation notations”; maybe it interprets the parameter-free definition that way and handles it differently.