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