> module Exercises12 One of the main advantages of dependently-typed programming languages is that, since they are able to express arbitrarily complex logical properties, we can use them to write the specifications of our programs, not just the programs themselves. We do not need a separate language or tool for stating what our programs should do, as we would if using, for example, Z (see http://www.usingz.com/). Moreover, the proofs that our programs satisfy these specifications are themselves written in the same language, and they are actually automatically verified by the type checker. In the following exercises, we explore this theme, using the simple case study of a function that computes the minimum of two natural numbers. Exercise 1: Introducing |LE| ---------------------------- In logic, new relations can be added to a language by stating the axioms that govern their use, in a way similar to the introduction of |Id| (or |=|). As an example, consider the relation ``less than or equal'' |LE| on natural numbers (we use |LE| instead of the usual |<=| in order to avoid confusion with the boolean-valued function). Here are the introduction rules for |LE|: n : Nat LE m n ----------- LE_IO ---------------- LE_IS LE O n LE (S m) (S n) The rule |LE_IO| states that we can infer that |O| is less than or equal to |n| for any natural number |n|. The second expresses the monotonicity of |S|. Define an Idris type that corresponds to the |LE| relation, by filling in the following data declaration: > data LE : Nat -> Nat -> Type where > LE_IO : --- > LE_IS : --- Exercise 2: Properties of |LE| ------------------------------ |LE| is an order relation, that is, it is reflexive, antisymmetric, and transitive. Reflexivity is expressed as < Forall n : Nat (LE n n) In Idris, this becomes > refl_LE : (n : Nat) -> LE n n Prove this by implementing |refl_LE|. Antisymmetry is expressed as < Forall n1, n2 : Nat (LE n1 n2 & LE n2 n1 -> n1 = n2) and transitivity is expressed as < Forall n1, n2, n3: Nat (LE n1 n2 & LE n2 n3 -> LE n1 n3) Translate these properties to Idris. (Warning: proving them can be quite tricky! I'm only asking you to state them!) Exercise 3: Specifiying |inf| ------------------------------ The minimum of two natural numbers |n1|, |n2| is the largest natural number which is smaller than the two numbers (I use ``smaller'' for ``less than or equal to''). That is 1. it is smaller than the two numbers 2. any other number which is also smaller than the two numbers is smaller than the minimum. Writing |inf n1 n2| for the minimum of |n1| and |n2|, the first property can be expressed as < infProp1 : (n1: Nat) -> (n2 : Nat) -> < (LE (inf n1 n2) n1, LE (inf n1 n2) n2) Express the second property, |infProp2|. Exercise 4: Implementing |inf| ------------------------------ Consider the following implementation of |inf| > inf : Nat -> Nat -> Nat > inf O n = O > inf (S n1) O = O > inf (S n1) (S n2) = S (inf n1 n2) Prove that |inf| satisfies the first property by implementing |infProp1|. > infProp1 : (n1: Nat) -> (n2 : Nat) -> > (LE (inf n1 n2) n1, LE (inf n1 n2) n2)