tapl8.agda

module tapl8 where

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Star
open import Data.Empty

infix 5 if_then_else_

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

-- Value is a subset of Term

data NValue : Term → Set where
  nv-zero : NValue zero
  nv-succ : ∀ {t} → NValue t → NValue (succ t)

data Value : Term → Set where
  v-true  : Value true
  v-false : Value false
  v-num   : ∀ {t} → NValue t → Value t

infix 3 _⟶_

data _⟶_ : Term → Term → 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₃
  e-succ       : ∀ {t t′} → t ⟶ t′ → succ t ⟶ succ t′
  e-predzero   : pred zero ⟶ zero
  e-predsucc   : ∀ {nv} → NValue nv → pred (succ nv) ⟶ nv
  e-pred       : ∀ {t t′} → t ⟶ t′ → pred t ⟶ pred t′
  e-iszerozero : iszero zero ⟶ true
  e-iszerosucc : ∀ {nv} → NValue nv → iszero (succ nv) ⟶ false
  e-iszero     : ∀ {t t′} → t ⟶ t′ → iszero t ⟶ iszero t′

infix 3 _⟶⋆_

_⟶⋆_ : Term → Term → Set
_⟶⋆_ = Star _⟶_

infix 3 _⇓_[_]

data _⇓_[_] : Term → (v : Term) → Value v → Set where
  b-value      : ∀ {t} → (vt : Value t) → t ⇓ t [ vt ]
  b-iftrue     : ∀ {t₁ t₂ t₃ v vt} → t₁ ⇓ true  [ v-true ]  → t₂ ⇓ v [ vt ] → if t₁ then t₂ else t₃ ⇓ v [ vt ]
  b-iffalse    : ∀ {t₁ t₂ t₃ v vt} → t₁ ⇓ false [ v-false ] → t₃ ⇓ v [ vt ] → if t₁ then t₂ else t₃ ⇓ v [ vt ]
  b-succ       : ∀ {t nv vt} → t ⇓ nv [ v-num vt ] → succ t ⇓ succ nv [ v-num (nv-succ vt) ]
  b-predzero   : ∀ {t}       → t ⇓ zero    [ v-num nv-zero ]      → pred t ⇓ zero [ v-num nv-zero ]
  b-predsucc   : ∀ {t nv vt} → t ⇓ succ nv [ v-num (nv-succ vt) ] → pred t ⇓ nv   [ v-num vt ]
  b-iszerozero : ∀ {t vt}    → t ⇓ zero    [ vt ]                 → iszero t ⇓ true  [ v-true ]
  b-iszerosucc : ∀ {t nv vt} → t ⇓ succ nv [ v-num (nv-succ vt) ] → iszero t ⇓ false [ v-false ]

sub-lem : ∀ {t v vt} → NValue t → t ⇓ v [ vt ] → pred (succ t) ⇓ v [ vt ]
sub-lem {true} () d
sub-lem {false} () d
sub-lem {if t then t₁ else t₂} () d
sub-lem {zero} nv (b-value (v-num nv-zero)) = b-predsucc (b-value (v-num (nv-succ nv-zero)))
sub-lem {succ t} (nv-succ nv) (b-value (v-num (nv-succ x))) = b-predsucc (b-value (v-num (nv-succ (nv-succ x))))
sub-lem {succ t} {vt = v-num (nv-succ vt)} (nv-succ nv₁) (b-succ d) with sub-lem nv₁ d
sub-lem {succ t} {.(succ (pred (succ t)))} {v-num (nv-succ ())} (nv-succ nv₁) (b-succ d) | b-value _
sub-lem {succ t} {.(succ zero)} {v-num (nv-succ .nv-zero)} (nv-succ nv₁) (b-succ d) | b-predzero ()
sub-lem {succ t} {_} {v-num (nv-succ vt)} (nv-succ nv₁) (b-succ d) | b-predsucc q = b-predsucc (b-succ q)
sub-lem {pred t} () d
sub-lem {iszero t} () d

