Homework 10: Predicate for Sorted Lists
(a) Define a predicate Sort as an Idris data type that is true for lists of Nats that are sorted.
Hint 1: Your data type definition needs 3 constructors.
Hint 2: You have to reuse the Less data type in the type of one of the constructors.
data Less : Nat -> Nat -> Type where
Suc : Less n (S n)
Trans : Less k n -> Less n m -> Less k m
(b) Express and prove the fact that [3,5] is sorted in Idris.
(c) Express and prove the theorem in Idris that the tail of a sorted list is also sorted.
(d) Express and prove the theorem in Idris that the first element of a sorted list is smaller than its second element.
(e) Express and prove the theorem in Idris that removing the second element form a sorted list yields a sorted list.