module Homework140929 where

open import PropositionalLogic

-- Problem 1. Prove the converse of the law of double negation:

reversedn : {A : Set} → A → ¬ (¬ A)
reversedn a f = {!!}

-- Problem 2. Is de Morgan's law ¬ A & ¬ B iff  ¬ (A ∨ B)
-- valid intuitionistically? In other words try to prove

demorgan1 : {A B : Set} → ¬ A & ¬ B →  ¬ (A ∨ B)
demorgan1 c = {!!}

demorgan2 : {A B : Set} → ¬ (A ∨ B) → ¬ A & ¬ B 
demorgan2 c = {!!}

-- or explain why one of them cannot be proved!

-- Problem 3. To prove a general property P for all Boolean expressions by "structural induction" you prove the base cases P true, P false, and a step case for if-statements. Express this induction principle as a type in Agda and prove it! Hint. Look at the type corresponding to mathematical induction on natural numbers! 

-- Problem 4. Define monads in Agda as a record! Look at the wikipedia article "Monad (functional programming)" where you can see that a monad is (i) a type constructor; (ii) an unit operation (called "return" in Haskell); and (iii) a binding operation (called _>>=_ in Haskell). 

-- Then define the Maybe monad as an instance of the Monad record in Agda!

-- Add the monad laws (see the wikipedia article) to your record for monads. Can you prove that the laws hold for the Maybe monad?

-- Hint: we defined the record for Counters in the lecture, and showed how the natural numbers form an instance of it. If you want more information on records, please consult the Agda wiki.