Agda 的标准库 Data.AVL.Sets 包含 Data.String 作为值

Question

我想弄清楚如何在 Data.AVL.Sets 模块中使用基于 AVL 树的有限集的 Agda 标准库实现。我能够使用 ℕ 作为以下代码的值成功地做到这一点。

import Data.AVL.Sets
open import Data.Nat.Properties as ℕ
open import Relation.Binary using (module StrictTotalOrder)
open Data.AVL.Sets (StrictTotalOrder.isStrictTotalOrder ℕ.strictTotalOrder)

test = singleton 5

现在我想实现同样的事情，但使用 Data.String 作为值。似乎没有相应的 Data.String.Properties 模块，但 Data.String 导出 strictTotalOrder : StrictTotalOrder _ _ _ 我认为看起来合适。

然而，仅仅严格按照这个假设替换模块是失败的。

import Data.AVL.Sets
open import Data.String as String
open import Relation.Binary using (module StrictTotalOrder)
open Data.AVL.Sets (StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder)

产生错误

.Relation.Binary.List.Pointwise.Rel 
  (StrictTotalOrder._≈_ .Data.Char.strictTotalOrder) (toList x) (toList x₁)
!= x .Relation.Binary.Core.Dummy.≡ x₁ of type Set

when checking that the expression
StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder
has type
Relation.Binary.IsStrictTotalOrder .Relation.Binary.Core.Dummy._≡_
__<__3

我发现很难详细解压，因为我不知道 Core.Dummy 是什么东西。 Strings的全序pointwise定义好像有点问题，我想不通

Answer 1

如果您查看 Data.AVL.Sets，您会发现它由与等价关系 _≡_（在 Relation.Binary.PropositionalEquality 中定义）关联的严格全序参数化：

module Data.AVL.Sets
  {k ℓ} {Key : Set k} {_<_ : Rel Key ℓ}
  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
  where

现在我们可以看看 Strings 上的严格全序是如何定义的。我们首先将 String 转换为 List Char，然后根据列表的严格字典顺序进行比较：

strictTotalOrder =
  On.strictTotalOrder
    (StrictLex.<-strictTotalOrder Char.strictTotalOrder)
    toList

如果我们深入研究 StrictLex.<-strictTotalOrder 的代码，我们可以看到与 Char 的 List 关联的等价关系是使用逐点提升 Pointwise.isEquivalence 无论 Chars 的等价关系是什么。

但是 Pointwise.isEquivalence 是根据此数据类型定义的：

data Rel {a b ℓ} {A : Set a} {B : Set b}
         (_∼_ : REL A B ℓ) : List A → List B → Set (a ⊔ b ⊔ ℓ) where
  []  : Rel _∼_ [] []
  _∷_ : ∀ {x xs y ys} (x∼y : x ∼ y) (xs∼ys : Rel _∼_ xs ys) →
        Rel _∼_ (x ∷ xs) (y ∷ ys)

因此，当 Agda 期望与 _≡_ 关联的严格全序时，我们反而为其提供了与 Rel _ on toList 关联的严格全序，它没有统一的机会。

我们如何从这里继续前进？好吧，您可以在字符串上定义自己的严格总顺序。或者，您可以尝试将当前的转换为 _≡_ 是使用的等价物。这就是我接下来要做的 post。

所以，我想重用具有不同等价关系 R′ 的 IsStrictTotalOrder R O。诀窍是注意如果可以将值从 R a b 传输到 R′ a b 那么，我应该没问题！所以我引入了一个 RawIso A B 的概念，它指出我们总是可以将值从 A 传输到 B，反之亦然：

record RawIso {ℓ : Level} (A B : Set ℓ) : Set ℓ where
  field
    push : A → B
    pull : B → A
open RawIso public

那么我们可以证明RawIsos保留了很多性质：

RawIso-IsEquivalence :
  {ℓ ℓ′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  IsEquivalence R → IsEquivalence R′
RawIso-IsEquivalence = ...

RawIso-Trichotomous :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  Trichotomous R O → Trichotomous R′ O
RawIso-Trichotomous = ...

RawIso-Respects₂ :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  O Respects₂ R → O Respects₂ R′
RawIso-Respects₂ = ...

所有这些引理可以组合起来证明给定一个严格的全序，我们可以通过 RawIso:

构建一个新的

RawIso-IsStrictTotalOrder :
  {ℓ ℓ′ ℓ′′ : Level} {A : Set ℓ} {R R′ : Rel A ℓ′} {O : Rel A ℓ′′} →
  (iso : {a b : A} → RawIso (R a b) (R′ a b)) →
  IsStrictTotalOrder R O → IsStrictTotalOrder R′ O    
RawIso-IsStrictTotalOrder = ...

既然我们知道我们可以沿着这些RawIso传输严格全序，我们只需要证明Data.String中定义的严格全序使用的等价关系在RawIso 命题相等。这（几乎）只是展开定义的问题。唯一的问题是字符的相等性是通过首先将它们转换为自然数然后使用命题相等来定义的。但是 toNat function used has no stated property (compare e.g. to toList and fromList 据说是倒数）！我加入了这个 hack，我认为应该没问题，但如果有人有更好的解决方案，我很想知道！

toNat-injective : {c d : Char} → toNat c ≡ toNat d → c ≡ d
toNat-injective {c} pr with toNat c
toNat-injective refl | ._ = trustMe -- probably unsafe
  where open import Relation.Binary.PropositionalEquality.TrustMe

无论如何，现在你已经有了这个，你可以展开定义并证明：

rawIso : {a b : String} →
         RawIso ((Ptwise.Rel (_≡_ on toNat) on toList) a b) (a ≡ b)
rawIso {a} {b} = record { push = `push ; pull = `pull } where

  `push : {a b : String} → (Ptwise.Rel (_≡_ on toNat) on toList) a b → a ≡ b
  `push {a} {b} pr =
    begin
      a                   ≡⟨ sym (fromList∘toList a) ⟩
      fromList (toList a) ≡⟨ cong fromList (aux pr) ⟩
      fromList (toList b) ≡⟨ fromList∘toList b ⟩
      b
    ∎ where

     aux : {xs ys : List Char} → Ptwise.Rel (_≡_ on toNat) xs ys → xs ≡ ys
     aux = Ptwise.rec (λ {xs} {ys} _ → xs ≡ ys)
           (cong₂ _∷_ ∘ toNat-injective) refl

  `pull : {a b : String} → a ≡ b → (Ptwise.Rel (_≡_ on toNat) on toList) a b
  `pull refl = Ptwise.refl refl

这让您可以

stringSTO : IsStrictTotalOrder _ _
stringSTO = StrictTotalOrder.isStrictTotalOrder String.strictTotalOrder

open Data.AVL.Sets (RawIso-IsStrictTotalOrder rawIso stringSTO)

呸！

我已经上传了一个raw gist，这样你就可以轻松访问代码，查看导入等

Agda 的标准库 Data.AVL.Sets 包含 Data.String 作为值

Agda's standard library Data.AVL.Sets containing Data.String as values

agda