In Coq: Umkehrung des Existenzquantors mit mehreren Variablen, mit einem Befehl?

Question

Ich arbeite durch einen Beweis, in dem es eine Hypothese

H : exists a b v, P a b v 

Wenn ich inversion H verwenden, dann rette ich

a : nat 
H1 : exists b v, P a b v. 

was in Ordnung ist, aber dann muss ich Inversion verwenden, noch zweimal zu recover b und v. Gibt es einen einzigen Befehl, um a, b, v auf einmal wiederherzustellen?

Answer 1

Sie eine Liste von Mustern (p1 & ... & pn) für Folge von rechtsassoziativ binären induktiven Konstrukteuren wie conj oder ex_intro verwenden können:

destruct H as (a & b & v & H). 

Ein weiteres schönes Beispiel aus dem Referenzhandbuch: Wenn wir eine Hypothese

haben

H: A /\ (exists x, B /\ C /\ D) 

Dann können wir es zerstören mit

destruct H as (a & x & b & c & d). 

Answer 2

Ja, durch Bindemittel für die Objekte, die Sie wollen, vorstellen, wie diese Angabe:

inversion [a [b [v H']]]. 

Beachten Sie, dass destruct auch hier funktioniert (mit der gleichen Syntax), erzeugt er einen etwas einfacheren Beweis (Generell Das Handbuch warnt vor großen Proofs, die von inversion generiert wurden.