## Stream: Coq users

### Topic: let in with pair in Latc (beginner)

#### Pierre Vial (Jan 19 2021 at 14:36):

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 ?

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:44):

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

#### Théo Winterhalter (Jan 19 2021 at 14:44):

``````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?

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:44):

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

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:45):

As written above by @Théo Winterhalter you have to use the Ltac `match` construction to observe a Coq term.

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:46):

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

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:46):

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

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:47):

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

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:48):

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

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:48):

It's easy to create exponential behaviours that way.

#### Théo Winterhalter (Jan 19 2021 at 14:49):

I updated to `lazymatch` because we certainly don't want to backtrack on matching.

#### Pierre-Marie Pédrot (Jan 19 2021 at 14:49):

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)

#### Pierre Vial (Jan 19 2021 at 15:10):

@Théo Winterhalter
Mmh

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

fails with

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

#### Théo Winterhalter (Jan 19 2021 at 15:11):

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

#### Pierre Vial (Jan 19 2021 at 15:11):

@Pierre-Marie Pédrot
Huh, how could `match` trigger backtracking here? Since the output of `f` is necessarily a pair

#### Pierre Vial (Jan 19 2021 at 15:12):

@Théo Winterhalter
In this example, `tac 8` should print 64 and 16

#### Guillaume Melquiond (Jan 19 2021 at 15:12):

It is the branch of `match` which triggers backtracking (here `idtac`, which does not, but another tactic could)

#### Pierre Vial (Jan 19 2021 at 15:13):

@Guillaume Melquiond oh yes, thanks

#### Théo Winterhalter (Jan 19 2021 at 15:19):

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

#### Pierre Vial (Jan 19 2021 at 15:23):

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

Last updated: Jun 18 2024 at 21:01 UTC