## Stream: Coq users

### Topic: ✔ Lost in Tactic Notation

#### Pierre Vial (Sep 26 2022 at 14:59):

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` `intro`s. 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.
``````

I wrote two different tactics to obtain this, but both fails:

``````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):

`pintros 5` is doing 6 introductions.

#### 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):

Olivier Laurent said:

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`.

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` `int`s.
But is there a way to define a recursive tactic by doing an induction on `Ltac` `int`s ? (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

#### 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