-- Homework 1b. Due February 1.
-- 
-- MATH 4680/4681/5680, Winter 2021
--
-- Note: this is the second part of Homework 1.
--
-- The goal of this homework is to prove the commutativity of
-- multiplication of natural numbers.
--
-- Complete the following file by filling in the "holes". There are 13
-- holes, and each of them is a homework problem. Some holes can't be
-- filled until you have completed earlier ones.

open import Equality

-- ----------------------------------------------------------------------
-- * The natural numbers

-- The set of natural numbers, defined as an inductive datatype.
data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

-- ----------------------------------------------------------------------
-- ** Addition

add : ℕ -> ℕ -> ℕ
add zero m = m
add (succ n) m = succ (add n m)

-- A lemma about addition.
-- 
-- The proof uses 'context', which takes two arguments: a function
-- f : A -> B, and a proof that x == y.  It produces a proof of
-- f x == f y.
--
-- Also note that the proof uses the induction hypothesis, by
-- recursively calling 'lemma-add-zero' with the smaller number n.
lemma-add-zero : ∀ (n : ℕ) -> add n zero == n
lemma-add-zero zero = refl
lemma-add-zero (succ n) = context succ (lemma-add-zero n)

-- Another lemma about addition.
lemma-add-succ : ∀ (n m : ℕ) -> add n (succ m) == succ (add n m)
lemma-add-succ zero m = refl
lemma-add-succ (succ n) m = context succ (lemma-add-succ n m)

-- A theorem stating that addition is commutative. The proof
-- uses 'trans', which is transitivity (of equality).
-- Given a proof p : x == y and another proof q : y == z,
-- trans p q is a proof of x == z.
theorem-add-commutative : ∀ (n m : ℕ) -> add n m == add m n
theorem-add-commutative n zero = lemma-add-zero n
theorem-add-commutative n (succ m) = trans step1 step2
  where
    step1 : add n (succ m) == succ (add n m)
    step1 = lemma-add-succ n m

    step2 : succ (add n m) == succ (add m n)
    step2 = context succ (theorem-add-commutative n m)

-- Prove the associativity of addition. Hint: do a case distinction on
-- x.
lemma-add-assoc : ∀ (x y z : ℕ) -> add (add x y) z == add x (add y z)
lemma-add-assoc zero y z = refl
lemma-add-assoc (succ x) y z = context succ (lemma-add-assoc x y z)

-- Here is another lemma about addition. It basically uses
-- lemma-add-succ, theorem-add-commutative, and symmetry of equality.
-- To understand what 'symm' does, put your cursor in the hole in step
-- 3 and type C-c C-, to see what the "type" of the hole is.
lemma3 : ∀ (n m : ℕ) ->  add n (succ m) == add m (succ n)
lemma3 n m = trans step1 (trans step2 step3)
  where
    step1 : add n (succ m) == succ (add n m)
    step1 = lemma-add-succ n m

    step2 : succ (add n m) == succ (add m n)
    step2 = context succ (theorem-add-commutative n m)

    step3 : succ (add m n) == add m (succ n)
    step3 = symm (lemma-add-succ m n)

-- ----------------------------------------------------------------------
-- ** Multiplication

-- The multiplication function. Fill in the missing case.
mult : ℕ -> ℕ -> ℕ
mult zero m = zero
mult (succ n) m = add (mult n m) m

-- Using your definition, prove the following lemmas.

-- Hint: do a case distinction on n. Use the induction hypothesis. You
-- probably also have to use transitivity.
lemma-mult-zero : ∀ (n : ℕ) -> mult n zero == zero
lemma-mult-zero zero = refl
lemma-mult-zero (succ n) = trans step1 step2
  where
    step1 : add (mult n zero) zero == add zero zero
    step1 = context (λ [-] → add [-] zero) (lemma-mult-zero n)

    step2 : add zero zero == zero
    step2 = refl

-- Hint: do a case distinction on n. Use the induction hypothesis. You
-- may also have to use 'context' (see above).
lemma-add-one :  ∀ (n : ℕ) -> add n (succ zero) == succ n
lemma-add-one zero = refl
lemma-add-one (succ n) = context succ (lemma-add-one n)

-- Hint: for this lemma, you may have to use 'trans' and 'context'.
-- The function (\x -> add x (succ zero)) may also be useful.
lemma-mult-one : ∀ (n : ℕ) -> mult n (succ zero) == n
lemma-mult-one zero = refl
lemma-mult-one (succ n) = trans step1 step2
  where
    step1 : add (mult n (succ zero)) (succ zero) == add n (succ zero)
    step1 = context (λ [-] → add [-] (succ zero)) (lemma-mult-one n)

    step2 : add n (succ zero) == succ n
    step2 = lemma-add-one n

-- Fill in the remaining steps of this lemma.
lemma-mult-succ : ∀ (n m : ℕ) -> add (mult m n) m == mult m (succ n)
lemma-mult-succ n zero = refl
lemma-mult-succ n (succ m) = trans step1 (trans step2 (trans step3 (trans step4 (trans step5 step6))))
  where
    -- Reflexitity works here because the equation holds
    -- by definition (of the function mult).
    step1 : add (mult (succ m) n) (succ m) == add (add (mult m n) n) (succ m)
    step1 = refl

    -- Use associativity of addition.
    step2 : add (add (mult m n) n) (succ m) == add (mult m n) (add n (succ m))
    step2 = lemma-add-assoc (mult m n) n (succ m)

    -- Use C-c C-, to check what needs to be proved. Then use the
    -- appropriate lemma.
    step3 : add (mult m n) (add n (succ m)) == add (mult m n) (add m (succ n))
    step3 = context (\ y -> add (mult m n) y) (lemma3 n m)

    -- Use associativity again. Note that the 'symm' is needed to get
    -- the equation in the correct form for lemma-add-assoc.
    step4 : add (mult m n) (add m (succ n)) == add (add (mult m n) m) (succ n)
    step4 = symm (lemma-add-assoc (mult m n) m (succ n))

    step5 : add (add (mult m n) m) (succ n) == add (mult m (succ n)) (succ n)
    step5 = context (\ x -> add x (succ n)) (lemma-mult-succ n m)

    -- Once again, reflexivity will work here, because the equation
    -- holds by definition of the function mult.
    step6 : add (mult m (succ n)) (succ n) == mult (succ m) (succ n)
    step6 = refl

-- Finally, a theorem stating that multiplication is commutative. If
-- you proved all of the above lemmas, the theorem will be true.
--
-- If you see yellow highlighting here, it is because you haven't yet
-- completed the definition of the 'mult' function.
theorem-mult-commutative : ∀ (n m : ℕ) -> mult n m == mult m n
theorem-mult-commutative zero m = symm (lemma-mult-zero m) 
theorem-mult-commutative (succ n) m =
   trans (context (\ x -> add x m) (theorem-mult-commutative n m))
     (lemma-mult-succ n m)