I've been trying to use So
type to implement SortedTwoElems
proof type and function isSortedTwoElems
. I'm not sure how to go about implementing proveUnsortedTwoElems
case.
Here's the full example:
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)
When doing it with:
proveUnsortedTwoElems (MkSortedTwoElems _) impossible
type checker complains with:
proveUnsortedTwoElems (MkSortedTwoElems _) is a valid case