如何比较 Agda 中的两组？答案

【问题标题】：How to compare two sets in Agda?如何比较 Agda 中的两组？
【发布时间】：2015-06-12 02:03:26
【问题描述】：

我想写一个函数，它以 set 作为输入和return true if it is top and false if it is bottom. 这种方式我试过了。。

isTop : Set → Bool
isTop x = if (x eq ⊤) then true
              else false

但我无法正确定义 eq。我试过了。。

_eq_ : Set → Set → Bool
⊤ eq ⊥ = false

这不起作用，因为当我检查 T eq T it is also returning false.

请帮我写这个 eq 函数或任何其他写 isTop 的方法。

【问题讨论】：

例如，可以定义一个集合，其居民是哥德巴赫猜想的证明。这告诉了你关于isTop 的什么信息？
我不确定如何定义isTop，但⊤ eq ⊤ 返回false 的原因是您无法对Set 类型的内容进行模式匹配。 Agda 将⊤ 和⊥ 解释为普通变量名。与x eq y = false 相同。
@luqui 我不知道如何用该证明定义一个集合。能详细点吗？？
简而言之，这是不可能的。相反，您应该说明您正在努力实现的更广泛的目标。
Universe Set 不是归纳定义的类型，因此您不能对其使用模式匹配。假设您可以使用模式匹配以某种方式定义_eq_。稍后您可以添加自定义类型data Foo : Set where ...，其中Foo 未在_eq_ 的定义中考虑。

标签： haskell functional-programming agda

【解决方案1】：

在 Agda 中是不可能的，但一般是 not senseless。

你可以写一些不是很有意义的东西：

open import Data.Empty
open import Data.Unit
open import Data.Bool

data U : Set where
  bot top : U

⟦_⟧ : U -> Set
⟦ bot ⟧ = ⊥
⟦ top ⟧ = ⊤

record Is {α} {A : Set α} (x : A) : Set where

is : ∀ {α} {A : Set α} -> (x : A) -> Is x
is _ = _

isTop : ∀ {u} -> Is ⟦ u ⟧ -> Bool
isTop {bot} _ = false
isTop {top} _ = true

open import Relation.Binary.PropositionalEquality

test-bot : isTop (is ⊥) ≡ false
test-bot = refl

test-top : isTop (is ⊤) ≡ true
test-top = refl

u 可以从Is ⟦ u ⟧ 推断出来，因为⟦_⟧ 是constructor headed。 Is 是一个单例，因此它允许将值提升到类型级别。你可以找到一个使用here的例子。

【讨论】：

这真的很有帮助。非常感谢。但我的问题仍然没有解决。我想写 if(isTop (is (chkTop))) 并且 chkTop 的定义是chkTop : something -> Set chkTop x = if (x is true) then T else bot. 当我编译这个我得到错误集！= [[ u x y]].
@ajayv，我不明白你的代码，但是，AFAIK，没有办法打破 Agda 中的参数化，所以不可能以某种方式模拟你的 isTop 函数。但是您最初的问题看起来像XY problem。为什么需要这个isTop？
其实这是我的根本问题。如果这个问题得到解决，我不需要 isTop 函数。请看stackoverflow.com/questions/30817693/…
@ajayv，你对isCut 的定义对我来说看起来不错（我宁愿使用Data.Bool.Base 中的T，但这是一个小问题）。您不需要isTop 函数——您需要在每个函数中使用with 对这个大表达式((((p mem (getLC x)) ... 进行模式匹配，利用isCut 属性，并以不同方式处理false 和true 情况.
@ajayv, "Is it possible to write isCut : cut -> Bool" — 不，因为isCut 的定义包含量化。请尽量减少您的问题并使问题自成一体，否则很难为您提供帮助。