我认为通过在假设中使用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))
</code>
除了使用示例之外,第二个与第一个相同,
我相信你必须使用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))
</code>
如果你想使用def语法,但问题是例如使用示例语法指定
example : A -> (A -> B) -> (A -> C)
-> (B -> D) -> (C -> D) -> D := s2p3
</code>
此外,在使用和在您的证明中,在拆包阶段
你解包给定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)
</code>