タクティクリファレンス: 否定と矛盾

absurd タクティク

absurd term

現在のゴールが何であるかにかかわらず、ゴールを二つのサブゴール term と ~ term に変換する。elimtype False; refine ((_ : ~ term) (_ : term)) に等しい。

Coq < Goal (P -> Q) -> (P -> ~ Q) -> ~ P.
1 subgoal
  
  ============================
   Prop, (P -> Q) -> (P -> ~ Q) -> ~ P

Unnamed_thm < intros H1 H2 H3.
1 subgoal
  
  H1 : P -> Q
  H2 : P -> ~ Q
  H3 : P
  ============================
   False

Unnamed_thm < absurd Q.
2 subgoals
  
  H1 : P -> Q
  H2 : P -> ~ Q
  H3 : P
  ============================
   ~ Q

subgoal 2 is:
 Q

Unnamed_thm < exact (H2 H3).
1 subgoal
  
  H1 : P -> Q
  H2 : P -> ~ Q
  H3 : P
  ============================
   Q

Unnamed_thm < exact (H1 H3).
Proof completed.

contradict タクティク

Coq 8.2 以降で使える。

contradict ident

指定した前提 identとゴールを入れ替える。

前	後
ident : P ⊢ Q	⊢ ~ P
ident : ~ P ⊢ Q	⊢ P
ident : P ⊢ ~ Q	ident : Q ⊢ ~ P
ident : ~ P ⊢ ~ Q	ident : Q ⊢ P

ゴールが ~ P の形をしていない場合は、前提 ident は削除されるので注意。

contradiction タクティク

contradiction

intros の後、前提にある False を使って任意のゴールの証明を完成させる。intros; elimtype False; assumption に同じ。また前提に False そのものがなくて assumption が利かなくても、P と ~ P がある場合は自動的に証明を完成させる。

Coq < Goal P -> ~ P -> 0 = 1.
1 subgoal
  
  ============================
   P -> ~ P -> 0 = 1

Unnamed_thm < contradiction.
Proof completed.

contradiction ident

False を導くために前提 ident を使う。

exfalso タクティク

Coq 8.3 以降で使える。

exfalso

現在のゴールが何であるかにかかわらず、ゴールを False にする。elimtype False に同じ。