lem : ∀ {t t′ v vt} → t ⟶ t′ → t′ ⇓ v [ vt ] → t ⇓ v [ vt ]
lem e-iftrue d = b-iftrue (b-value v-true) d
lem e-iffalse d = b-iffalse (b-value v-false) d
lem (e-if r) (b-value (v-num ()))
lem (e-if r) (b-iftrue d d₁) = b-iftrue (lem r d) d₁
lem (e-if r) (b-iffalse d d₁) = b-iffalse (lem r d) d₁
lem (e-succ r) (b-value (v-num (nv-succ x))) = b-succ (lem r (b-value (v-num x)))
lem (e-succ r) (b-succ d) = b-succ (lem r d)
lem e-predzero (b-value (v-num nv-zero)) = b-predzero (b-value (v-num nv-zero))
lem {pred (succ t)} (e-predsucc r) d = sub-lem r d
lem (e-pred r) (b-value (v-num ()))
lem (e-pred r) (b-predzero d) = b-predzero (lem r d)
lem (e-pred r) (b-predsucc d) = b-predsucc (lem r d)
lem e-iszerozero (b-value v-true) = b-iszerozero (b-value (v-num nv-zero))
lem e-iszerozero (b-value (v-num ()))
lem (e-iszerosucc x) (b-value v-false) = b-iszerosucc (b-value (v-num (nv-succ x)))
lem (e-iszerosucc x₁) (b-value (v-num ()))
lem (e-iszero r) (b-value (v-num ()))
lem (e-iszero r) (b-iszerozero d) = b-iszerozero (lem r d)
lem (e-iszero r) (b-iszerosucc d) = b-iszerosucc (lem r d)

lem-stop : ∀ {t t′} → t ⟶ t′ → ¬ Value t
lem-stop e-iftrue (v-num ())
lem-stop e-iffalse (v-num ())
lem-stop (e-if d) (v-num ())
lem-stop (e-succ d) (v-num (nv-succ vt)) = lem-stop d (v-num vt)
lem-stop e-predzero (v-num ())
lem-stop (e-predsucc x) (v-num ())
lem-stop (e-pred d) (v-num ())
lem-stop e-iszerozero (v-num ())
lem-stop (e-iszerosucc x) (v-num ())
lem-stop (e-iszero d) (v-num ())

ex-3-5-17 : ∀ {t v} → t ⟶⋆ v → (vt : Value v) → t ⇓ v [ vt ]
ex-3-5-17 ε vt = b-value vt
ex-3-5-17 (e-iftrue ◅ r) vt = b-iftrue (b-value v-true) (ex-3-5-17 r vt)
ex-3-5-17 (e-iffalse ◅ r) vt = b-iffalse (b-value v-false) (ex-3-5-17 r vt)
ex-3-5-17 (e-if x ◅ r) vt with ex-3-5-17 r vt
ex-3-5-17 (e-if x ◅ r) (v-num ()) | b-value _
ex-3-5-17 (e-if x ◅ r) vt | b-iftrue u u₁ = b-iftrue (lem x u) u₁
ex-3-5-17 (e-if x ◅ r) vt | b-iffalse u u₁ = b-iffalse (lem x u) u₁
ex-3-5-17 (e-succ x ◅ r) vt with ex-3-5-17 r vt
ex-3-5-17 (e-succ x₁ ◅ r) (v-num (nv-succ x)) | b-value .(v-num (nv-succ x)) = b-succ (lem x₁ (b-value (v-num x)))
ex-3-5-17 (e-succ x ◅ r) _ | b-succ q = b-succ (lem x q)
ex-3-5-17 (e-predzero ◅ ε) (v-num nv-zero) = b-predzero (b-value (v-num nv-zero))
ex-3-5-17 (e-predzero ◅ () ◅ r) vt
ex-3-5-17 (e-predsucc x ◅ ε) vt = sub-lem x (b-value vt)
ex-3-5-17 (e-predsucc x ◅ x₁ ◅ r) vt with lem-stop x₁ (v-num x)
... | ()
ex-3-5-17 (e-pred x ◅ r) vt with ex-3-5-17 r vt
ex-3-5-17 (e-pred x₁ ◅ r) (v-num ()) | b-value _
ex-3-5-17 (e-pred x ◅ r) .(v-num nv-zero) | b-predzero u = b-predzero (lem x u)
ex-3-5-17 (e-pred x ◅ r) _ | b-predsucc u = b-predsucc (lem x u)
ex-3-5-17 (e-iszerozero ◅ ε) v-true = b-iszerozero (b-value (v-num nv-zero))
ex-3-5-17 (e-iszerozero ◅ ε) (v-num ())
ex-3-5-17 (e-iszerozero ◅ () ◅ r) vt
ex-3-5-17 (e-iszerosucc x ◅ ε) v-false = b-iszerosucc (b-value (v-num (nv-succ x)))
ex-3-5-17 (e-iszerosucc x ◅ ε) (v-num ())
ex-3-5-17 (e-iszerosucc x ◅ () ◅ r) vt
ex-3-5-17 (e-iszero x ◅ r) vt with ex-3-5-17 r vt
ex-3-5-17 (e-iszero x₁ ◅ r) (v-num ()) | b-value _
ex-3-5-17 (e-iszero x ◅ r) .v-true | b-iszerozero u = b-iszerozero (lem x u)
ex-3-5-17 (e-iszero x ◅ r) .v-false | b-iszerosucc u = b-iszerosucc (lem x u)

