Agda中使用标准库的对/列表的字典排序

Question

Agda标准库包含一些模块Relation.Binary.*.(Non)StrictLex(目前仅用于Product和List).我们可以使用这些模块轻松构造例如IsStrictTotalOrder自然数对(即? × ?)的实例.

open import Data.Nat as ? using (?; _<_)
open import Data.Nat.Properties as ?
open import Relation.Binary using (module StrictTotalOrder; IsStrictTotalOrder)
open import Relation.Binary.PropositionalEquality using (_?_)
open import Relation.Binary.Product.StrictLex using (×-Lex; _×-isStrictTotalOrder_)
open import Relation.Binary.Product.Pointwise using (_×-Rel_)

?-isSTO : IsStrictTotalOrder _?_ _<_
?-isSTO = StrictTotalOrder.isStrictTotalOrder ?.strictTotalOrder

?×?-isSTO : IsStrictTotalOrder (_?_ ×-Rel _?_) (×-Lex _?_ _<_ _<_)
?×?-isSTO = ?-isSTO ×-isStrictTotalOrder ?-isSTO

这将使用逐点相等创建实例_?_ ×-Rel _?_.在命题相等的情况下,这应该是等同于使用只是命题的平等.

是否有一种简单的方法可以IsStrictTotalOrder _?_ (×-Lex _?_ _<_ _<_)使用正常的命题相等将上面的实例转换为类型的实例？

Answer 1

所需的套件并不难组装：

\n\n

open import Data.Product\nopen import Function using (_\xe2\x88\x98_; case_of_)\nopen import Relation.Binary\n\n_\xe2\x87\x94\xe2\x82\x82_ : \xe2\x88\x80 {a \xe2\x84\x93\xe2\x82\x81 \xe2\x84\x93\xe2\x82\x82} {A : Set a} \xe2\x86\x92 Rel A \xe2\x84\x93\xe2\x82\x81 \xe2\x86\x92 Rel A \xe2\x84\x93\xe2\x82\x82 \xe2\x86\x92 Set _\n_\xe2\x89\x88_ \xe2\x87\x94\xe2\x82\x82 _\xe2\x89\x88\xe2\x80\xb2_ = (\xe2\x88\x80 {x y} \xe2\x86\x92 x \xe2\x89\x88 y \xe2\x86\x92 x \xe2\x89\x88\xe2\x80\xb2 y) \xc3\x97 (\xe2\x88\x80 {x y} \xe2\x86\x92 x \xe2\x89\x88\xe2\x80\xb2 y \xe2\x86\x92 x \xe2\x89\x88 y)\n\n-- I was unable to write this nicely using Data.Product.map... \n-- hence it is moved here to a toplevel where it can pattern-match\n-- on the product of proofs\ntransform-resp : \xe2\x88\x80 {a \xe2\x84\x93\xe2\x82\x81 \xe2\x84\x93\xe2\x82\x82 \xe2\x84\x93} {A : Set a} {\xe2\x89\x88 : Rel A \xe2\x84\x93\xe2\x82\x81} {\xe2\x89\x88\xe2\x80\xb2 : Rel A \xe2\x84\x93\xe2\x82\x82} {< : Rel A \xe2\x84\x93} \xe2\x86\x92\n                 \xe2\x89\x88 \xe2\x87\x94\xe2\x82\x82 \xe2\x89\x88\xe2\x80\xb2 \xe2\x86\x92\n                 < Respects\xe2\x82\x82 \xe2\x89\x88 \xe2\x86\x92 < Respects\xe2\x82\x82 \xe2\x89\x88\xe2\x80\xb2\ntransform-resp (to ,  from) = \xce\xbb { (resp\xe2\x82\x81 , resp\xe2\x82\x82) \xe2\x86\x92 (resp\xe2\x82\x81 \xe2\x88\x98 from , resp\xe2\x82\x82 \xe2\x88\x98 from) }\n\ntransform-isSTO : \xe2\x88\x80 {a \xe2\x84\x93\xe2\x82\x81 \xe2\x84\x93\xe2\x82\x82 \xe2\x84\x93} {A : Set a} {\xe2\x89\x88 : Rel A \xe2\x84\x93\xe2\x82\x81} {\xe2\x89\x88\xe2\x80\xb2 : Rel A \xe2\x84\x93\xe2\x82\x82} {< : Rel A \xe2\x84\x93} \xe2\x86\x92\n                  \xe2\x89\x88 \xe2\x87\x94\xe2\x82\x82 \xe2\x89\x88\xe2\x80\xb2 \xe2\x86\x92\n                  IsStrictTotalOrder \xe2\x89\x88 < \xe2\x86\x92 IsStrictTotalOrder \xe2\x89\x88\xe2\x80\xb2 <\ntransform-isSTO {\xe2\x89\x88\xe2\x80\xb2 = \xe2\x89\x88\xe2\x80\xb2} {< = <} (to , from) isSTO = record\n  { isEquivalence = let open IsEquivalence (IsStrictTotalOrder.isEquivalence isSTO)\n                    in record { refl = to refl\n                              ; sym = to \xe2\x88\x98 sym \xe2\x88\x98 from\n                              ; trans = \xce\xbb x y \xe2\x86\x92 to (trans (from x) (from y))\n                              }\n  ; trans = IsStrictTotalOrder.trans isSTO\n  ; compare = compare\n  ; <-resp-\xe2\x89\x88 = transform-resp (to , from) (IsStrictTotalOrder.<-resp-\xe2\x89\x88 isSTO)\n  }\n  where\n    compare : Trichotomous \xe2\x89\x88\xe2\x80\xb2 <\n    compare x y with IsStrictTotalOrder.compare isSTO x y\n    compare x y | tri< a \xc2\xacb \xc2\xacc = tri< a (\xc2\xacb \xe2\x88\x98 from) \xc2\xacc\n    compare x y | tri\xe2\x89\x88 \xc2\xaca b \xc2\xacc = tri\xe2\x89\x88 \xc2\xaca (to b) \xc2\xacc\n    compare x y | tri> \xc2\xaca \xc2\xacb c = tri> \xc2\xaca (\xc2\xacb \xe2\x88\x98 from) c\n

