----------------------------------------------------------------------
-- 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