rev-lem-cong : ∀ {t t′} → (f : Term → Term) (c : ∀ {t t′} → t ⟶ t′ → f t ⟶ f t′) → t ⟶⋆ t′ → f t ⟶⋆ f t′
rev-lem-cong f c ε = ε
rev-lem-cong f c (x ◅ r) = c x ◅ rev-lem-cong f c r

rev-lem-if : ∀ {t₁ t₁′ t₂ t₃} → t₁ ⟶⋆ t₁′ → if t₁ then t₂ else t₃ ⟶⋆ if t₁′ then t₂ else t₃
rev-lem-if {t₁} {t₂ = t₂} {t₃ = t₃} = rev-lem-cong (λ t → if t then t₂ else t₃) e-if

rev : ∀ {t v vt} → t ⇓ v [ vt ] → t ⟶⋆ v
rev (b-value vt) = ε
rev (b-iftrue d d₁) = rev-lem-if (rev d) ◅◅ e-iftrue ◅ rev d₁
rev (b-iffalse d d₁) = rev-lem-if (rev d) ◅◅ e-iffalse ◅ rev d₁
rev (b-succ d) = rev-lem-cong succ e-succ (rev d)
rev (b-predzero d) = (rev-lem-cong pred e-pred (rev d)) ◅◅ e-predzero ◅ ε
rev {vt = v-num nv} (b-predsucc d) = (rev-lem-cong pred e-pred (rev d)) ◅◅ e-predsucc nv ◅ ε
rev (b-iszerozero d) = (rev-lem-cong iszero e-iszero (rev d)) ◅◅ e-iszerozero ◅ ε
rev (b-iszerosucc {vt = vt} d) = (rev-lem-cong iszero e-iszero (rev d)) ◅◅ e-iszerosucc vt ◅ ε

data Type : Set where
  bool : Type
  nat  : Type

infix 4 _∶_

data _∶_ : Term → Type → Set where
  t-true    : true ∶ bool
  t-false   : false ∶ bool
  t-if      : ∀ {t₁ t₂ t₃ T}
              → t₁ ∶ bool
              → t₂ ∶ T
              → t₃ ∶ T
              → if t₁ then t₂ else t₃ ∶ T
  t-zero   : zero ∶ nat
  t-succ   : ∀ {t} → t ∶ nat → succ t ∶ nat
  t-pred   : ∀ {t} → t ∶ nat → pred t ∶ nat
  t-iszero : ∀ {t} → t ∶ nat → iszero t ∶ bool

lem-8-2-2-1 : ∀ {R} → true ∶ R → R ≡ bool
lem-8-2-2-1 t-true = refl

lem-8-2-2-2 : ∀ {R} → false ∶ R → R ≡ bool
lem-8-2-2-2 t-false = refl

lem-8-2-2-3 : ∀ {t₁ t₂ t₃ R}
              → if t₁ then t₂ else t₃ ∶ R
              → t₁ ∶ bool × t₂ ∶ R × t₃ ∶ R
lem-8-2-2-3 (t-if d₁ d₂ d₃) = d₁ , d₂ , d₃

lem-8-2-2-4 : ∀ {R} → zero ∶ R → R ≡ nat
lem-8-2-2-4 t-zero = refl

lem-8-2-2-5 : ∀ {t R} → succ t ∶ R → R ≡ nat × t ∶ nat
lem-8-2-2-5 (t-succ d) = refl , d

lem-8-2-2-6 : ∀ {t R} → pred t ∶ R → R ≡ nat × t ∶ nat
lem-8-2-2-6 (t-pred d) = refl , d

lem-8-2-2-7 : ∀ {t R} → iszero t ∶ R → R ≡ bool × t ∶ nat
lem-8-2-2-7 (t-iszero d) = refl , d

infix 4 _∈_

