-- 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 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 prove 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 = {!!}

-- 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 = {!!}

-- Another fun theorem about negation.
lemma1 : {A B : Set} -> (A -> B) -> (A -> not B) -> not A
lemma1 = {!!}

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

-- 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 = {!!}

-- 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 = {!!}

-- 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 = {!!}

lemma4 : {A B : Set} -> A ∨ B -> not (not A ∧ not B)
lemma4 = {!!}

-- 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 = {!!}

-- -----------------------------------------------------------------------
-- * 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 = {!!}

-- Define a predicate for oddness. You have to complete the following
-- definition, as the clauses after "where" are missing.
data Odd : ℕ -> Set where
  -- You have to provide the constructors here.

-- Prove the following lemmas.

-- 3 is not even.
lemma-3-not-even : not (Even 3)
lemma-3-not-even = {!!}

-- Every number is even or odd.
lemma-even-or-odd : (n : ℕ) -> Even n ∨ Odd n
lemma-even-or-odd = {!!}

-- No number is even and odd.
lemma-not-even-and-odd : ∀ (n : ℕ) -> not (Even n ∧ Odd n)
lemma-not-even-and-odd = {!!}

-- Prove that the square of an odd number is odd, and that the square
-- of an even number is even. It is likely that you will need several
-- lemmas to prove this.
lemma-square-odd : (n : ℕ) -> Odd n -> Odd (n * n)
lemma-square-odd = {!!}

lemma-square-even : (n : ℕ) -> Even n -> Even (n * n)
lemma-square-even = {!!}

-- ----------------------------------------------------------------------
-- * 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
  -- You have to provide the constructors here.

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 = {!!}

-- Prove that the natural numbers are totally ordered.
lemma-total : ∀ n m -> n == m ∨ (n < m ∨ m < n)
lemma-total = {!!}