Как правильно кодировать наборы (списки уникальных элементов)? - PullRequest
Новая
       11

Как правильно кодировать наборы (списки уникальных элементов)?

0 голосов
/ 06 сентября 2018

В Agda, как правильно кодировать набор; то есть список уникальных элементов?

Что я пробовал:

Можно сделать это, используя один из предложенных методов на моем последнем вопросе , который должен был бы закодировать предикат is-set как List A -> Set функцию, а затем использовать сигма для создания подмножество списков, которые также являются наборами: 

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 функцией. Таким образом, есть ли более подходящий способ сделать это? Также доступна ли такая структура данных в стандартных (или других) библиотеках?

...