Nie można użyć let-destruct dla krotki w Coq

Question

Jestem nowym użytkownikiem Coq. Zdefiniowałem niektóre funkcje:

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. 

Próbuję zniszczyć wynik p w reprezentacji krotki. Jednak coqc narzeka na q:

Error: Destructing let on this type expects 2 variables. 

natomiast q 'może przekazać kompilację. Jeśli zmienię p, aby zwrócić parę (a + 1, a + 2), odpowiednie q i q 'działają bez zarzutu.

Dlaczego zezwala się tylko na zezłomowanie? Czy popełniłem błąd w składni? Sprawdziłem z podręcznikiem Coq, ale nie znalazłem żadnej wskazówki.

Dziękujemy!

Answer 1

W Coq jest trochę mylące jest to, że są dwie różne formy niszczenia niech. Jedna jesteś przed wzór szuka potrzeb cytat:

Definition p (a : nat) := (a + 1, a + 2, a + 3). 

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

przedrostkiem wzór z cytatem pozwala używać zagnieżdżonych wzory i używać zdefiniowanych przez użytkownika w nich zapisów. Formularz bez cytowania działa tylko z wzorami jednopoziomowymi i nie pozwala na używanie notacji lub odwoływanie się do nazw konstruktorów we wzorach.