module BoolExprComputation where

open import BoolExpr

{-
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 ⇒, cf Thierry's lecture. In fact, we can define the transitive-reflexive closure of any binary relation, as follows:
-}

data _* {A : Set} (R : A → A → Set) : A → A → Set where
   r : (a : A) → (R *) a a
   i : (a a' : A) → R a a' → (R *) a a'
   t : (a a' a'' : A) → (R *) a a' → (R *) a' a'' → (R *) a a''

{-
Now we can implement proof by "rule induction", cf Thierry's lecture:
-}

*-induction : {A : Set} → {R Q : A → A → Set} →
   ((a : A) → Q a a) →
   ((a a' : A) → R a a' → Q a a') →
   ((a a' a'' : A) → Q a a' → Q a' a'' → Q a a'') →
   (a a' : A) →
   (R *) a a' →
   Q a a'
*-induction q-refl q-inj q-trans a .a (r .a) = q-refl a
*-induction q-refl q-inj q-trans a a' (i .a .a' p) = q-inj a a' p
*-induction q-refl q-inj q-trans a a'' (t .a a' .a'' p q) = q-trans a a' a'' (*-induction q-refl q-inj q-trans a a' p) (*-induction q-refl q-inj q-trans a' a'' q)

-- _⇒*_ : BoolExpr → BoolExpr → Set
-- t ⇒* t' = (⇒ *) t t'