coqでドモルガン 命題論理編
命題論理ドモルガン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.
自分でも騙されている感じしかしない。
述語論理版はどうやったらいいのか良くわからん。