Coqノウハウ

仮定のexistsをinstantiateする

destruct タクティックの，disj_conj_intro_pattern というのを使う．

例:

H1 : exists x : A, P x
=======

で，destruct H1 as [a H2] とすると

a : A
H2 : P a
=======

となる．同様に，

 H1 : exists x : A, P x /\ Q x
============================

で，destruct H1 as [a [H2 H3]] とすると，

 a : A
 H2 : P a
 H3 : Q a
 ============================

となる．また，

 H1 : exists x : A, P x \/ Q x
 ============================

で，destruct H1 as [a [H2 | H3]]

とすると，2つのゴールができる:

 a : A
 H2 : P a
 ============================

 a : A
 H3 : Q a
 ============================