✔ Lost in Tactic Notation · Coq users

Hey,
Trying to understand tactic notations here (too bad there aren't examples in the refman).
Currently, I want to combine tactics here in a very simple way, but whatever I do, this fail. Basically, I'm writing a tactic which has a parameter p (an int). The tactic performs p intros. After that, it introduces a new hypo H, applies inversion to H and then reflexivity.
But the following code fails with the message:

Must evaluate to a closed term
offending expression:
p
this is an object of type int
Not in proof mode.

Ltac pintros p := intro ;
  match p with
  | S ?p0 => pintros p0
  | 0 => idtac
  end.

Ltac pintros_inv p := (pintros p ; let HProd := fresh "H" in
intro HProd ; inversion HProd ; reflexivity).

Tactic Notation "pintros_inv" integer(k) := pintros_inv (k).
   (* note that I'm not sure of this*)

Ltac pintros_inv0 p :=
  match p with
  | S ?p0 => intro ; pintros_inv0 p0
  | 0 => let HProd := fresh "H" in
  intro HProd ; inversion HProd ; reflexivity
  end.

Tactic Notation "pintros_inv0" integer(k) := pintros_inv0 (k).
  (* not sure of this either *)

Lemma foo:  forall (A : Type) (l : list A) (def : A) (a : A) (l0 : list A),
 l =  a :: l0 -> ((match l with
 | [] => def
 | a :: l0 => a
 end) = a).
Proof.
 (*  pintros 5 would work fine here, but the following fails: *)
  Fail pintros_inv 5. Fail pintros_inv0 5.
Abort.

I can circumvent this with Ltac2, but I'm using a plugin which does not support it. Anyway, I'm interested in understanding how things work in Ltac1

Olivier Laurent (Sep 26 2022 at 15:05):

Olivier Laurent (Sep 26 2022 at 15:16):

Now concerning your Tactic Notation problem, I think integer relates to an Ltac integer not a nat.
You can either replace integer with constr, or replace pintros p with do p intro.

Pierre Vial (Sep 26 2022 at 17:42):

Putting do p intro works, thanks!
So I get what wasn't working in the first tactic: I was working with Coq natural numbers instead of Ltac ints.
But is there a way to define a recursive tactic by doing an induction on Ltac ints ? (apparently, calling the value for p - 1 is also interpreted as inside nat)

Paolo Giarrusso (Sep 26 2022 at 19:31):

Ltac is able to compute on Coq nats, you need lots of eval compute and ltac matches

Paolo Giarrusso (Sep 26 2022 at 19:33):

Pierre Vial (Sep 26 2022 at 20:46):

Yes, I guess it would work, but I was just wondering if one could just avoid Coq integers altogether, but I guess Ltac does not really have a proper integer type

Stream: Coq users

Topic: ✔ Lost in Tactic Notation