FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

08.05
Tue
ここのページを参考にCoqでドモルガンの法則を証明していたときのメモです.
証明したいのはです。
おおまかな方針としては、まず含意の式なので前件を仮定して後件をひねり出せばいいだけです。

apply conjで連言を分けて別々に証明すればいいようにします.
or_introl,or_introlはそのまま選言の導入の推論規則みたいな感じです.

以下Coqのコード

Lemma de_morgan3 :
forall (A B : Prop) , ~(A \/ B) -> (~A /\ ~B).
Proof.
unfold not. (* ~はシンタックスシュガー *)
intros. (* 含意の前件を仮定する *)
apply conj. (* ∧の命題を証明したい.つまり 左と右を別個に証明すればいい *)
intros. (* 含意の前件を仮定する*)
apply H. (* Falseを得たい *)
apply or_introl. (* 論理和の導入は左か右が証明できればいい.左のAが仮定にある *)
exact H0.
(* 以下同様にして証明する *)
intros.
apply H.
apply or_intror.
exact H0.
Qed.

いくらか分かりやすさが増すので自然演繹の証明図もはっておきます。

Screenshot from 2014-08-05 01:55:00


スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/191-e35bfe04
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。