在 Lean 中表示具有多个假设的定理（命题逻辑）

Question

真正的初学者在这里提问。我如何用精益中的多个假设来表示一个问题？例如：

给定

一个
A→B
A→C
B→D
C→D

证明命题D.

（问题取自 Incredible Proof Machine, Session 2 problem 3. I was actually reading Logic and Proof, Chapter 4, Propositional Logic in Lean 但那里的练习较少）

显然，通过两次应用 modus ponens 来证明这是完全微不足道的，我的问题是我首先如何表示问题？！这是我的证明：

variables A B C D : Prop

example : (( A    )
    /\     ( A->B )
    /\     ( A->C )
    /\     ( B->D )
    /\     ( C->D ))
-> D :=
assume h,
have given1: A, from and.left h,
have given2: A -> B, from and.left (and.right h),
have given3: A -> C, from and.left (and.right (and.right h)),
have given4: B -> D, from and.left (and.right (and.right (and.right h))),
have given5: C -> D, from and.right (and.right (and.right (and.right h))),
show D, from given4 (given2 given1)

Try it!

我想我把问题打包然后解包已经吃得太饱了，有人能告诉我一个更好的方法来表示这个问题吗？

Answer 1

我认为在假设中不使用 And 而使用 -> 会更清楚。这里有两个等价的证明，我更喜欢第一个

def s2p3 {A B C D : Prop} (ha : A)
      (hab : A -> B) (hac : A -> C)
      (hbd : B -> D) (hcd : C -> D) : D
  := show D, from (hbd (hab ha))

第二个与第一个相同，除了使用示例，我相信您必须使用 assume 指定参数的名称而不是在声明中

example : A -> (A -> B) -> (A -> C) -> (B -> D) -> (C -> D) -> D :=
assume ha : A,
assume hab : A -> B,
assume hac, -- You can actually just leave the types off the above 2
assume hbd, 
assume hcd,
show D, from (hbd (hab ha))

如果您想使用 def 语法但问题是例如使用示例语法指定

example : A -> (A -> B) -> (A -> C)
            -> (B -> D) -> (C -> D) -> D := s2p3

另外，在你的proof中使用and的时候，在解包阶段你解包给定 3，给定 5，但从不在你的 "show" 证明中使用它们。所以你不需要解压它们，例如

example : (( A    )
    /\     ( A->B )
    /\     ( A->C )
    /\     ( B->D )
    /\     ( C->D ))
-> D :=
assume h,
have given1: A, from and.left h,
have given2: A -> B, from and.left (and.right h),
have given4: B -> D, from and.left (and.right (and.right (and.right h))),
show D, from given4 (given2 given1)

在 Lean 中表示具有多个假设的定理（命题逻辑）

Representing a theorem with multiple hypotheses in Lean (propositional logic)

lean