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

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

这里的错误消息应该提示您：So (not (x <= y)) 中使用的 Ord e 约束是 unsortedTwoElems 中的约束，而 MkSortedTwoElems 中使用的约束受其限制。

不能保证这两个 Ord 兼容。

我建议的解决方案：重新定义 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

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

Proving that list has exactly two sorted elements

idris