记录lean4德摩根定律证明

我证出来啦！！！

最近闲来无事又想学学lean4，先从《lean4定理证明》看起，在写第三章的练习题证明德摩根定律的时候我一直没有头绪，因为不知道怎么处理¬，后面直接开挂使用万能的经典逻辑和排中律，硬是列举了p和q的每种可能然后整出来了，但是我一直觉得这样写不太对，而且这里应该不需要使用经典逻辑，以及太不优雅了。

然后刚刚躺在床上刷手机的时候突然想到，第三章前面提过，¬(p ∨ q)的定义是p ∨ q → False，然后我感觉我突然就悟了，突然知道德摩根定律怎么证明了，甚至突然理解了什么是构造主义，然后我马上打开电脑，写下了证明，然后看见前面的勾冒出来，太完美了，果然这才是正确的证明，下面写下我的证明

variable (p q r : Prop)

example: ¬(p ∨ q) ↔ ¬p ∧ ¬q := Iff.intro
  (fun h:p ∨ q → False => show ¬p ∧ ¬q from ⟨fun hp:p => h (Or.inl hp), fun hq:q => h (Or.inr hq)⟩)
  (fun h:(p → False) ∧ (q → False) => show p ∨ q → False from fun hpq:p ∨ q =>
    hpq.elim (fun hp => h.left hp) (fun hq => h.right hq))

完美，所以我喜欢写代码刷题，需要动一点脑子但不多，能有快速且极强的正反馈，让人上头，当然如果刷完之后能让我感觉思维上有提升那就更好了。