Fehler bei der Verwendung von Let-Destruct für Tupel in Coq

Question

Ich bin ein neuer Benutzer für Coq. Ich habe einige Funktionen definiert:

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. 

Ich versuche, das Ergebnis von p in eine Tupel-Darstellung zu zerstören. Allerdings beschwert sich Coqc auf q:

Error: Destructing let on this type expects 2 variables. 

während q 'die Kompilierung bestehen kann. Wenn ich p ändere, um ein Paar (a + 1, a + 2) zurückzugeben, funktionieren die entsprechenden q und q 'beide gut.

Warum lässt die Zerstörung nur Paare zu? Oder habe ich irgendeinen Syntaxfehler gemacht? Ich habe mit Coq Handbuch überprüft, aber keine Ahnung gefunden.

Vielen Dank!

Answer 1

Was ist ein bisschen verwirrend in Coq ist, dass es zwei verschiedene Formen der Zerstörung gibt. Die Sie für Bedürfnisse suchen ein Angebot vor dem Muster:

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

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

voranstellen, das Muster mit einem Zitat ermöglicht es Ihnen, in ihnen verschachtelten Mustern und Verwendung benutzerdefinierten Bezeichnungen zu verwenden. Das Formular ohne Anführungszeichen funktioniert nur mit Mustern auf einer Ebene, und Sie können keine Notationen verwenden oder auf Konstruktornamen in Ihren Mustern verweisen.