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 = ⊥ {- We can also define equality (equivalence) of booleans as a function returning a boolean (a computable function): -} _<==>_ : Bool → Bool → Bool true <==> true = true true <==> false = false false <==> true = false false <==> false = true {- We can use it to state and prove the double negation law in the following form: -} notnot : (b : Bool) → isTrue (b <==> not (not b)) notnot true = <> notnot false = <> {- Exercise: Now 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' = {!!} Prove it also with the alternative formulation using isTrue: deMorgan-or-isTrue : (b b' : Bool) → isTrue (not (b || b') <==> not b && not b') deMorgan-or-isTrue b b' = {!!} -}