0

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

给定

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

证明命题 D。

（问题取自 The Incredible Proof Machine，第 2 课第 3 题。我实际上正在阅读逻辑与证明，第 4 章，精益中的命题逻辑，但那里的练习较少）

显然，通过两次应用 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)

试试看！

我想我已经做了太多的打包问题然后拆包的饭菜，有人可以告诉我一个更好的方式来表达这个问题吗？

4

1 回答 1

1

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

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))

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

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

此外，在你的证明中使用和时，在解包阶段你解包给定3，并给出5，但从不在你的“展示”证明中使用它们。所以你不需要打开它们，例如

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)
于 2018-02-13T09:58:18.177 回答