Lean中如何表示含多个假设的命题逻辑定理？

嘿，作为Lean新手，能提出这个问题说明你已经在认真思考如何把逻辑问题转化为Lean代码啦！我来一步步帮你理清怎么在Lean里表示并证明这个问题。

在Lean里，这类带有多个前提的证明问题，我们可以直接把所有假设作为定理的参数来定义，清晰对应你给出的逻辑前提。针对你的例子，对应的定理定义如下：

theorem prove_D (A B C D : Prop) 
  (hA : A)          -- 前提：A成立
  (hAB : A → B)     -- 前提：A蕴含B
  (hAC : A → C)     -- 前提：A蕴含C
  (hBD : B → D)     -- 前提：B蕴含D
  (hCD : C → D)     -- 前提：C蕴含D
  : D :=             -- 要证明的结论：D
begin
  -- 证明过程写在这里
end

简单解释下：

• A B C D : Prop 先声明这四个符号都是命题类型；
• 后面的hA : A、hAB : A → B等就是你提到的各个前提，每个假设都有一个自定义的名字（比如hA就是“A成立”的假设）；
• 最后的: D明确了我们要推导的结论。

你提到用两次假言推理（modus ponens）就能解决，下面是几种对应的实现方式：

方法一：手动拆解推理步骤（适合理解逻辑） #

我们可以一步步推导，先从前提推出中间结论，再得到最终结果：

theorem prove_D (A B C D : Prop) (hA : A) (hAB : A → B) (hAC : A → C) (hBD : B → D) (hCD : C → D) : D :=
begin
  -- 用hA（A成立）和hAB（A→B）推出B成立，命名为hB
  have hB : B := hAB hA,
  -- 再用hB和hBD（B→D）推出D，直接用exact返回结果
  exact hBD hB,
end

当然也可以从C的路径推导：

theorem prove_D (A B C D : Prop) (hA : A) (hAB : A → B) (hAC : A → C) (hBD : B → D) (hCD : C → D) : D :=
begin
  have hC : C := hAC hA,
  exact hCD hC,
end

方法二：简洁的链式写法 #

Lean支持直接把推理链组合起来，不用定义中间变量，本质和上面的逻辑完全一致：

theorem prove_D (A B C D : Prop) (hA : A) (hAB : A → B) (hAC : A → C) (hBD : B → D) (hCD : C → D) : D :=
hBD (hAB hA)  -- 直接把hAB作用在hA上得到B，再用hBD作用得到D

或者走C的路径：

theorem prove_D (A B C D : Prop) (hA : A) (hAB : A → B) (hAC : A → C) (hBD : B → D) (hCD : C → D) : D :=
hCD (hAC hA)

方法三：自动证明策略（适合快速验证） #

如果只是想验证结论的正确性，也可以用Lean的自动证明tactic，比如tauto!或者finish：

theorem prove_D (A B C D : Prop) (hA : A) (hAB : A → B) (hAC : A → C) (hBD : B → D) (hCD : C → D) : D :=
begin
  tauto!,  -- 自动完成命题逻辑的证明
end

不过作为初学者，还是建议先手动写清楚推理步骤，这样能更好地理解Lean的逻辑推导机制~

你提到《Logic and Proof》第4章练习不多，其实像你现在这样，把《The Incredible Proof Machine》里的问题转化为Lean代码来证明，就是非常好的练习方式！另外，你还可以尝试给同一个证明写几种不同的实现，比如用不同的tactic，或者拆解成更细的步骤，这样能加深对Lean命题逻辑的理解。

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