Failed to use let-destruct for tuple in Coq

Question

I am a new user for Coq. I defined some functions:

Definition p (a : nat) := (a + 1, a + 2, a + 3). Definition q := let (s, r, t) := p 1 in s + r + t. Definition q' := match p 1 with | (s, r, t) => s + r + t end. 

I am trying to destroy the result of p in a tuple view. However, coqc complains about q:

 Error: Destructing let on this type expects 2 variables. 

while q 'can pass compilation. If I change p to return a pair (a + 1, a + 2), then the corresponding q and q 'work fine.

Why does let-destruct only allow a couple? Or did I make any syntax error? I checked with the Coq manual, but did not find a clue.

Thanks!

Answer 1

What is a bit confusing in Coq is that there are two different forms of destruction of let. The one you need requires a quote before the pattern:

 Definition p (a : nat) := (a + 1, a + 2, a + 3). Definition q := let '(s, r, t) := p 1 in s + r + t. 

The template prefix with a quote allows you to use nested templates and use custom notation in them. A form without a quote works only with single-level templates and does not allow you to use notations or refer to the names of constructors in your templates.