-- Homework 2. Due February 26.
-- 
-- MATH 4680/4681/5680, Winter 2021
--
-- If you get stuck, the discussion forum is your friend. Remember:
-- you are allowed to collaborate on the homework. Try to be helpful,
-- but avoid just giving away the answer!

module Homework2-answers where

open import Equality

-- ----------------------------------------------------------------------
-- * Propositional logic
--
-- We start by defining some propositional constants and connectives
-- as in class.

-- Propositional constants:

data True : Set where
  <> : True

data False : Set where
  -- no constructors

-- Conjunction:

infix 3 _∧_

data _∧_ : Set -> Set -> Set where
  _,_ : {A B : Set} -> A -> B -> A ∧ B

fst : {A B : Set} -> A ∧ B -> A
fst (a , b) = a

snd : {A B : Set} -> A ∧ B -> B
snd (a , b) = b

-- Disjunction:

infix 2 _∨_

data _∨_ :  Set -> Set -> Set where
  left : {A B : Set} -> A -> A ∨ B
  right : {A B : Set} -> B -> A ∨ B

-- Negation:

not : Set -> Set
not A = A -> False

-- We also define the "if and only if" operator, which we write A <-> B.

infix 1 _<->_ 
_<->_ : Set -> Set -> Set
A <-> B = (A -> B) ∧ (B -> A) 

-- ----------------------------------------------------------------------
-- * Some theorems about propositional logic

-- Complete the proofs.

-- "Ex falsum quodlibet" is Latin for "from falsity, anything you
-- want". We already proved this one in class, but prove it anyway, to
-- make sure you know how to.
ex-falsum : {A : Set} -> False -> A
ex-falsum ()

-- This theorem is known as "disjunction elimination" or "or elimination".
orElim : {A B C : Set} -> (A -> C) -> (B -> C) -> A ∨ B -> C
orElim f g (left x) = f x
orElim f g (right x) = g x

-- We already proved this one in class. Prove it anyway, to make sure
-- you remember how.
double-negation : {A : Set} -> A -> not (not A)
double-negation a = λ x → x a

-- Another fun theorem about negation.
lemma1 : {A B : Set} -> (A -> B) -> (A -> not B) -> not A
lemma1 x y = λ x₁ → y x₁ (x x₁)

-- This is another version of "ex falsum".
lemma2 : {A B : Set} -> A -> not A -> B
lemma2 a b = ex-falsum (b a)

-- This is one of De Morgan's laws. Note that we do not ask you to
-- prove the converse, because the converse is not constructively
-- valid. (You can verify this with Venn diagrams if you like).
de-morgan-1 : {A B : Set} -> not A ∨ not B -> not (A ∧ B) 
de-morgan-1 (left x) = λ x₁ → x (fst x₁)
de-morgan-1 (right x) = λ x₁ → x (snd x₁)

-- This is another of De Morgan's laws. Note that this proposition
-- uses an "if and only if". See the definition of _<->_ above.
-- Recall that to prove A <-> B, you actually have to prove
-- (A -> B) ∧ (B -> A).
de-morgan-2 : {A B : Set} -> not A ∧ not B <-> not (A ∨ B) 
de-morgan-2 = ((λ x x₁ → orElim (fst x) (snd x) x₁) , λ x → ((λ x₁ → x (left x₁)) , λ x₁ → x (right x₁)))

-- The next two lemmas are similar to De Morgan's laws, but with all
-- the negations in the conclusion. They are constructively valid.
lemma3 : {A B : Set} -> A ∧ B -> not (not A ∨ not B)
lemma3 (x , x₁) = λ x₂ → orElim (λ x₃ → x₃ x) (λ z → z x₁) x₂

lemma4 : {A B : Set} -> A ∨ B -> not (not A ∧ not B)
lemma4 (left x) = λ x₁ → fst x₁ x
lemma4 (right x) = λ x₁ → snd x₁ x

-- Bonus question. The last lemma in this section is a bit
-- challenging. It is the "missing" law of De Morgan, but with an
-- additional double negation. This version of the law is
-- constructively valid, but the proof is not at all trivial.
de-morgan-3 : {A B : Set} -> not (A ∧ B) -> not (not (not A ∨ not B))
de-morgan-3 hyp hyp2 = hyp2 (left (λ x → hyp2 (right (λ y → hyp ((x , y))))))

-- -----------------------------------------------------------------------
-- * Inductive predicates

-- In this section, we will define predicates for evenness and oddness
-- on the natural numbers, and then prove some theorems about them.
-- Some of the proofs may require lemmas. Please define and prove the
-- lemmas that you need.

-- We start with the usual definitions of the natural numbers,
-- addition, and multiplication. We also give a proof of
-- associativity, because it will be useful later.

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ -> ℕ -> ℕ
zero + m = m
succ n + m = succ (n + m)

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

lemma-add-assoc : ∀ (x y z : ℕ) ->  (x + y) + z ==  x + (y + z)
lemma-add-assoc zero y z = refl
lemma-add-assoc (succ x) y z = context succ (lemma-add-assoc x y z)

-- The evenness predicate.
data Even : ℕ -> Set where
  even-base : Even zero
  even-step : ∀ (n : ℕ) -> Even n -> Even (succ (succ n))

