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.
gtac t idttwhich takes a term
t, makes a few computations (giving a result
r) and ends with
pose r as itdtt
fthat 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.
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
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)
Goal 2 + 2 = 4. tac 8.
Error: No matching clauses for match.
I did not test it because I don't know what you want to do.
Huh, how could
match trigger backtracking here? Since the output of
f is necessarily a pair
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.
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: Feb 01 2023 at 13:03 UTC