---------------------------------------------------------------------- -- Your mission, should you choose to accept it, is to complete the -- following module so it type checks with no remaining holes! ---------------------------------------------------------------------- module PS8Idris import Syntax.PreorderReasoning -- Our standard type of length-indexed lists, for use later data ListN : Nat -> Type -> Type where Nil : ListN 0 a (::) : a -> ListN n a -> ListN (S n) a (++) : ListN m a -> ListN n a -> ListN (m + n) a (++) [] ys = ys (++) (x :: xs) ys = x :: (xs ++ ys) ---------------------------------------------------------------------- -- Part 1: Functional programming and equational reasoning -- EXERCISE 1. -- This is a formal version of Exercise 1a from PS 4. mapid : (as : List a) -> map id as = id as -- EXERCISE 2. -- This is a formal version of PS4 1d. lengthApp : (xs, ys : List a) -> length (xs ++ ys) = length xs + length ys -- EXERCISE 3. -- This is a formal version of PS4 1e. -- First, define a variant of ++ in terms of foldr. You should NOT -- need to pattern-match on xs or ys. That is foldr's job! append2 : List a -> List a -> List a -- Now, prove they are equal. appendIsappend2 : (xs, ys : List a) -> xs ++ ys = append2 xs ys ------------------------------------------------------------ -- Part 3: Encoding mathematics via Curry-Howard -- A *monoid* is -- * a set M, together with -- * an associative binary operation M -> M -> M, and -- * a distinguished identity element (e : M). -- -- If you have seen group theory, a monoid is just like a group -- without the requirement of inverses. -- -- We can express the notion of a monoid in the predicate calculus, -- and then encode it in Agda via the Curry-Howard isomorphism. -- A "raw monoid" is the data for a monoid, without the associativity -- and identity laws. Conceptually, a monoid is a triple consisting -- of a type (M : Type), a binary operation (&) : M -> M -> M, and an -- identity element (e : M). Note, however, that the *types* of (&) -- and e depend on the *value* M. So we encode it using a dependent -- pair type. -- -- Note that parentheses around a dependent pair are required syntax. RawMonoid : Type RawMonoid = (M ** (M , M -> M -> M)) infixl 6 & -- Now we encode what it means for some element to be the identity for -- a binary operation. e is the identity for (&) if for all x, both e -- & x = x AND x & e = x. By the Curry-Howard isomorphism, we encode -- this AND by a pair: evidence of e & x = x AND x & e = x consists of -- a evidence for the first equality paired with evidence for the -- second. Note also how we encode "for all x of type A" as a -- function (x : A) -> ... IdentityFor : (A : Type) -> A -> (A -> A -> A) -> Type IdentityFor A e (&) = (x : A) -> ((e & x) = x , (x & e) = x) -- EXERCISE 6. Encode what it means for a binary operation to be -- associative. Associative : (A : Type) -> (A -> A -> A) -> Type -- Finally, IsMonoid defines the evidence that a RawMonoid is in fact -- a real monoid, as a pair of an identity proof and an associativity -- proof. Note how we pattern-match on the RawMonoid to get its type -- A, identity element e, and binary operation &. IsMonoid : RawMonoid -> Type IsMonoid (M ** (e , (&))) = (IdentityFor M e (&) , Associative M (&)) -- Here is an example showing that the natural numbers are a monoid -- under the operation of addition. First we write down the raw monoid. NatSumMonoid : RawMonoid NatSumMonoid = (Nat ** (0 , (+))) -- Finally, we prove that NatSumMonoid is really a monoid. -- -- EXERCISE 7: Complete the proof below. You may find useful the -- standard library lemmas plusZeroRightNeutral and plusAssociative. NatSumIsMonoid : IsMonoid NatSumMonoid -- EXERCISE 8. For any type A, List A is a monoid under list -- concatenation (++). Prove it by filling in the holes below. -- (Note: you may need to state and prove some additional lemmas about -- (++), or go find the necessary lemmas in the standard library: -- https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/List.idr -- ) ListMonoid : (A : Type) -> RawMonoid ListIsMonoid : (A : Type) -> IsMonoid (ListMonoid A) -- EXERCISE 9. The natural numbers are also a monoid under -- multiplication. Prove it by filling in the holes below. (Of -- course all this is already proved in the Idris standard library, -- but it's instructive to work out the details from scratch.) -- -- There are several ways to define multiplication, and in theory any -- one of them can be used. However, this one is provided since it -- tends to make the following proofs go a bit more smoothly. Note -- that, unlike (+), it pattern-matches on its *second* argument. mul : Nat -> Nat -> Nat mul m Z = Z mul m (S n) = m + (m `mul` n) -- First, prove that 1 is the identity element for (*). leftOne : (n : Nat) -> 1 `mul` n = n rightOne : (n : Nat) -> n `mul` 1 = n -- Next, prove that mul is associative. You will probably need the -- lemma mulDistribL in your proof of mulAssoc, though note that you can -- complete them in either order. Idris is perfectly happy to type -- check uses of mulDistribL even if it is not yet defined. -- Hint: to prove mulDistribL and mulAssoc you may find it helpful to -- use the notation for structured equational reasoning. -- Hint 2: pattern match wisely. mulDistribL : (x, y, z : Nat) -> x `mul` (y + z) = (x `mul` y) + (x `mul` z) mulAssoc : (x, y, z : Nat) -> (x `mul` (y `mul` z)) = ((x `mul` y) `mul` z) -- Finally, define and prove the monoid of natural numbers under mul. NatProdMonoid : RawMonoid NatProdIsMonoid : IsMonoid NatProdMonoid