-- Homework 1a. Due February 1.
-- 
-- MATH 4680/4681/5680, Winter 2021
--
-- Note: this is the first part of Homework 1. There will also be a
-- Homework 1b, also due on February 1.
--
-- Complete the following file by filling in the "holes". There are 5
-- holes, and each of them is a homework problem. Some holes can't be
-- filled until you have completed earlier ones.
--
-- Hint: If you place the cursor in any hole, you can type C-c C-,
-- (Control-c followed by Control-comma) to see the type of the hole,
-- i.e., the proposition you have to prove or the type of the
-- expression you have to write. Moreover, C-c C-, also shows you the
-- current context, i.e., what the types of the relevant variables
-- are.
--
-- 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!

open import Equality

-- ----------------------------------------------------------------------
-- * Booleans

-- The set of booleans.
data Bool : Set where
  true : Bool
  false : Bool

-- ----------------------------------------------------------------------
-- ** Some functions

-- The "not" function.
not : Bool -> Bool
not true = false
not false = true

-- The boolean "and" function.
and : Bool -> Bool -> Bool
and true y = y
and false y = false

-- The boolean "or" function.
or : Bool -> Bool -> Bool
or true y = {!!}
or false y = {!!}

-- ----------------------------------------------------------------------
-- ** Some theorems

-- A theorem about double negation.
--
-- Note: the proof uses 'refl', which is defined in Equality.agda.
-- It stands for reflexivity (of equality), and its type is a == a, for all a.
double-negation : ∀ (x : Bool) -> not (not x) == x
double-negation true = refl
double-negation false = refl

-- A theorem about De Morgan's law. 
de-morgan : ∀ (x y : Bool) -> not (and x y) == or (not x) (not y)
de-morgan true y = {!!}
de-morgan false y = {!!}

-- A theorem about the commutativity of "or".
or-commutative : ∀ (x y : Bool) -> or x y == or y x
or-commutative x y = {!!}