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
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.
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: Jan 31 2023 at 10:01 UTC