Hatena::ブログ(Diary)

memo

2018-05-06

coqでドモルガン 命題論理編

23:27

命題論理ドモルガン4兄弟

¬(A ∨ B) → ¬A ∧ ¬B.

¬A ∧ ¬B → ¬(A ∨ B).

¬A ∨ ¬B → ¬(A ∧ B).

¬(A ∧ B) → ¬A ∨ ¬B.

のうち、直観主義論理の範囲で証明出来ないらしい

¬(A ∧ B) → ¬A ∨ ¬B.の証明。

排中律を前提とする。

排中律を使って、A∨¬AとB∨¬Bをコンテキストに加えて、場合分け。

AかつBのときだけ、¬(A ∧ B) の前提が使われる。

ssreflectの本を読み始めたので、SSReflectのスタイルで。

Hypothesis ExMidLaw : forall P : Prop, P \/ ~P.
Lemma Demorgan1_1 (A B : Prop) :  ~(A /\ B) -> ~A \/ ~B.
Proof.
  move: (ExMidLaw A) => HAnA.
  move: (ExMidLaw B) => HBnB.
  case: HBnB.
  -case:HAnA. 
   +move => HA HB HnAB. case: HnAB.  by [].
   +move => HnA HB HnAB. apply: or_introl HnA.
  -move => HnB HnAB. apply: or_intror HnB.
Qed.   
   

自分でも騙されている感じしかしない。

述語論理版はどうやったらいいのか良くわからん。

トラックバック - http://d.hatena.ne.jp/morita_non/20180506/1525616864