module BoolExpr where open import Bool open import PropositionalLogic {- We define the type of Boolean expression, cf Figure 3.1 in Pierce: -} data BoolExpr : Set where True : BoolExpr False : BoolExpr If_then_else_ : BoolExpr → BoolExpr → BoolExpr → BoolExpr ex : BoolExpr ex = If True then False else False {- We then define the value of a Boolean expression -} val : BoolExpr → Bool val True = true val False = false val (If t₁ then t₂ else t₃) = if (val t₁) then (val t₂) else (val t₃) {- We finally map a Boolean value to a Boolean expression ("quote" in the terminology of LISP). -} quot : Bool → BoolExpr quot true = True quot false = False {- We can now define the "normal form" of a Boolean expression: -} nf : BoolExpr → BoolExpr nf b = quot (val b) Nf : BoolExpr → Set Nf True = ⊤ Nf False = ⊤ Nf (If t then t₁ else t₂) = ⊥ quot-is-Nf : (b : Bool) → Nf (quot b) quot-is-Nf true = <> quot-is-Nf false = <> nf-is-Nf : (b : BoolExpr) → Nf (nf b) nf-is-Nf b = quot-is-Nf (val b) {- Exercise: implement the principle of induction on Boolean expressions! Hint: See Pierce 3.3, p 36. -}