In Idris, there are functions `believe_me` and `really_believe_me`, which assert things to the compiler. They're generally only used for FFI code, or for extremely tedious proofs.
If you wanted to prove that a list was sorted, you'd write another datatype:
IsSorted : Ord a => List a -> Type
which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair:
(l : List a ** IsSorted l)
which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!).
The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.
If you wanted to prove that a list was sorted, you'd write another datatype:
which represents the proposition that the input list is sorted. You could encode this by requiring that any new element in the list is either the first element, or less than or equal to the previous element. Then, your sorting function could return a dependent pair: which can be read as the list, accompanied by a proof that it is, in fact, sorted. Since your `IsSorted` type requires that the list is sorted, via construction, you won't be able to supply the output of the function unless your code is correct (or you use `believe_me`!).The compiler doesn't generally come up with counterexamples for you; with this style, if the proof isn't complete, it won't compile.