data _∈_ : Term → Term → Set where
  sub-if₁    : ∀ {t₁ t₂ t₃} → t₁ ∈ if t₁ then t₂ else t₃
  sub-if₂    : ∀ {t₁ t₂ t₃} → t₂ ∈ if t₁ then t₂ else t₃
  sub-if₃    : ∀ {t₁ t₂ t₃} → t₃ ∈ if t₁ then t₂ else t₃
  sub-succ   : ∀ {t} → t ∈ succ t
  sub-pred   : ∀ {t} → t ∈ pred t
  sub-iszero : ∀ {t} → t ∈ iszero t
  sub-trans  : ∀ {t₁ t₂ t₃} → t₁ ∈ t₂ → t₂ ∈ t₃ → t₁ ∈ t₃

sub-test : succ true ∈ if (succ (succ true)) then false else (succ zero)
sub-test = sub-trans sub-succ sub-if₁

ex-8-2-3 : ∀ {t R} → t ∶ R → ∀ s → s ∈ t → ∃ λ T → s ∶ T
ex-8-2-3 d s (sub-trans {t₂ = t′} s₁ s₂) = ex-8-2-3 (proj₂ (ex-8-2-3 d t′ s₂)) s s₁
ex-8-2-3 (t-if d _ _) _ sub-if₁ = bool , d
ex-8-2-3 {R = R} (t-if _ d _) _ sub-if₂ = R , d
ex-8-2-3 {R = R} (t-if _ _ d) _ sub-if₃ = R , d
ex-8-2-3 (t-succ d) _ sub-succ = nat , d
ex-8-2-3 (t-pred d) _ sub-pred = nat , d
ex-8-2-3 (t-iszero d) _ sub-iszero = nat , d

-- Theorem 8.2.4.
type-uniqueness : ∀ {t T₁ T₂} → t ∶ T₁ → t ∶ T₂ → T₁ ≡ T₂
type-uniqueness {true}  t-true  t-true  = refl
type-uniqueness {false} t-false t-false = refl
type-uniqueness {if _ then _ else _} (t-if _ d₁ _) (t-if _ d₂ _) = type-uniqueness d₁ d₂
type-uniqueness {zero} t-zero t-zero = refl
type-uniqueness {succ t} (t-succ _) (t-succ _) = refl
type-uniqueness {pred t} (t-pred _) (t-pred _) = refl
type-uniqueness {iszero t} (t-iszero _) (t-iszero _) = refl

derivation-uniqueness : ∀ {t T} (d₁ d₂ : t ∶ T) → d₁ ≡ d₂
derivation-uniqueness {true} t-true t-true = refl
derivation-uniqueness {false} t-false t-false = refl
derivation-uniqueness {if t₁ then t₂ else t₃} (t-if d₁ d₂ d₃) (t-if d₄ d₅ d₆)
  rewrite derivation-uniqueness d₁ d₄
        | derivation-uniqueness d₂ d₅
        | derivation-uniqueness d₃ d₆
     = refl
derivation-uniqueness {zero} t-zero t-zero = refl
derivation-uniqueness {succ t} (t-succ d₁) (t-succ d₂)
  rewrite derivation-uniqueness d₁ d₂
    = refl
derivation-uniqueness {pred t} (t-pred d₁) (t-pred d₂)
  rewrite derivation-uniqueness d₁ d₂
    = refl
derivation-uniqueness {iszero t} (t-iszero d₁) (t-iszero d₂)
  rewrite derivation-uniqueness d₁ d₂
    = refl

lem-8-3-1-1 : ∀ {v} → v ∶ bool → Value v → v ≡ true ⊎ v ≡ false
lem-8-3-1-1 t-true val = inj₁ refl
lem-8-3-1-1 t-false val = inj₂ refl
lem-8-3-1-1 (t-if d d₁ d₂) (v-num ())
lem-8-3-1-1 (t-iszero d) (v-num ())

lem-8-3-1-2 : ∀ {v} → v ∶ nat → Value v → NValue v
lem-8-3-1-2 (t-if _ _ _) (v-num ())
lem-8-3-1-2 t-zero _ = nv-zero
lem-8-3-1-2 (t-succ _) (v-num x) = x
lem-8-3-1-2 (t-pred _) (v-num ())

