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

Question

我试图弄清楚如何在模块中使用基于AVL树的Agda标准库实现有限集Data.AVL.Sets.我能够成功地使用?以下代码作为值.

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东西是什么,我觉得很难详细解开.似乎字符串总顺序的逐点定义存在一些问题,但我无法弄明白.

Answer 1

如果你看一下Data.AVL.Sets,你可以看到它是由与等价关系_?_(定义在Relation.Binary.PropositionalEquality)相关联的严格总顺序参数化的:

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

现在我们可以看一下如何String定义s 的严格总顺序.我们首先将Strings 转换为List Chars,然后根据列表的严格词典排序对它们进行比较:

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

如果我们深入研究代码StrictLex.<-strictTotalOrder,我们可以看到List与Chars 相关联的等价关系是使用逐点解除s Pointwise.isEquivalence的等价关系来构建Char的.

但是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无法统一.

我们如何从这里继续前进？那么,您可以在字符串上定义自己的严格总订单.或者,您可以尝试将当前的一个转换_?_为使用等效的一个.这是我将在本文的其余部分中做的事情.

所以,我想重用IsStrictTotalOrder R O具有不同等价关系的a R?.诀窍是要注意,如果可以传输值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 = ...

现在,我们知道我们可以沿着这些严格的运输订单总量RawIsoS,我们只需要证明,在规定的严格的总订单中使用的等价关系Data.String是RawIso与命题平等.它(几乎)只是展开定义的问题.唯一的问题是字符的相等性是通过首先将它们转换为自然数然后使用命题相等来定义的.但是所使用的toNat函数没有声明的属性(例如比较toList和fromList声明反转)!我投入了这个黑客,我觉得它应该没问题,但如果有人有更好的解决方案,我很想知道它!

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)

唷!

我上传了一个原始要点,以便您可以轻松访问代码,查看导入等.