## 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: Feb 06 2023 at 11:03 UTC