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) := ..

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

:'-(

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: Oct 13 2024 at 01:02 UTC