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`

`pintros 5`

is doing 6 introductions.

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`

.

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`

)

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

If your notation took constr, most of your code would already work?

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

Pierre Vial has marked this topic as resolved.

Last updated: Jun 18 2024 at 22:01 UTC