PreservationCounterexample.agda

open import Data.Nat
open import Data.Sum
open import Data.Product
open import Relation.Nullary

module PreservationCounterexample
  where

data Type : Set where
  Boolean : Type
  Nat : Type

data Expr : Set where
  mult : Expr → Expr → Expr
  sub : Expr → Expr → Expr
  true : Expr
  false : Expr
  nat : ℕ → Expr

data _⦂_ : Expr → Type → Set where
  T-mult : ∀ {a b} →
    a ⦂ Nat →
    b ⦂ Nat →
    ----
    mult a b ⦂ Nat

  T-sub : ∀ {a b} →
    a ⦂ Nat →
    b ⦂ Nat →
    ----
    sub a b ⦂ Nat

  T-true :
    ----
    true ⦂ Boolean

  T-false :
    ----
    false ⦂ Boolean

  T-nat : ∀ {n} →
    ----
    nat n ⦂ Nat

data _⟶_ : Expr → Expr → Set where

  -- The bad evaluation rule:
  E-mult : ∀ {a b} →
    ----
    mult a b ⟶ true

  E-sub : ∀ {x y} →
    ----
    sub (nat x) (nat y) ⟶ nat (x + y)

  E-sub-1 : ∀ {a a′ b} →
    a ⟶ a′ →
    ----
    sub a b ⟶ sub a′ b

  E-sub-2 : ∀ {a b b′} →
    b ⟶ b′ →
    ----
    sub a b ⟶ sub a b′

data Value : Expr → Set where
  V-nat : ∀ {n} →
    ----
    Value (nat n)

  V-true :
    ----
    Value true

  V-false :
    ----
    Value false

progress : ∀ {a t} →
  a ⦂ t →
  Value a ⊎ (∃[ a′ ] (a ⟶ a′))
progress (T-mult a-typed b-typed) = inj₂ (true , E-mult)
progress (T-sub a-typed b-typed) with progress a-typed | progress b-typed
... | inj₁ (V-nat {x}) | inj₁ (V-nat {y}) = inj₂ (nat (x + y) , E-sub)
... | inj₁ x | inj₂ (fst , snd) = inj₂ (sub _ fst , E-sub-2 snd)
... | inj₂ (fst , snd) | inj₁ x = inj₂ (sub fst _ , E-sub-1 snd)
... | inj₂ (fst , snd) | inj₂ y₁ = inj₂ (sub fst _ , E-sub-1 snd)
progress T-true = inj₁ V-true
progress T-false = inj₁ V-false
progress T-nat = inj₁ V-nat

-- This becomes ill-typed in one step
example : Expr
example = sub (nat 5) (mult (nat 1) (nat 2))

-- It starts out well-typed...
example-well-typed :
  example ⦂ Nat
example-well-typed = T-sub T-nat (T-mult T-nat T-nat)

-- ... but then it steps to this expression:
ill-typed : Expr
ill-typed = sub (nat 5) true

ill-typed-step : example ⟶ ill-typed
ill-typed-step = E-sub-2 E-mult

¬preservation : ¬ ∀ {a b t} →
  a ⦂ t →
  a ⟶ b →
  b ⦂ t
¬preservation f
  with
    f {example}
      {ill-typed}
      {Nat}
      (T-sub T-nat (T-mult T-nat T-nat))
      ill-typed-step
... | T-sub x ()

-- Even though we have progress and the initial example expression type checks,
-- once we have evaluated it one step we can no longer take a step:
ill-typed-example-errors :
  ¬ (∃[ b ] (ill-typed ⟶ b))
ill-typed-example-errors (.(sub _ true) , E-sub-1 ())
ill-typed-example-errors (.(sub (nat 5) _) , E-sub-2 ())

-- But it's also not a value:
¬ill-typed-example-value : ¬ Value ill-typed
¬ill-typed-example-value ()