Idris 中的复杂量词？

Posted 2023-03-28

【中文标题】Idris 中的复杂量词？

【英文标题】：Complex quantifiers in Idris?

【发布时间】：2021-03-17 15:29:34

【问题描述】：

现在我知道了，可以通过依赖类型来表达量词。所以我为此写了一个简单的实现“for all (a, b: N): exists (c: N): c = a + b”：

f : (a : Nat) -> (b : Nat) -> (c : Nat ** c = a + b)
f a b = (a + b ** Refl)

它有效。

现在我想知道，我可以表达这个“for all (a, b: N): exists (c: N): c > a and c

【参考方案1】：

对于Nat 比较，您可以使用Data.Nat's GT（大于）、GTE（大于）、LT（小于）、LTE（小于）。所以GT c a 和LT c b 对应c > a 和c < b。

对于and，您可以将两个证明放入一个元组：(GT c a, LT c b)。例如，如果您想or 他们，您可以使用Either (GT c a) (LT c b)。

因此：

import Data.Nat

f : (a, b : Nat) -> (c : Nat ** (GT c a, LT c b))

（然而，这个确切的例子是行不通的，因为你不能定义f，因为没有c所以c > 5 and c < 5。）