В Coq: инверсия квантора существования с несколькими переменными с одной командой?

Question

Я работаю через доказательство, в котором существует гипотеза

H : exists a b v, P a b v 

Если я использую inversion H, то я Recover

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

, который прекрасно, но тогда мне нужно использовать инверсию вдвое больше, чтобы восстановить b и v. Есть ли одна команда для восстановления a, b, v одновременно?

Answer 1

Вы можете использовать список шаблонов (p1 & ... & pn) для последовательности правоассоциативных бинарных индуктивных конструкторов, таких как conj или ex_intro:

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

Другого хорошим примером из справочного руководства: если у нас есть гипотеза

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

Тогда мы можем уничтожить его с

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

Answer 2

Да, указав связующие для объектов, которые вы хотите ввести, например:

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

Обратите внимание, что destruct также здесь работает (с тем же синтаксисом), он создает несколько более простое доказательство (В общем, руководство предостерегает от больших доказательств, вызванных inversion).