thm-8-3-2 : ∀ {t T} → t ∶ T → (Value t ⊎ ∃ λ t′ → t ⟶ t′)
thm-8-3-2 t-true = inj₁ v-true
thm-8-3-2 t-false = inj₁ v-false
thm-8-3-2 (t-if d _ _) with thm-8-3-2 d
thm-8-3-2 (t-if d _ _) | inj₁ x with lem-8-3-1-1 d x
thm-8-3-2 (t-if {t₂ = t₂} _ _ _) | inj₁ _ | inj₁ refl = inj₂ (t₂ , e-iftrue)
thm-8-3-2 (t-if {t₃ = t₃} _ _ _) | inj₁ _ | inj₂ refl = inj₂ (t₃ , e-iffalse)
thm-8-3-2 (t-if {t₁} {t₂} {t₃} _ _ _) | inj₂ (t₁′ , ev) = inj₂ (if t₁′ then t₂ else t₃ , e-if ev)
thm-8-3-2 t-zero = inj₁ (v-num nv-zero)
thm-8-3-2 (t-succ d) with thm-8-3-2 d
thm-8-3-2 (t-succ d) | inj₁ x = inj₁ (v-num (nv-succ (lem-8-3-1-2 d x)))
thm-8-3-2 (t-succ d) | inj₂ (t′ , ev) = inj₂ (succ t′ , e-succ ev)
thm-8-3-2 (t-pred d) with thm-8-3-2 d
thm-8-3-2 (t-pred d) | inj₁ x with lem-8-3-1-2 d x
thm-8-3-2 (t-pred d) | inj₁ x | nv-zero = inj₂ (zero , e-predzero)
thm-8-3-2 (t-pred d) | inj₁ x | nv-succ {t} v = inj₂ (t , e-predsucc v)
thm-8-3-2 (t-pred d) | inj₂ (t′ , ev) = inj₂ (pred t′ , e-pred ev)
thm-8-3-2 (t-iszero d) with thm-8-3-2 d
thm-8-3-2 (t-iszero d) | inj₁ x with lem-8-3-1-2 d x
thm-8-3-2 (t-iszero d) | inj₁ x | nv-zero = inj₂ (true , e-iszerozero)
thm-8-3-2 (t-iszero d) | inj₁ x | nv-succ v = inj₂ (false , e-iszerosucc v)
thm-8-3-2 (t-iszero d) | inj₂ (t′ , ev) = inj₂ (iszero t′ , e-iszero ev)

thm-8-3-3 : ∀ {t t′ T} → t ∶ T → t ⟶ t′ → t′ ∶ T
thm-8-3-3 t-true              ()
thm-8-3-3 t-false             ()
thm-8-3-3 (t-if d d₁ d₂)      e-iftrue         = d₁
thm-8-3-3 (t-if d d₁ d₂)      e-iffalse        = d₂
thm-8-3-3 (t-if d d₁ d₂)      (e-if ev)        = t-if (thm-8-3-3 d ev) d₁ d₂
thm-8-3-3 t-zero              ()
thm-8-3-3 (t-succ d)          (e-succ ev)      = t-succ (thm-8-3-3 d ev)
thm-8-3-3 (t-pred d)          e-predzero       = d
thm-8-3-3 (t-pred (t-succ d)) (e-predsucc x)   = d
thm-8-3-3 (t-pred d)          (e-pred ev)      = t-pred (thm-8-3-3 d ev)
thm-8-3-3 (t-iszero d)        e-iszerozero     = t-true
thm-8-3-3 (t-iszero d)        (e-iszerosucc x) = t-false
thm-8-3-3 (t-iszero d)        (e-iszero ev)    = t-iszero (thm-8-3-3 d ev)

ex-8-3-4 : ∀ {t t′ T} → t ∶ T → t ⟶ t′ → t′ ∶ T
ex-8-3-4 (t-if d d₁ d₂) e-iftrue = d₁
ex-8-3-4 (t-if d d₁ d₂) e-iffalse = d₂
ex-8-3-4 (t-if d d₁ d₂) (e-if ev) = t-if (ex-8-3-4 d ev) d₁ d₂
ex-8-3-4 (t-succ d) (e-succ ev) = t-succ (ex-8-3-4 d ev)
ex-8-3-4 (t-pred d) e-predzero = d
ex-8-3-4 (t-pred (t-succ d)) (e-predsucc x) = d
ex-8-3-4 (t-pred d) (e-pred ev) = t-pred (ex-8-3-4 d ev)
ex-8-3-4 (t-iszero d) e-iszerozero = t-true
ex-8-3-4 (t-iszero d) (e-iszerosucc x) = t-false
ex-8-3-4 (t-iszero d) (e-iszero ev) = t-iszero (ex-8-3-4 d ev)

ex-8-3-6 : ¬ ∀ {t t′ T} → t ⟶ t′ → t′ ∶ T → t ∶ T
ex-8-3-6 contra with contra {if true then true else zero} {true} {bool} e-iftrue t-true
ex-8-3-6 contra | t-if _ _ ()

ex-8-3-7 : ∀ {t v vt T} → t ∶ T → t ⇓ v [ vt ] × v ∶ T
ex-8-3-7 d = {!!}