Hi,

I need help to define correctly a tactical for ltac1 tactics and I think ltac2 is the only way to go, because `Tactic Notation`

and `ltac1`

are so bizarre. I think I need the `thunk`

feature from ltac2.

Here is the (simplified) tactical I want a good syntax for:

```
(* This reverts one hyp of the form (_<_) AND THEN applies tac. *)
Ltac combine tac1 :=
match goal with
H: _ < _ |- _ => revert H ; ltac:(tac1)
end.
```

Now I want to define the syntax `tac !!`

which performs `combine tac1`

. The difficulty is that it should work for ANY tactic, not just the one that starts by `idtac;`

or the ones that are actually taking one argument: I don't want the user to write `(idtac; foo) !!`

instead of `foo !!`

.

Here is one of my attempts:

```
(* Example tactic: it prints the goal. It takes no argument. *)
Ltac print_goal :=
idtac;match goal with
| H: _ |- _ => idtac H; fail
| |- ?g => idtac "======"; idtac g
end.
Require Import Ltac2.Ltac2.
Local Ltac2 ltac2_combine (tac1: unit -> unit) := ltac1:(tac1 |- combine_app ltac:(tac1) ).
Ltac2 Notation tac1(thunk(tactic)) "!!" := (ltac2_combine tac1).
Goal forall n m:nat, n<m -> True.
Proof.
intros n m H.
ltac1:(print_goal) !!. (* "should have type unit" *)
```

Any help welcome, I am quite new to ltac2 (which looks very nice!).

I don't think one can do this. The arguments to `ltac1:( |- )`

should be a Coq term - I don't think it could be a Ltac1 tactic and even less a ltac2 function. The `ltac1:(print_goal)`

wraps the ltac1 tactic in a ltac2 function and I don't see how one could feed this back to an ltac1 tactic as tactic argument.

The `ltac1:(tac1 |- combine_app ltac:(tac1) )`

construct is a lambda btw. - it expects an argument (which should be a Coq term).

Of cause it would be easy to do if `combine`

would be written in Ltac2.

That is what I am currently trying, hence my second question about postfix notation.

thanks I understand the problem now. Definining combine in ltac2 is not a problem I guess.

Last updated: Oct 12 2024 at 12:01 UTC