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
  ============================

{{e #124}}
{{e #42}}

{{e #42}}

で，destruct H1 as [a [H2 {{e #124}} H3]]

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

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

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