module BoolExprComputation where open import BoolExpr open import PropositionalLogic {- We define the binary relation t ⇒ t' of one-step reduction of Boolean expressions. Cf Pierce and Thierry's lecture. It is an inductively defined relation: there is one constructor for each rule of computation. Note that we here use "propositions as sets" and "proofs as programs"! -} data _⇒_ : BoolExpr → BoolExpr → Set where If-True : {t2 t3 : BoolExpr} → If True then t2 else t3 ⇒ t2 If-False : {t2 t3 : BoolExpr} → If False then t2 else t3 ⇒ t3 If- : {t t' t2 t3 : BoolExpr} → t ⇒ t' → If t then t2 else t3 ⇒ If t' then t2 else t3 {- Agda has an alternative notation for dependent function space using the sign for the universal quantifier ∀: we can write ∀ (x : A) → B and ∀ {x : A} → B or even leave out the domain type A ∀ x → B and ∀ {x} → B instead of (x : A) → B and {x : A} → B respectively. Exercise: Define next : BoolExpr → Maybe BoolExpr such that next t = Just t' iff there is proof p : t ⇒ t' Moreover, we can define many-step reduction ⇒ * as the reflexive-transitive closure of ⇒. In fact, we can define the transitive-reflexive closure of any binary relation, as follows: -}