Stream: Ltac2

Topic: Ltac1 - Ltac2 interaction

Pierre Courtieu (Jun 28 2021 at 18:17):

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!).

Michael Soegtrop (Jun 29 2021 at 07:17):

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.

Pierre Courtieu (Jun 29 2021 at 07:20):

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

Pierre Courtieu (Jun 29 2021 at 07:21):

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