CS代考计算机代写 Homework 10: Predicate for Sorted Lists

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.