-- This project is a continuation of homework 1. You will define some
-- basic functions and predicates on the natural numbers and prove
-- some theorems about them.

open import Equality

-- ----------------------------------------------------------------------
-- * Basic definitions

-- We start with the definitions of the natural numbers and addition
-- and multiplication. You have seen this before. For convenience, we
-- use infix notation for addition and multiplication.

infixl 7 _+_
infixl 9 _*_

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ -> ℕ -> ℕ
zero + y = y
succ x + y = succ (x + y)

_*_ : ℕ -> ℕ -> ℕ
zero * m = zero
succ n * m = n * m + m

-- ----------------------------------------------------------------------
-- * More properties of addition and multiplication

-- Note: the proof of the following theorems may require additional
-- lemmas. You have to state and prove your own lemmas. If you need
-- any lemmas from Homework 1 or from class, copy them and their
-- proofs here. (You may have to adjust the notations accordingly).

lemma-n-plus-zero : ∀ n -> n == n + zero
lemma-n-plus-zero zero = refl
lemma-n-plus-zero (succ n) = context succ (lemma-n-plus-zero n)

lemma-n-plus-succ : ∀ n m -> succ (n + m) == n + (succ m)
lemma-n-plus-succ zero m = refl
lemma-n-plus-succ (succ n) m = context succ (lemma-n-plus-succ n m)

lemma-comm : ∀ n m -> n + m == m + n
lemma-comm zero m = lemma-n-plus-zero m
lemma-comm (succ n) m = trans step1 step2
  where
    step1 : succ (n + m) == succ (m + n)
    step1 = context succ (lemma-comm n m)

    step2 : succ (m + n) == m + succ n
    step2 = lemma-n-plus-succ m n

lemma-assoc : ∀ n m k -> (n + m) + k == n + (m + k)
lemma-assoc zero m k = refl
lemma-assoc (succ n) m k = context succ (lemma-assoc n m k)

lemma-assoc2 : ∀ n m k -> (n + m) + k == (n + k) + m
lemma-assoc2 zero m k = lemma-comm m k
lemma-assoc2 (succ n) m k = context succ (lemma-assoc2 n m k)

-- 1. Prove the following distributivity law.
theorem-right-distributive : ∀ (n m k : ℕ) -> (n + m) * k == n * k + m * k
theorem-right-distributive zero m k = refl
theorem-right-distributive (succ n) m k = trans step1 step2
  where
    step1 : (n + m) * k + k == (n * k + m * k) + k
    step1 = context (λ x → x + k) (theorem-right-distributive n m k)

    step2 : (n * k + m * k) + k == (n * k + k) + m * k
    step2 = lemma-assoc2 (n * k) (m * k) k

-- 2. State and prove a theorem that asserts the associatitivy of
-- multiplication.
theorem-mult-associative : ∀ n m k -> (n * m) * k == n * (m * k)
theorem-mult-associative zero m k = refl
theorem-mult-associative (succ n) m k = trans step1 step2
  where
    step1 : (n * m + m) * k == (n * m) * k + m * k
    step1 = theorem-right-distributive (n * m) m k

    step2 : (n * m) * k + m * k == n * (m * k) + m * k
    step2 = context (λ x → x + m * k) (theorem-mult-associative n m k)

-- ----------------------------------------------------------------------
-- * The "less than or equal" relation

-- We define the ≤ relation as an inductive predicate.  In this way,
-- whenever n,m are natural numbers, n ≤ m will be a set, namely, the
-- set of proofs that n ≤ m.
--
-- You will learn more about inductive predicates on Friday, Jan 29.
-- For now, all you need to know is that the ≤ relation is defined as
-- the smallest relation satisfying the following two properties:
--
-- * Zero is the smallest number:
--   ∀ (n : ℕ) -> zero ≤ n
--
-- * The successor function is monotone:
--   ∀ (n m : ℕ) -> n ≤ m -> succ n ≤ succ m
--
-- The proofs of these properties are called z≤n and s≤s,
-- respectively.

