agda - 编码集合(唯一元素列表)的正确方法是什么?
问题描述
在 Agda 中,对集合进行编码的正确方法是什么?即,独特元素的列表?
我试过的:
可以使用我上一个问题中建议的方法之一来做到这一点,即将谓词编码is-set
为List A -> Set
函数,然后使用 Sigma 来制作列表的子集,这些列表也是集合:
open import Data.List
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Product
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
DecEq : (A : Set) -> Set
DecEq A = (a : A) -> (b : A) -> Dec (a ≡ b)
is-in : {A : Set} -> (eq : DecEq A) -> (a : A) -> List A -> Bool
is-in eq v [] = false
is-in eq v (x ∷ xs) with eq v x
is-in eq v (x ∷ xs) | yes p = true
is-in eq v (x ∷ xs) | no ¬p = is-in eq v xs
is-set : {A : Set} -> (eq : DecEq A) -> List A -> Set
is-set eq [] = ⊤
is-set eq (x ∷ xs) with is-in eq x xs
... | false = is-set eq xs
... | true = ⊥
Uniques : (A : Set) -> DecEq A -> Set
Uniques A eq = Σ (List A) (is-set eq)
eq : (a : ℕ) -> (b : ℕ) -> Dec (a ≡ b)
eq zero zero = yes refl
eq zero (suc b) = no (λ ())
eq (suc a) zero = no (λ ())
eq (suc a) (suc b) with eq a b
eq (suc a) (suc b) | yes p = yes (cong suc p)
eq (suc a) (suc b) | no ¬p = no f where
f : suc a ≡ suc b -> ⊥
f refl = ¬p refl
set : Uniques ℕ eq
set = (1 ∷ 2 ∷ 3 ∷ []) , tt
同样,我也可以使用is-in
. 但是这两个想法看起来都相当做作,因为两者仍然依赖于is-in
哪个仍然是一个List A -> Bool
函数。那么,有没有更合适的方法呢?此外,标准(或其他)库中是否提供此类数据结构?
解决方案
推荐阅读
- vba - 抑制错误 3021:Access 中没有当前记录
- javascript - 组件多次渲染 - 多个 fetch 函数
- python - ubuntu 和 fedora 上 crypt.crypt 的不同结果
- oracle - 估计 Oracle 数据库大小
- python - 将字典列表中的 Python 时间戳转换为日期
- node.js - 如何在没有 index.html 的情况下使用 Firebase 托管部署应用程序?
- php - 如何从 HTML 中检索句子以翻译它们并将它们插入回 HTML?
- javascript - JavaScript (ES6):在条件表达式中使用扩展运算符 (?-operator)
- vue.js - VueJS - 限制存储中数据的反应性
- android - 将应用程序安装到 android 设备时出现问题