Some parts of TAPL Chapter 3 Formalized in Agda

Chapter3.agda

open import Data.Nat hiding (pred)
open import Data.Nat.Properties
open import Data.Nat.Induction
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation
open import Induction.WellFounded
import Relation.Binary.Construct.On as On
open ≤-Reasoning

-- Definition [Terms, Inductively] 3.2.2 (p26)
-- Note that `Set` means "Type"

data 𝑇 : Set where
  true          : 𝑇
  false         : 𝑇
  zero          : 𝑇
  succ          : 𝑇 → 𝑇
  pred          : 𝑇 → 𝑇
  iszero        : 𝑇 → 𝑇
  if_then_else_ : 𝑇 → 𝑇 → 𝑇 → 𝑇


-- Definition 3.3.2 (p29)
size : 𝑇 → ℕ
size true                   = 1
size false                  = 1
size zero                   = 1
size (succ x)               = suc (size x)
size (pred x)               = suc (size x)
size (iszero x)             = suc (size x)
size (if x then x₁ else x₂) = suc (size x + size x₁ + size x₂)

-- Note that ⊔ means "max"
depth : 𝑇 → ℕ
depth true                   = 1
depth false                  = 1
depth zero                   = 1
depth (succ x)               = suc (depth x)
depth (pred x)               = suc (depth x)
depth (iszero x)             = suc (depth x)
depth (if x then x₁ else x₂) = suc (depth x ⊔ depth x₁ ⊔ depth x₂)


-- We now start our proof of 3.3.4 (p31)
-- The first is induction on depth
inductionDepth : ∀ {ℓ} (p : 𝑇 → Set ℓ)
  → (∀ s → (∀ r → depth r < depth s → p r) → p s)
  → (∀ s → p s)

-- Note that the predicate `p` does not return a boolean,
-- but rather a Set ℓ.
-- The type `p s` represents a theorem related to s (for example depth(s) ≥ 0)
-- And a value of type `p s` is a proof of the theorem
 
-- ℓ is the "level" of the set. We have Set₁, Set₂, ...
-- This is necessary to avoid due to Russell's paradox
-- Note that the surrounding {} means that ℓ is an implicit parameter


-- We implement the proof via well-founded induction
-- Well-founded induction allows us to show 
--    (∀ s → (∀ r → r < s → p r) → p s) →
--    (∀ s → p s)
-- which holds so long as _<_ is well-founded


-- We define _<ᵈ_ as a relationship on terms, where
-- t₁ <ᵈ t₂ iff depth t₁ < depth t₂
-- This will make things easier later
_<ᵈ_ : 𝑇 → 𝑇 → Set
t₁ <ᵈ t₂ = depth t₁ < depth t₂

-- Note that _<ᵈ_ is a function that returns a Set ("type")


-- Here we show that 𝑇 is well-founded wrt the relationship _<ᵈ_
-- This is because `depth t` is a natural number, and natural numbers
-- are well-founded w.r.t to
-- 
-- This is a very easy way to show that relationships are well-founded.
-- 
-- Also note that we don't need to know anything about the implementation
-- of `depth`
<ᵈ-wf : WellFounded _<ᵈ_
<ᵈ-wf = On.wellFounded depth <-wellFounded

-- Here we prove induction on depth holds using well-founded induction
inductionDepth {ℓ} p ind = wfRec p ind
  where
    open All <ᵈ-wf ℓ

-- Induction on size proceeds similarly

_<ˢ_ : 𝑇 → 𝑇 → Set
t₁ <ˢ t₂ = size t₁ < size t₂

<ˢ-wf : WellFounded _<ˢ_
<ˢ-wf = On.wellFounded size <-wellFounded

inductionSize : ∀ {ℓ} (p : 𝑇 → Set ℓ)
  → (∀ s → (∀ r → size r < size s → p r) → p s)
  → (∀ s → p s)
inductionSize {ℓ} p ind = wfRec p ind
  where
    open All <ˢ-wf ℓ

-- For structural induction, we will define _⊂_ as the "immediate"
-- subterm relation
-- 
-- Here we define the relation.
-- The type t₁ ⊂ t₂ represents the theorem,
-- and it's inhabitants (data constructors) represents the proof