infix 5 _≤_

data _≤_ : ℕ -> ℕ -> Set where
  z≤n : ∀ (n : ℕ) -> zero ≤ n
  s≤s : ∀ (n m : ℕ) -> n ≤ m -> succ n ≤ succ m

-- 1. Prove: the relation ≤ is reflexive.
theorem-refl≤ : ∀ (n : ℕ) -> n ≤ n
theorem-refl≤ zero = z≤n zero
theorem-refl≤ (succ n) = s≤s n n (theorem-refl≤ n)

theorem-refl≤' : ∀ (n m : ℕ) -> n == m -> n ≤ m
theorem-refl≤' n m refl = theorem-refl≤ n

-- 2. Prove: the relation ≤ is transitive. Hint: do a case split on
-- the hypothesis n ≤ m.
theorem-trans : ∀ (n m k : ℕ) -> n ≤ m -> m ≤ k -> n ≤ k
theorem-trans .zero m k (z≤n .m) hyp2 = z≤n k
theorem-trans .(succ n) .(succ m) .(succ m₁) (s≤s n m hyp1) (s≤s .m m₁ hyp2) = s≤s n m₁ (theorem-trans n m m₁ hyp1 hyp2)

-- 3. Prove: the relation ≤ is antisymmetric.
anti-symmetric : ∀ (n m : ℕ) -> n ≤ m -> m ≤ n -> n == m
anti-symmetric .0 .0 (z≤n .0) (z≤n .0) = refl
anti-symmetric .(succ n) .(succ m) (s≤s n m hyp1) (s≤s .m .n hyp2) = context succ (anti-symmetric n m hyp1 hyp2)

-- ----------------------------------------------------------------------
-- * Monotonicity of addition

-- Here, you will prove the monotonicity of addition. You will
-- probably need several lemmas. You must state and prove your own
-- lemmas.
--
-- Hint: you might first want to prove simpler properties, such as n ≤
-- n' implies n + m ≤ n' + m.

lemma-n-plus-succ-m : ∀ m n -> succ (n + m) ≤ n + succ m
lemma-n-plus-succ-m m zero = theorem-refl≤ (succ m)
lemma-n-plus-succ-m m (succ n) = s≤s (succ (n + m)) (n + succ m) (lemma-n-plus-succ-m m n)

lemma-m-leq-n+m : ∀ m n -> m ≤ n + m
lemma-m-leq-n+m zero n = z≤n (n + zero)
lemma-m-leq-n+m (succ m) n = theorem-trans (succ m) (succ (n + m)) (n + succ m)  step1 step2 where
  step1 : succ m ≤ succ (n + m)
  step1 = s≤s m (n + m) (lemma-m-leq-n+m m n)

  step2 : succ (n + m) ≤ n + succ m
  step2 = lemma-n-plus-succ-m m n

theorem-add-monotone-left : ∀ n n' m -> n ≤ n' -> n + m ≤ n' + m
theorem-add-monotone-left .0 n' m (z≤n .n') = lemma-m-leq-n+m m n'
theorem-add-monotone-left .(succ n) .(succ m₁) m (s≤s n m₁ hyp) = s≤s (n + m) (m₁ + m) (theorem-add-monotone-left n m₁ m hyp)

theorem-add-monotone-right : ∀ n m m' -> m ≤ m' -> n + m ≤ n + m'
theorem-add-monotone-right n m m' hyp = theorem-trans (n + m) (m + n) (n + m') step1 (theorem-trans _ _ _ step2 step3)
  where
    step1 : n + m ≤ m + n
    step1 = theorem-refl≤' (n + m) (m + n) (lemma-comm n m)

    step2 : m + n ≤ m' + n
    step2 = theorem-add-monotone-left m m' n hyp

    step3 : m' + n ≤ n + m'
    step3 = theorem-refl≤' (m' + n) (n + m') (lemma-comm m' n)

