证明该列表恰好有两个已排序的元素

Question

我一直在尝试使用So类型来实现SortedTwoElems证明类型和函数isSortedTwoElems。我不确定如何实施proveUnsortedTwoElems案例。

这是完整的例子：

import Data.So

data SortedTwoElems : List e -> Type where
  MkSortedTwoElems : Ord e => {x : e} -> {y : e} -> (prf : So (x <= y))-> SortedTwoElems [x, y]

proveUnsortedTwoElems : Ord e => {x : e} -> {y : e} -> So (not (x <= y)) -> SortedTwoElems [x, y] -> Void
proveUnsortedTwoElems = ?how_to_implement_this

isSortedTwoElems : Ord e => {x : e} -> {y : e} -> (xs : List e) -> Dec (SortedTwoElems xs)
isSortedTwoElems []                      = No (\(MkSortedTwoElems _)  impossible)
isSortedTwoElems (x :: [])               = No (\(MkSortedTwoElems _)  impossible)
isSortedTwoElems (x :: (y :: (z :: xs))) = No (\(MkSortedTwoElems _)  impossible)
isSortedTwoElems (x :: (y :: [])) =
  case choose (x <= y) of
    (Left prf) => Yes (MkSortedTwoElems prf)
    (Right prfNot) => No (proveUnsortedTwoElems prfNot)

这样做时：

proveUnsortedTwoElems (MkSortedTwoElems _) impossible

类型检查器抱怨：

proveUnsortedTwoElems (MkSortedTwoElems _) is a valid case

Answer 1

我从一个中间引理开始，当你发现两个相互矛盾的Sos时，它应该允许结束：

soNotTrue : So b -> So (not b) -> Void
soNotTrue {b = True}  prf prf' = absurd prf'
soNotTrue {b = False} prf prf' = absurd prf

然后你可以尝试写：

unsortedTwoElems : Ord e => So (not (x <= y)) -> SortedTwoElems [x, y] -> Void
unsortedTwoElems prf (MkSortedTwoElems prf') = soNotTrue prf' prf

在这里，错误信息应该让你知道：在Ord e中使用的So (not (x <= y))约束是在unsortedTwoElems中绑定的那个，而在MkSortedTwoElems中使用的约束是由它限制的。

无法保证这两个Ords兼容。

我建议的解决方案：重新定义SortedTwoElems，以便明确它正在使用的Ord。

import Data.So

data SortedTwoElems : Ord e -> List e -> Type where
  MkSortedTwoElems : {o : Ord e} -> So (x <= y) -> SortedTwoElems o [x, y]

soNotTrue : So b -> So (not b) -> Void
soNotTrue {b = True}  prf prf' = absurd prf'
soNotTrue {b = False} prf prf' = absurd prf

unsortedTwoElems : (o : Ord e) => So (not (x <= y)) -> SortedTwoElems o [x, y] -> Void
unsortedTwoElems prf (MkSortedTwoElems prf') = soNotTrue prf' prf