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.

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.

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

?

`ltac:()`

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

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

Note that inside terms you can also directly write

```
Eval cbv in (square x).
```

like

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

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?

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.

`pose`

in turn expects a term as an argument so we have to use `ltac:()`

to give it using a tactic.

and actually, theos comment also applies

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.

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

Last updated: Jun 25 2024 at 15:02 UTC