-- 4. Prove: addition is monotone.
theorem-add-monotone : ∀ (n n' m m' : ℕ) -> n ≤ n' -> m ≤ m' -> n + m ≤ n' + m'
theorem-add-monotone n n' m m' hyp1 hyp2 = theorem-trans _ _ _ step1 step2
  where
    step1 : n + m ≤ n + m'
    step1 = theorem-add-monotone-right n m m' hyp2

    step2 : n + m' ≤ n' + m'
    step2 = theorem-add-monotone-left n n' m' hyp1

-- ----------------------------------------------------------------------
-- * Bonus question: monotonicity of multiplication

-- Here, you will prove the monotonicity of multiplication. This is
-- harder than for addition, and you will need more additional lemmas.

-- First, we need commutativity of multiplication. We already proved
-- this in homework 1, so here is the proof again.

lemma-m-times-zero : ∀ m -> zero == m * zero
lemma-m-times-zero zero = refl
lemma-m-times-zero (succ m) = context (λ x → x + zero) (lemma-m-times-zero m)

lemma-m-times-succ : ∀ n m -> m * n + m == m * (succ n)
lemma-m-times-succ n zero = refl
lemma-m-times-succ n (succ m) =
  equational (succ m) * n + (succ m)
          by refl -- i.e., by definition
      equals (m * n + n) + succ m
          by lemma-assoc (m * n) n (succ m)
      equals m * n + (n + succ m)
          by context (λ x → m * n + x) (symm (lemma-n-plus-succ n m))
      equals m * n + succ (n + m)
          by context (λ x → m * n + succ x) (lemma-comm n m)
      equals m * n + succ (m + n)
          by context (λ x → m * n + x) (lemma-n-plus-succ m n)
      equals m * n + (m + succ n)
          by symm (lemma-assoc (m * n) m (succ n))
      equals (m * n + m) + succ n
          by context (λ x → x + succ n) (lemma-m-times-succ n m)
      equals m * succ n + succ n
          by refl -- i.e., by definition
      equals (succ m) * (succ n)

mult-comm : ∀ n m -> n * m == m * n
mult-comm zero m = lemma-m-times-zero m
mult-comm (succ n) m =
  equational (succ n) * m
          by refl -- i.e., by definition
      equals n * m + m
          by context (λ x → x + m) (mult-comm n m)
      equals m * n + m
          by lemma-m-times-succ n m
      equals m * (succ n)

theorem-mult-monotone-left : ∀ n n' m -> n ≤ n' -> n * m ≤ n' * m
theorem-mult-monotone-left .0 n' m (z≤n .n') = z≤n (n' * m)
theorem-mult-monotone-left .(succ n) .(succ m₁) m (s≤s n m₁ hyp) = theorem-add-monotone-left (n * m) (m₁ * m) m (theorem-mult-monotone-left n m₁ m hyp)

theorem-mult-monotone-right : ∀ n m m' -> m ≤ m' -> n * m ≤ n * m'
theorem-mult-monotone-right n m m' hyp = theorem-trans (n * m) (m * n) (n * m') step1 (theorem-trans (m * n) (m' * n) (n * m') step2 step3)
  where
    step1 : n * m ≤ m * n
    step1 = theorem-refl≤' (n * m) (m * n) (mult-comm n m)

    step2 : m * n ≤ m' * n
    step2 = theorem-mult-monotone-left m m' n hyp

    step3 : m' * n ≤ n * m'
    step3 = theorem-refl≤' (m' * n) (n * m') (mult-comm m' n)


-- 5. Prove: multiplication is monotone.
theorem-mult-monotone : ∀ (n n' m m' : ℕ) -> n ≤ n' -> m ≤ m' -> n * m ≤ n' * m'
theorem-mult-monotone n n' m m' hyp1 hyp2 = theorem-trans _ _ _ step1 step2
  where
    step1 : n * m ≤ n' * m
    step1 = theorem-mult-monotone-left n n' m hyp1

    step2 : n' * m ≤ n' * m'
    step2 = theorem-mult-monotone-right n' m m' hyp2