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
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)
but yeah, ltac also has completely bonkers evaluation order and it can be made more sane by using
idtac; match instead of
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.
Ltac := and
Tactic Notation := can behave very differently
If you are using
Tactic Notation, I don't think you even need
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