data _⊂_ : 𝑇 → 𝑇 → Set where
  succ'   : (t : 𝑇)     → t ⊂ (succ t)
  pred'   : (t : 𝑇)     → t ⊂ (pred t)
  iszero' : (t : 𝑇)     → t ⊂ (iszero t)
  if'     : (t u v : 𝑇) → t ⊂ (if t then u else v)
  then'   : (t u v : 𝑇) → u ⊂ (if t then u else v)
  else'   : (t u v : 𝑇) → v ⊂ (if t then u else v)

-- Now we can express the theorem
inductionStruct : ∀ {ℓ} (p : 𝑇 → Set ℓ)
  → (∀ s → (∀ r → r ⊂ s → p r) → p s)
  → (∀ s → p s)

-- Once again we will proceed via well-founded induction
⊂-wf : WellFounded _⊂_

-- To show that _⊂_ is well-founded, we will show that
-- t₁ ⊂ t₂ implies t₁ <ˢ t₂,
-- therefore 𝑇 is well-founded on _⊂_ since <ˢ is well-founded
--
-- First let's show the implication
subSize : ∀ {t u} → t ⊂ u → t <ˢ u

-- Note that we are "pattern matching" on the *proofs*, not terms
--
-- Therefore we don't need to consider cases where `u` is `zero` etc,
-- since there is no proof constructor for t ⊂ zero
--
-- The proofs of the unary predicates are simple, they follow directly from the
-- definition of size
subSize (succ' t)   = n<1+n (size t)
subSize (pred' t)   = n<1+n (size t)
subSize (iszero' t) = n<1+n (size t)


-- Proofs of the if-then-else are also relatively straightforward
-- They rely respectively on the facts, t ≤ t + u + v, u ≤ t + u + v, v ≤ t + u + v
subSize (if' t u v) = s≤s
  (begin
    size t ≤⟨ m≤m+n (size t) (size u) ⟩
    size t + size u ≤⟨ m≤m+n (size t + size u) (size v) ⟩
    size t + size u + size v
  ∎)
subSize (then' t u v) = s≤s
  (begin
    size u ≤⟨ m≤m+n (size u) (size t) ⟩
    size u + size t ≡⟨ +-comm (size u) (size t) ⟩
    size t + size u ≤⟨ m≤m+n (size t + size u) (size v) ⟩
    size t + size u + size v
  ∎)

subSize (else' t u v) = s≤s
  (begin
    size v                     ≤⟨ m≤m+n (size v) (size t + size u) ⟩
    size v + (size t + size u) ≡⟨ +-comm (size v) (size t + size u) ⟩
    size t + size u + size v
  ∎)

-- We can now prove that ⊂-wf is well-founded via the implication

⊂-wf = wellFounded <ˢ-wf
  where
    open Subrelation subSize


-- We finally can prove via well-founded induction
inductionStruct {ℓ} p ind = wfRec p ind
  where
    open All ⊂-wf ℓ


-- We now define the one-step evaluation relation
-- The inference rules are the proofs that the relationship holds
data _⟶_ : 𝑇 → 𝑇 → Set where
  E-IfTrue  : ∀ {t₂ t₃} → if true then t₂ else t₃ ⟶ t₂
  E-IfFalse : ∀ {t₂ t₃} → if false then t₂ else t₃ ⟶ t₃
  E-If      : ∀ {t₁ t′₁ t₂ t₃} →
              t₁ ⟶ t′₁
              --------
            → if t₁ then t₂ else t₃ ⟶ if t′₁ then t₂ else t₃
infix 10 _⟶_


-- Once again, we pattern match on the proofs
⟶-det : ∀ {t t′ t′′} → t ⟶ t′ → t ⟶ t′′ → t′ ≡ t′′
⟶-det E-IfTrue E-IfTrue                       = refl
⟶-det E-IfFalse E-IfFalse                     = refl
⟶-det (E-If d₁) (E-If d₂) rewrite ⟶-det d₁ d₂ = refl

-- Reflexive-Transitive closure
data _⟶*_ : 𝑇 → 𝑇 → Set where
  ⟶*sym : ∀ {t} → t ⟶* t
  ⟶*+   : ∀ {t u v} → t ⟶* u → u ⟶ v → t ⟶* v

infix 10 _⟶*_

-- Example derivation
derivation : if true then (if true then true else false) else false ⟶* true
derivation = ⟶*+ (⟶*+ ⟶*sym E-IfTrue) E-IfTrue