-- We already proved this theorem in class. Prove it again, to make
-- sure you know how!
theorem-add-even : ∀ (n m : ℕ) -> Even n -> Even m -> Even (n + m)
theorem-add-even .zero m even-base hyp2 = hyp2
theorem-add-even .(succ (succ n')) m (even-step n' hyp1') hyp2 = even-step (n' + m) (theorem-add-even n' m hyp1' hyp2)

-- Define a predicate for oddness. You have to complete the following
-- definition, as the clauses after "where" are missing.
data Odd : ℕ -> Set where
  base-odd : Odd (succ zero)
  step-odd : ∀ (n : ℕ) -> Odd n -> Odd (succ (succ n))

-- Some useful lemmas.

lemma-even-odd : (n : ℕ) -> Even n -> Odd (succ n)
lemma-even-odd .zero even-base = base-odd
lemma-even-odd .(succ (succ n)) (even-step n h) = step-odd (succ n) (lemma-even-odd n h)

lemma-odd-even : (n : ℕ) -> Odd n -> Even (succ n)
lemma-odd-even .(succ zero) base-odd = even-step zero even-base
lemma-odd-even .(succ (succ n)) (step-odd n h) = even-step (succ n) (lemma-odd-even n h)

-- Prove the following lemmas.

-- 3 is not even.
lemma-3-not-even : not (Even 3)
lemma-3-not-even (even-step .1 ())

-- Every number is even or odd.
lemma-even-or-odd : (n : ℕ) -> Even n ∨ Odd n
lemma-even-or-odd zero = left even-base
lemma-even-or-odd (succ n) = orElim (λ x → right (lemma-even-odd n x)) (λ x → left (lemma-odd-even n x)) (lemma-even-or-odd n)

-- No number is even and odd.
lemma-not-even-and-odd : ∀ (n : ℕ) -> not (Even n ∧ Odd n)
lemma-not-even-and-odd .(succ (succ n)) (even-step n x , step-odd .n y) = lemma-not-even-and-odd n (x , y)

-- Some useful lemmas.

lemma5 : (n m : ℕ) -> Odd n -> Odd m -> Even (n + m)
lemma5 .(succ zero) m base-odd h2 = lemma-odd-even m h2
lemma5 .(succ (succ n)) m (step-odd n h1) h2 = even-step (n + m) (lemma5 n m h1 h2)

lemma6 : (n m : ℕ) -> Odd n -> Even m -> Odd (n + m)
lemma6 .(succ zero) m base-odd h2 = lemma-even-odd m h2
lemma6 .(succ (succ n)) m (step-odd n h1) h2 = 
  step-odd (n + m) (lemma6 n m h1 h2)

lemma7 : (n m : ℕ) -> Odd n -> Odd m -> Odd (n * m)
lemma7 .(succ zero) m base-odd h2 = h2
lemma7 .(succ (succ n)) m (step-odd n h1) h2 =
  subst (\ u -> Odd u) (symm (lemma-add-assoc (n * m) m m)) (lemma6 (n * m) (m + m) (lemma7 n m h1 h2) (lemma5 m m h2 h2))

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

lemma10 : (n : ℕ) -> Even (n + n)
lemma10 zero = even-base
lemma10 (succ n) =
  subst (λ u → Even (succ u)) (lemma-add-succ n n) (even-step (n + n) (lemma10 n))

lemma9 : (n m : ℕ) -> Even n -> Even (n * m)
lemma9 .zero m even-base = even-base
lemma9 .(succ (succ n)) m (even-step n h) =
  subst Even (symm (lemma-add-assoc (n * m) m m)) (theorem-add-even (n * m) (m + m) (lemma9 n m h) (lemma10 m)) 

-- Prove that the square of an odd number is odd, and that the square
-- of an even number is even. You may have to come up with additional
-- lemmas to prove this.
lemma-square-odd : (n : ℕ) -> Odd n -> Odd (n * n)
lemma-square-odd n h1 = lemma7 n n h1 h1

lemma-square-even : (n : ℕ) -> Even n -> Even (n * n)
lemma-square-even n h = lemma9 n n h

-- ----------------------------------------------------------------------
-- * The less-then relation

-- Define an inductive predicate for the strict "less than". Note that
-- this is different from "less than or equal".
data _<_ : ℕ -> ℕ -> Set where
  less-zero : ∀ {n} -> zero < succ n
  less-succ : ∀ {n m} -> n < m -> succ n < succ m

infix 5 _<_

-- Prove that zero is not less than itself
lemma-zero-not-less : not (zero < zero)
lemma-zero-not-less = λ ()

-- Prove that no number is less than itself.
lemma-less-irreflexive : ∀ n -> not (n < n)
lemma-less-irreflexive zero ()
lemma-less-irreflexive (succ n) (less-succ hyp) = lemma-less-irreflexive n hyp

-- Prove that the natural numbers are totally ordered.
lemma-total : ∀ n m -> n == m ∨ (n < m ∨ m < n)
lemma-total zero zero = left refl
lemma-total zero (succ m) = right (left less-zero)
lemma-total (succ n) zero = right (right less-zero)
lemma-total (succ n) (succ m) =
  orElim (\ x -> left (context succ x))
         (\ x -> orElim (λ x₁ → right (left (less-succ x₁))) (λ x₁ → right (right (less-succ x₁))) x)
         (lemma-total n m)