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: Apr 18 2024 at 13:01 UTC