PROSAGA码农传奇-精益-在精益（命题逻辑）中表示具有多个假设的定理

<div class =“post-text”itemprop =“text”>
  <P>
    我认为通过在假设中使用And并使用 - ＆gt;来更清楚。这里有2个等效的样张，我更喜欢第一个
  </p>
   <pre>
    <code>
      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))

</code>
  </pre>
  <P>
    除了使用示例之外，第二个与第一个相同，
我相信你必须使用assume来指定参数的名称
而不是在声明中
  </p>
   <pre>
    <code>
      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))

</code>
  </pre>
  <P>
    如果你想使用def语法，但问题是例如使用示例语法指定
  </p>
   <pre>
    <code>
      example : A -> (A -> B) -> (A -> C)
            -> (B -> D) -> (C -> D) -> D := s2p3

</code>
  </pre>
  <P>
    此外，在使用和在您的证明中，在拆包阶段
你解包给定3，并给出5但从未在你的“show”证明中使用它们。
所以你不需要打开它们，例如
  </p>
   <pre>
    <code>
      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)

</code>
  </pre>
</DIV>