在agda中编写依赖类型以保证列表已排序

Question

我有一个记录类型，在 Agda 中调用 if Foo。我可以通过生成字符串表示形式（显示 foo）并对结果字符串进行排序来对其进行排序。我有一个关系，称之为

<=Foo

，用于比较 Foo 记录，它有一个构造函数

$<=Foo$

，它获取证据

((display a) Data.String.Base.<= (display b))

a

的字符串是 LT

b

的字符串。我已经证明它是 DecTotalOrder，产生 fooTotalOrder

我现在想创建一个依赖类型，强制列表按排序顺序排列。看来应该是这样

Σ[ l ∈ (List Foo) ] (FooSorted.Sorted l)

其中

FooSorted.Sorted

来自通过

fooTotalOrder

到

Data.List.Relation.Unary.Sorted.TotalOrder

。

据我了解，为了使这项工作正常进行，我需要一个函数，比如说

fooSorted : (l : List Foo) -> (FooSorted.Sorted l)

FooSorted 派生自 Data.List.Relation.Unary.Linked.Linked，其定义为

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)

这里，R 是

<=Foo

。

在我看来 fooSorted 需要返回

Linked <=Foo l

，其中 l 是 List Foo 参数。

前两种情况很简单，但我无法弄清楚最后一种情况。我需要使用证据来证明

(x <=Foo y)

。我有这个构造函数，但它需要证据证明

((display x) Data.String.Base.≤ (display x))

并且我不知道从哪里得到它。

我不能简单地输入它 - 它不会编译。从我可以获得类似类型的各种方法中，最接近的是使用全序，但它返回一个总和类型，我不知道如何从中获取一个值。

我试图使用

isEven

来模仿的示例，如果在需要偶数的地方使用奇数，则无法编译。我正在寻找相同的列表 - 如果列表未排序，程序不应编译 - 但我确实希望编译我的依赖类型。

我完全有可能走错了方向。如有任何帮助，我们将不胜感激！

我最接近的是以下：

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 = {!  !}

yes

分支中的P正是我想要的，但是另一个孔中该放什么？目的是证明证明失败。

Answer 1

感谢您的建议，对于延迟回复表示抱歉。最后，我无法利用 Naïm 建议的方法，该方法适用于严格静态的实例。最后我需要遵循最后一个建议 - 这本质上涉及重新发明冒泡排序。这样我最终会得到列表开头的项目（假设是 a）并使用 Linked 中的第二个构造函数。

然后我会得到列表中的下一个（比如 b）并检查 b <= a getting b :: a :: [], or create a new list a :: b :: [].

然后，当添加每个附加项目时，我可以在添加到列表或递归排序到现有列表之前将其与前一个项目进行检查。因此，如果给定一个排序列表，则在 O(n) 时间内返回一个依赖类型的排序列表，否则可以是 O(n^2)

幸运的是，一旦列表排序完毕，我想做的所有其他操作都可以维持顺序。