\n\n

然后我们可以用它来解决你原来的问题：

\n\n

\xe2\x84\x95\xc3\x97\xe2\x84\x95-isSTO\xe2\x80\xb2 : IsStrictTotalOrder _\xe2\x89\xa1_ (\xc3\x97-Lex _\xe2\x89\xa1_ _<_ _<_)\n\xe2\x84\x95\xc3\x97\xe2\x84\x95-isSTO\xe2\x80\xb2 = transform-isSTO (to , from) \xe2\x84\x95\xc3\x97\xe2\x84\x95-isSTO\n  where\n    open import Function using (_\xe2\x9f\xa8_\xe2\x9f\xa9_)\n    open import Relation.Binary.PropositionalEquality\n\n    to : \xe2\x88\x80 {a b} {A : Set a} {B : Set b}\n         {x x\xe2\x80\xb2 : A} {y y\xe2\x80\xb2 : B} \xe2\x86\x92 (x , y) \xe2\x9f\xa8 _\xe2\x89\xa1_ \xc3\x97-Rel _\xe2\x89\xa1_ \xe2\x9f\xa9 (x\xe2\x80\xb2 , y\xe2\x80\xb2) \xe2\x86\x92 (x , y) \xe2\x89\xa1 (x\xe2\x80\xb2 , y\xe2\x80\xb2)\n    to (refl , refl) = refl\n\n    from : \xe2\x88\x80 {a b} {A : Set a} {B : Set b}\n           {x x\xe2\x80\xb2 : A} {y y\xe2\x80\xb2 : B} \xe2\x86\x92 (x , y) \xe2\x89\xa1 (x\xe2\x80\xb2 , y\xe2\x80\xb2) \xe2\x86\x92 (x , y) \xe2\x9f\xa8 _\xe2\x89\xa1_ \xc3\x97-Rel _\xe2\x89\xa1_ \xe2\x9f\xa9 (x\xe2\x80\xb2 , y\xe2\x80\xb2)\n    from refl = refl , refl\n

\n