Hi,

I'm having difficulties doing a `let in`

defining a pair in Ltac , more precisely something of the form `let (a,b) := f ... in`

where `f`

is a coq function.

I'm considering:

- a tactic
`gtac t idtt`

which takes a term`t`

, makes a few computations (giving a result`r`

) and ends with`pose r as itdtt`

- a Coq function
`f`

that outputs a pair.

Here is a minimal non trivial example.

```
Definition f (x : nat * nat) := let (a, b) := x in (a * a , 2 * b).
Ltac g_tac t idtt := pose (t , t) as idtt.
Ltac bad_tac n := let idk := fresh "k" in (g_tac n idk ; let (x,y) := constr:(f idk)) in idtac (x,y)).
```

I obtain the error

```
Error: Syntax error: 'rec' expected after 'let' (in [tactic:binder_tactic]).
```

I tried most variants that came to mind, e.g., `let (?x,y) :=...`

, `let constr:((x,y)) := ...`

and so on, but nothing works.

What is happening here? And what does the error mean ?

You're confusing the Ltac-level let-binding with the Coq-level one.

```
Ltac tac n :=
let idk := fresh "k" in
g_tac n idk ;
let foo := constr:(f idk) in
lazymatch foo with
| (?x,?y) =>
idtac x y
end.
```

Works?

Ltac has no pairs, so it doesn't even feature a destructuring let binding

As written above by @Théo Winterhalter you have to use the Ltac `match`

construction to observe a Coq term.

(sorry for pinging the other Théo, my autocomplete is the fastest in the wild west)

@Pierre Vial anyways don't confuse Ltac `match`

with Coq `match`

Although they have similar syntaxes they're very different beasts.

Another caveat with @Théo Winterhalter solution is that the tactic in the branch may trigger backtrack.

It's easy to create exponential behaviours that way.

I updated to `lazymatch`

because we certainly don't want to backtrack on matching.

When you destruct from Ltac a Coq term, it's recommended to either use lazymatch or perform a commutative cut (this might be harder done than said)

@Théo Winterhalter

Mmh

```
Goal 2 + 2 = 4.
tac 8.
```

fails with

```
Error: No matching clauses for match.
```

I did not test it because I don't know what you want to do.

@Pierre-Marie Pédrot

Huh, how could `match`

trigger backtracking here? Since the output of `f`

is necessarily a pair

@Théo Winterhalter

In this example, `tac 8`

should print 64 and 16

It is the branch of `match`

which triggers backtracking (here `idtac`

, which does not, but another tactic could)

@Guillaume Melquiond oh yes, thanks

Yeah sorry, as @Pierre-Marie Pédrot said, Ltac `match`

is not the same as that of Coq and it will not compute anything.

So `foo`

is equal to `f k`

but not to a pair. If you want to get a pair, you have to evaluate it.

```
Ltac tac n :=
let idk := fresh "k" in
g_tac n idk ;
let foo := constr:(f idk) in
lazymatch eval hnf in foo with
| (?x,?y) =>
idtac x y
end.
```

This works now :upside_down: , thanks @Théo Winterhalter and @Pierre-Marie Pédrot !

Last updated: Oct 13 2024 at 01:02 UTC