在Agda中编写依赖类型以保证列表有序的技术求助

我在Agda中定义了Foo记录类型，可通过display foo生成字符串表示来排序。已定义比较Foo的关系<=Foo，其构造器$<=Foo$需要证据(display a) Data.String.Base.<= (display b)，且已证明该关系是DecTotalOrder（fooTotalOrder）。

我想要构建依赖类型强制列表有序，预期类型为Σ[ l ∈ (List Foo) ] (FooSorted.Sorted l)，其中FooSorted.Sorted是通过Data.List.Relation.Unary.Sorted.TotalOrder传入fooTotalOrder得到的。

我需要实现函数fooSorted : (l : List Foo) → (FooSorted.Sorted l)，FooSorted基于Data.List.Relation.Unary.Linked.Linked定义，其中关系R为<=Foo。前两种空列表和单元素列表的情况容易处理，但在多元素列表的情况中，需要获取(x <=Foo y)的证据，而这依赖于(display x) Data.String.Base.<= (display y)的证据。

我尝试的代码中，getProof函数通过decLT的yes分支获取证据，但no分支无法填充，希望实现列表无序则程序不编译的效果，求解决方法。

相关代码片段 #

data Linked (R : Rel A ℓ) : List A → Set (a ⊔ ℓ) where
    []  : Linked R []
    [-] : ∀ {x} → Linked R (x ∷ [])
    _∷_ : ∀ {x y xs} → R x y → Linked R (y ∷ xs) → Linked R (x ∷ y ∷ xs)

fooSorted (x ∷ x₁ ∷ m) =  Linked.∷ ($<=Foo$ (getProof x x₁)) (rectype (x₁ ∷ m))
   where
      getProof : (a : Foo) → (b : Foo) → ((display a) Data.String.Base.<= (display b))
      getProof a b with decLT (display a) (display b)
      ...      | yes P = P
      ...      | no Q = {!  !}

解决方法 #

• 调整函数类型，从源头保证有序性
  你当前的fooSorted试图为任意List Foo生成有序证据，这本身不合理——无序列表确实无法构造对应的证据。正确的做法是定义归纳的已排序列表类型，直接在构建列表时强制有序：

  data SortedFoo : List Foo → Set where
    []  : SortedFoo []
    [-] : ∀ {x} → SortedFoo (x ∷ [])
    _∷_ : ∀ {x y xs} → x <=Foo y → SortedFoo (y ∷ xs) → SortedFoo (x ∷ y ∷ xs)
  

  后续直接使用SortedFoo类型构建列表，从根源避免无序情况。

• 利用DecTotalOrder自带的排序工具
  基于已证明的fooTotalOrder，可以使用Data.List.Sort中的sort函数，它会直接返回带有序证据的列表，无需手动处理比较分支：

  open import Data.List.Sort using (sort)
  open import Data.List.Relation.Unary.Sorted using (Sorted)
  
  sortedFooList : List Foo → Σ[ l ∈ List Foo ] (Sorted fooTotalOrder l)
  sortedFooList l = sort fooTotalOrder l
  

• 给函数添加有序前置条件（不推荐）
  若坚持要从现有列表生成证据，需为函数添加“列表已按字符串顺序排列”的前置条件，再用⊥-elim处理no分支（此时no分支的情况因前置条件不存在矛盾）：

  open import Data.String using (_<=_)
  open import Relation.Nullary using (¬_)
  open import Data.Empty using (⊥-elim)
  open import Data.List.Membership.Propositional using (_∈_)
  
  fooSorted : (l : List Foo) → (∀ x y → x ∈ l → y ∈ l → x 在 y 前 → display x <= display y) → Sorted fooTotalOrder l
  fooSorted [] _ = []
  fooSorted (x ∷ []) _ = [-]
  fooSorted (x ∷ y ∷ xs) ok = 
    Linked.∷ ($<=Foo$ (getProof x y)) (fooSorted (y ∷ xs) ok)
    where
      getProof : (a b : Foo) → display a <= display b
      getProof a b with decLT (display a) (display b)
      ... | yes p = p
      ... | no ¬p = ⊥-elim (¬p (ok a b (here refl) (there here) _))
  

  这种方式代码冗余，不如前两种方案简洁。

内容的提问来源于stack exchange，提问作者mattdf