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.   
   

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

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