Small soundness proof for Boolean formulae

BF.agda

module BF where

open import Agda.Builtin.Equality

data BF : Set where
  True  : BF
  False : BF
  Not   : BF → BF
  And   : BF → BF → BF
  Or    : BF → BF → BF

data Bool : Set where
  true false : Bool

not : Bool → Bool
not true  = false
not false = true

and : Bool → Bool → Bool
and true true = true
and _    _    = false

or : Bool → Bool → Bool
or false false = false
or _     _     = true

eval : BF → Bool
eval True  = true
eval False = false
eval (Not x)   = not (eval x)
eval (And x y) = and (eval x) (eval y)
eval (Or  x y) = or  (eval x) (eval y)

sym : {X : Set} {a b : X} → a ≡ b → b ≡ a
sym refl = refl

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

evalDoubleNeg : (f : BF) → eval (Not (Not f)) ≡ eval f
evalDoubleNeg f = doubleNeg (eval f)

removeTopLevelDoubleNeg : BF -> BF
removeTopLevelDoubleNeg (Not (Not x)) = removeTopLevelDoubleNeg x
removeTopLevelDoubleNeg x             = x

rtldnSound : (f : BF) → eval (removeTopLevelDoubleNeg f) ≡ eval f
rtldnSound True  = refl
rtldnSound False = refl
-- rtldnSound (Not (Not p)) rewrite rtldnSound p = sym (doubleNeg (eval p))
rtldnSound (Not (Not p)) with eval (removeTopLevelDoubleNeg p) | rtldnSound p
... | ._ | refl = sym (doubleNeg (eval p))
rtldnSound (Not True)  = refl
rtldnSound (Not False) = refl
rtldnSound (Not (And p q)) = refl
rtldnSound (Not (Or  p q)) = refl
rtldnSound (And x y) = refl
rtldnSound (Or  x y) = refl