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 thinkinteger
relates to anLtac
integer not anat
.
You can either replaceinteger
withconstr
, or replacepintros p
withdo 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: Sep 23 2023 at 14:01 UTC