{- George Bool (1815--1864) invented Boolean Logic. The data type Bool is named after him. His intention was to equip logic with simple laws like the ones we learn at school for +,*,^, etc. In 1864 his wife, a firm believer in homeopathic medicine, attempted to treat the chill he had acquired by walking home in heavy rain by pouring buckets of cold water on him. He caught pneumonia and died. But, don't let that put you off! Please complete the exercises below -} module BoolQuestions where data Bool : Set where tt ff : Bool data _isTrue : Bool → Set where qed : tt isTrue ¬_ : Bool → Bool ¬ tt = ff ¬ ff = tt _∧_ : Bool → Bool → Bool a ∧ b = {!!} _∨_ : Bool → Bool → Bool a ∨ b = {!!} _⇒_ : Bool → Bool → Bool a ⇒ b = ¬ a ∨ b _≡_ : Bool → Bool → Bool tt ≡ b = b ff ≡ b = ¬ b infix 2 _≡_ refl≡ : ∀ a → (a ≡ a) isTrue refl≡ a = {!!} symm≡ : ∀ a b → ((a ≡ b) ⇒ (b ≡ a)) isTrue symm≡ a b = {!!} trans≡ : ∀ a b c → (((a ≡ b) ∧ (b ≡ c)) ⇒ (a ≡ c)) isTrue trans≡ a b c = {!!} iden∨ : ∀ a → (a ∨ ff ≡ a) isTrue iden∨ a = {!!} iden∧ : ∀ a → (a ∧ tt ≡ a) isTrue iden∧ a = {!!} anni∧ : ∀ a → (a ∧ ff ≡ ff) isTrue anni∧ a = {!!} anni∨ : ∀ a → (a ∨ tt ≡ tt) isTrue anni∨ a = {!!} comp∨ : ∀ a → (a ∨ ¬ a ≡ tt) isTrue comp∨ a = {!!} comp∧ : ∀ a → (a ∧ ¬ a ≡ ff) isTrue comp∧ a = {!!} assoc∨ : ∀ a b c → (a ∨ (b ∨ c) ≡ (a ∨ b) ∨ c) isTrue assoc∨ a b c = {!!} assoc∧ : ∀ a b c → (a ∧ (b ∧ c) ≡ (a ∧ b) ∧ c) isTrue assoc∧ a b c = {!!} comm∨ : ∀ a b → (a ∨ b ≡ b ∨ a) isTrue comm∨ a b = {!!} comm∧ : ∀ a b → (a ∧ b ≡ b ∧ a) isTrue comm∧ a b = {!!} dist∧ : ∀ a b c → (a ∧ (b ∨ c) ≡ (a ∧ b) ∨ (a ∧ c)) isTrue dist∧ a b c = {!!} dist∨ : ∀ a b c → (a ∨ (b ∧ c) ≡ (a ∨ b) ∧ (a ∨ c)) isTrue dist∨ a b c = {!!} abso∨ : ∀ a b → (a ∨ (a ∧ b) ≡ a) isTrue abso∨ a b = {!!} abso∧ : ∀ a b → (a ∧ (a ∨ b) ≡ a) isTrue abso∧ a b = {!!} idem∨ : ∀ a → (a ∨ a ≡ a) isTrue idem∨ a = {!!} idem∧ : ∀ a → (a ∧ a ≡ a) isTrue idem∧ a = {!!} doub¬ : ∀ a → (a ≡ ¬ ¬ a) isTrue doub¬ a = {!!} deMo∧ : ∀ a b → (¬ a ∧ ¬ b ≡ ¬ (a ∨ b)) isTrue deMo∧ = {!!} deMo∨ : ∀ a b → (¬ a ∨ ¬ b ≡ ¬ (a ∧ b)) isTrue deMo∨ = {!!}