module BoolProofs where

open import Bool
open import Identity
open import PropositionalLogic

{-
We shall now prove an identity for booleans by writing a program that maps a boolean to a proof of that identity:
-}

notnotI : (b : Bool) → b ≡ not (not b)
notnotI true = refl
notnotI false = refl

{-
Clearly, we could also have written

notnotI x = if x then refl else refl

It is often useful to turn a boolean into set so that true maps to an inhabited set and false maps to an empty set. We call this "isTrue" predicate "isTrue": 
-}

isTrue : Bool -> Set
isTrue true = ⊤
isTrue false = ⊥
 
{-
Exercise:
We can prove the law of excluded middle for booleans (note that we have claossical propositional logic here)

em-bool : (b : bool) → isTrue (b || not b)
em-bool b = ?

Prove the following de Morgan law 

deMorgan-or : (b b' : Bool) → not (b || b') ≡ not b && not b'
deMorgan-or b b' = {!!}
-}