Stream: Coq users

Topic: Compute inside a ltac term (beginner's question)

Pierre Vial (Dec 08 2020 at 09:04):

Hi,
I would like to use evaluation strategies while I'm using Ltac. For instance, if I write:

Definition square x := x * x.

Goal 2 + 2 = 4.
Proof. pose (square 2) as k.

I will obtain k:= square 2 in the context. I can then write cbv in k to obtain that k is equal to 4. How should I do to obtain 4 directly?
I mean, something in the lines of:
Ltac square_cbv_tac x := let s := constr:(square x) in cbv s. (which of course does not work) so that pose (square_cbv_tac 2) as k gives me directly that k is equal to 4.

Kenji Maillard (Dec 08 2020 at 09:13):

I think you could use something like Ltac square_cbv_tac x := let t := eval cbv in (square x) in exact t., but then you would need to use another invocation for pose (maybe pose ltac:(square_cbv_tac 2)) as k ?) or change the tactic so it does the posing for you.

Pierre Vial (Dec 08 2020 at 09:49):

Thanks @Kenji Maillard , this works the way you say. However, is there a reason why if I write Ltac square_cbv_tac x := ltac:(let t := eval cbv in (square x) in exact t) (i.e. I put ltac: in the tactic), I still need to write pose ltac:(sq....)?

Théo Winterhalter (Dec 08 2020 at 10:11):

ltac:() is the syntax to write tactics inside terms. Inside tactics you don't need it.

Théo Winterhalter (Dec 08 2020 at 10:12):

Ltac square_cbv_tac x :=
  let t := eval cbv in (square x) in
  exact t.

Théo Winterhalter (Dec 08 2020 at 10:13):

Note that inside terms you can also directly write

Eval cbv in (square x).

like

Definition foo : nat :=
  (Eval cbv in square 2) + 3.

Pierre Vial (Dec 08 2020 at 10:34):

Yes, but what I don't understand is that pose is a tactic, so why should we write pose ltac:(square_cbv...) if the declaration of square_cbv_tac already specifies that the output should be taken as a ltac term?

Fabian Kunze (Dec 08 2020 at 10:36):

the "ltac:" is important for parsing. The parser assumes then when you with 'pose', the next thing is a term, so if you want a different shing there you need to tell it to the parser.

Théo Winterhalter (Dec 08 2020 at 10:36):

pose in turn expects a term as an argument so we have to use ltac:() to give it using a tactic.

Fabian Kunze (Dec 08 2020 at 10:36):

and actually, theos comment also applies

Fabian Kunze (Dec 08 2020 at 10:40):

Note that "ltac:" has two uses,
-make sure that you parse the thing as tactic
-if ltac: occured whre a constr was expected, perform some magic so that the ltac:() stands for the term that the tactic produces.

AFAIK it is merely a coincidence(.suggestive choice) that both use cases use the same syntax.

Pierre Vial (Dec 08 2020 at 11:00):

Ok thanks @Théo Winterhalter and @Fabian Kunze , I get it better now!

Last updated: Sep 23 2023 at 08:01 UTC