Lean4中¬(p∨q)↔¬p∧¬q证明报错：期望函数却得False

问题背景 #

尝试证明《Lean4定理证明》第三章中的德摩根定律¬(p∨q)↔¬p∧¬q的双向推导，但两段代码均报相同错误：function expected at xxx, term has type False，报错位置恰好是需要证明False的地方，现分析错误原因并给出修正方案。

错误代码 #

theorem negAndOr_Fwd : ¬(p ∨ q) → ¬p ∧ ¬q :=
   λ h: ¬(p ∨ q) => 
      And.intro
        λ hp:p =>
          have hpq:(p ∨ q) := Or.inl hp
          show False from h hpq   -- 此处逻辑正确
        λ hq:q =>     -- 错误提示："function expected at h hpq term has type False"
          have hpq:(p ∨ q) := Or.inr hq
          show False from hpq h


theorem negAndOr_Bwd : ¬p ∧ ¬q → ¬(p ∨ q) :=
  λ h: (¬p ∧ ¬q) =>
    have hnp:¬p := And.left h
    have hnq:¬q := And.right h
    λ hpq: (p ∨ q) =>    -- 通过证明OR的两边都导出False来证明¬(p∨q)
      hpq.elim           -- 消除OR
        λ hp:p =>
          show False from hnp hp  -- 此处报错
        λ hq:q => 
          show False from hnq hq

错误原因 #

• negAndOr_Fwd的核心错误：第二个分支里的hpq h参数顺序完全搞反了。h的类型是¬(p∨q)，本质是个函数——它接收一个p∨q类型的参数，就能返回False。而hpq正好是p∨q类型的项，所以正确的调用方式是h hpq，让h去处理hpq。你写成hpq h，相当于让一个非函数类型的hpq去接收参数h，Lean自然会报错说“需要函数，但得到的是False类型”。
• negAndOr_Bwd的报错说明：这段代码里的hnp hp和hnq hq逻辑本身是对的——hnp是¬p（即p→False的函数），传入hp（p类型）就能得到False。如果这里仍报错，大概率是输入时的笔误（比如参数顺序写反），或者Lean环境的临时问题，检查下代码拼写即可。

修正后的代码 #

theorem negAndOr_Fwd : ¬(p ∨ q) → ¬p ∧ ¬q :=
   λ h: ¬(p ∨ q) => 
      And.intro
        λ hp:p =>
          have hpq:(p ∨ q) := Or.inl hp
          show False from h hpq
        λ hq:q =>
          have hpq:(p ∨ q) := Or.inr hq
          show False from h hpq  -- 修正参数顺序


theorem negAndOr_Bwd : ¬p ∧ ¬q → ¬(p ∨ q) :=
  λ h: (¬p ∧ ¬q) =>
    have hnp:¬p := And.left h
    have hnq:¬q := And.right h
    λ hpq: (p ∨ q) =>
      hpq.elim
        λ hp:p =>
          show False from hnp hp
        λ hq:q => 
          show False from hnq hq

内容的提问来源于stack exchange，提问作者Igott