Tiny lambda calculus extended with Fix combinators, unit, pair, and sum values

Tiny.lean

-- One argument operations with strict evaluation strategy
inductive UnOp : Type :=
  | ufst                                     : UnOp -- first element of the pair
  | usnd                                     : UnOp -- second element of the pair
  | umkl                                     : UnOp -- left constructor of either type
  | umkr                                     : UnOp -- right constructor of either type
  deriving DecidableEq

open UnOp

-- Two argument operations with strict evaluation strategy
inductive BinOp : Type :=
  | bapp                                     : BinOp -- λ-application
  | bmkp                                     : BinOp -- pair constructor
  deriving DecidableEq

open BinOp

-- Type family of expressions indexed by size of external context
inductive Expr : Nat → Type :=
  | evar (m : Nat) (_: m < n)                : Expr n -- de-brujin indexed variable
  | emku (n : Nat)                           : Expr n -- element of the unit type
  | euop (u : UnOp) (e : Expr n)             : Expr n -- unary operation
  | ebop (b : BinOp) (e₁ e₂ : Expr n)        : Expr n -- binary operation
  | eabs (e : Expr (n + 1))                  : Expr n -- λ-abstraction
  | elet (e₁ : Expr n) (e₂ : Expr (n + 1))   : Expr n -- let e₁ in e₂ (e₂ can refer to e₁ with evar)
  | ecas (e : Expr n) (e₁ e₂ : Expr (n + 1)) : Expr n -- case statement on sum type (encoded as two lambdas)
  | efix (e : Expr (n + 1))                  : Expr n -- fix combinator
  deriving DecidableEq

open Expr

-- Cast `Expr n` to `Expr m` provided that `n = m`
def Expr.castEq (e : Expr n) (h : n = m) : Expr m := cast (congrArg Expr h) e

-- Left-extend `Expr n` to `Expr (n + 1)`
def Expr.leftExtend (e : Expr n) : Expr (n + 1) :=
  match e with
  | evar m m_lt_n   => evar m (Nat.lt_trans m_lt_n (Nat.lt_succ_self n))
  | emku _          => emku (n + 1)
  | euop u e        => euop u (e.leftExtend)
  | ebop b e₁ e₂    => ebop b (e₁.leftExtend) (e₂.leftExtend)
  | eabs e          => eabs (e.leftExtend)
  | elet e₁ e₂      => elet (e₁.leftExtend) (e₂.leftExtend)
  | ecas e e₁ e₂    => ecas (e.leftExtend) (e₁.leftExtend) (e₂.leftExtend)
  | efix e          => efix (e.leftExtend)

-- Some expressions that have reached final state are values
inductive Value : Expr 0 → Prop :=
  | vmku : Value (emku 0)                                -- unit-type elements are values
  | vmkp : Value e₁ → Value e₂ → Value (ebop bmkp e₁ e₂) -- pairs are values
  | vmkl : Value e → Value (euop umkl e)                 -- left sum type constructors are values
  | vmkr : Value e → Value (euop umkr e)                 -- right sum type constructors are values
  | vabs : Value (eabs e)                                -- all functions are values

-- Decide if expression is a value
def Expr.decideIsValue (e : Expr 0) : Decidable (Value e) := 
  match e with
  | evar m m_lt_n    => isFalse (by intro h; cases h)
  | emku _           => isTrue Value.vmku
  | euop u e         => match Expr.decideIsValue e with
                        | isTrue h =>
                          match u with
                          | umkl => isTrue (Value.vmkl h)
                          | umkr => isTrue (Value.vmkr h)
                          | ufst => isFalse (by intro h; contradiction)
                          | usnd => isFalse (by intro h; contradiction)
                        | isFalse h => isFalse (by intro h; cases h; repeat {contradiction})
  | ebop b e₁ e₂     => match Expr.decideIsValue e₁ with
                        | isTrue h₁ => 
                          match Expr.decideIsValue e₂ with
                          | isTrue h₂ =>
                            match b with
                            | bapp => isFalse (by intro h; contradiction)
                            | bmkp => isTrue (Value.vmkp h₁ h₂)
                          | isFalse h₂ => isFalse (by intro h; cases h; repeat {contradiction})
                        | isFalse h₂ => isFalse (by intro h; cases h; repeat {contradiction})
  | eabs e           => isTrue Value.vabs
  | elet e₁ e₂       => isFalse (by intro h; cases h)
  | ecas e e₁ e₂     => isFalse (by intro h; cases h)
  | efix e           => isFalse (by intro h; cases h)

-- Derive decidable instance using decideIsValue method
instance Expr.isValueDec (e : Expr 0) : Decidable (Value e) := Expr.decideIsValue e

-- Perform substitution
def Expr.subst (e₁ : Expr (n + 1)) (e₂ : Expr n) : Expr n :=
  match e₁ with
  | evar m m_lt_n    => if h : m = n then e₂ else evar m (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ m_lt_n) h)
  | emku _           => emku n
  | euop u e         => euop u (e.subst e₂)
  | ebop b e₁₁ e₁₂   => ebop b (e₁₁.subst e₂) (e₁₂.subst e₂)
  | eabs e₁          => eabs (e₁.subst e₂.leftExtend)
  | elet e₁₁ e₁₂     => elet (e₁₁.subst e₂) (e₁₂.subst e₂.leftExtend)
  | ecas e₁ e₁₁ e₁₂  => ecas (e₁.subst e₂) (e₁₁.subst e₂.leftExtend) (e₁₂.subst e₂.leftExtend)
  | efix e₁          => efix (e₁.subst e₂.leftExtend)

-- Small-step semantics for Expr
inductive SmallStep : Expr 0 → Expr 0 → Prop
  | uopNext  : SmallStep e e' → SmallStep (euop u e) (euop u e')
  | bopLeft  : SmallStep e₁ e₁' → SmallStep (ebop b e₁ e₂) (ebop b e₁' e₂)
  | bopRight : Value e₁ → SmallStep e₂ e₂' → SmallStep (ebop b e₁ e₂) (ebop b e₁ e₂')
  | appApply : Value (eabs e₁) → Value e₂ → SmallStep (ebop bapp (eabs e₁) e₂) (e₁.subst e₂)
  | letLeft  : SmallStep e₁ e₁' → SmallStep (elet e₁ e₂) (elet e₁' e₂)
  | letApply : Value e₁ → SmallStep (elet e₁ e₂) (e₂.subst e₁)
  | fstApply : Value (ebop bmkp e₁ e₂) → SmallStep (euop ufst (ebop bmkp e₁ e₂)) e₁
  | sndApply : Value (ebop bmkp e₁ e₂) → SmallStep (euop usnd (ebop bmkp e₁ e₂)) e₂
  | casNext  : SmallStep e e' → SmallStep (ecas e e₁ e₂) (ecas e' e₁ e₂)
  | casFst   : Value (euop umkl e) → SmallStep (ecas (euop umkl e) e₁ e₂) (e₁.subst e)
  | casSnd   : Value (euop umkr e) → SmallStep (ecas (euop umkr e) e₁ e₂) (e₂.subst e)
  | fixApply : SmallStep (efix e) (e.subst (efix e))

-- Value e implies termination of e
theorem Value.noStep {e : Expr 0} (e' : Expr 0) (v : Value e) : ¬SmallStep e e' := by
  intro h
  cases v with
  | vmku => cases h
  | @vmkp e₁ e₂ v₁ v₂ => cases h with
    | @bopLeft _ e₁' _ _ s => exact (Value.noStep e₁' v₁) s
    | @bopRight _ _ e₂' _ _ s => exact (Value.noStep e₂' v₂) s
  | @vmkl e v' => cases h with
    | @uopNext _ e₂ _ s => exact (Value.noStep e₂ v') s
  | @vmkr e v' => cases h with
    | @uopNext _ e₂ _ s => exact (Value.noStep e₂ v') s
  | vabs => cases h

-- Small step implies not being a value
theorem SmallStep.noValue {e e' : Expr 0} (s : SmallStep e e') : ¬Value e := by
  intro h; exact (Value.noStep e' h) s

-- Executable small-step semantics
def Expr.step : Expr 0 → Option (Expr 0)
  | evar m m_lt_n    => ((Nat.not_lt_zero m) m_lt_n).elim
  | emku _           => Option.none
  | euop u e         => if Value e then
                          match u with
                          | ufst =>
                            match e with
                            | ebop bmkp e₁ _ => Option.some e₁ 
                            | _              => Option.none
                          | usnd =>
                            match e with
                            | ebop bmkp _ e₂ => Option.some e₂ 
                            | _              => Option.none
                          | umkl => Option.none
                          | umkr => Option.none
                        else e.step.map (λ e' => euop u e')
  | ebop b e₁ e₂     => if Value e₁ then
                          if Value e₂ then
                            match b with
                            | bapp =>
                              match e₁ with
                              | eabs e₁' => Option.some (e₁'.subst e₂)
                              | _        => Option.none
                            | bmkp => Option.none
                          else e₂.step.map (λ e₂' => ebop b e₁ e₂')
                        else e₁.step.map (λ e₁' => ebop b e₁' e₂)
  | eabs _           => Option.none
  | elet e₁ e₂       => if Value e₁ then Option.some (e₂.subst e₁) else e₁.step.map (λ e₁ => elet e₁ e₂)
  | ecas e e₁ e₂     => if Value e then
                          match e with
                          | euop umkl e => Option.some (e₁.subst e)
                          | euop umkr e => Option.some (e₂.subst e)
                          | _           => Option.none
                        else e.step.map (λ e => ecas e e₁ e₂)
  | efix e           => Option.some (e.subst (efix e))

-- If Expr.step steps, SmallStep also will
theorem Expr.small_step_of_step {e e' : Expr 0} (h : Expr.step e = Option.some e') : SmallStep e e' := by
  unfold Expr.step at h
  unfold Option.map at h
  cases e with
  | evar m m_lt_n => exact ((Nat.not_lt_zero m) m_lt_n).elim
  | emku _ => simp [*] at h
  | euop u e =>
      cases e.isValueDec with
      | isTrue h₁ =>
        cases u with
        | ufst =>
          cases e with
          | ebop b e₁ e₂ =>
            cases b with
            | bmkp => simp [*] at h; rw [←h]; exact SmallStep.fstApply h₁
            | _ => simp [*] at h
          | _ => simp [*] at h
        | usnd =>
          cases e with
          | ebop b e₁ e₂ =>
            cases b with
            | bmkp => simp [*] at h; rw [←h]; exact SmallStep.sndApply h₁
            | _ => simp [*] at h
          | _ => simp [*] at h
        | umkl => simp [*] at h
        | umkr => simp [*] at h
      | isFalse h₁ =>
        simp [*] at h
        cases h₂ : step e with
        | some e' => simp [*] at h; rw [←h]; exact SmallStep.uopNext (Expr.small_step_of_step h₂)
        | none => simp [*] at h
  | ebop b e₁ e₂ =>
    cases e₁.isValueDec with
    | isTrue h₁ =>
      cases e₂.isValueDec with
      | isTrue h₂ =>
        cases b with
        | bapp =>
          simp [*] at h
          cases h₁' : e₁ with
          | eabs e₁' => rw [h₁'] at h; simp [*] at h; rw [←h]; rw [h₁'] at h₁; exact SmallStep.appApply h₁ h₂
          | _ => simp [*] at h
        | bmkp => simp [*] at h
      | isFalse h₂ =>
        simp [*] at h;
        cases h'' : step e₂ with
        | some e₂' =>
          rw [h''] at h; simp [*] at h; rw [←h]
          exact SmallStep.bopRight h₁ (Expr.small_step_of_step h'')
        | none => simp [*] at h
    | isFalse h₁ =>
      simp [*] at h
      cases h'' : step e₁ with
      | some e₁' =>
        rw [h''] at h; simp [*] at h; rw [←h]
        exact SmallStep.bopLeft (Expr.small_step_of_step h'')
      | none => simp [*] at h
  | eabs e' => simp [*] at h
  | elet e₁ e₂ =>
    simp at h
    cases e₁.isValueDec with
    | isTrue h₁ => simp [*] at h; rw [←h]; exact SmallStep.letApply h₁
    | isFalse h₁ =>
      simp [*] at h;
      cases h'' : step e₁ with
      | some e₁' =>
        rw [h''] at h; simp [*] at h; rw [←h]
        exact SmallStep.letLeft (Expr.small_step_of_step h'')
      | none => simp [*] at h
  | ecas e e₁ e₂ =>
    cases e.isValueDec with
    | isTrue h' =>
      cases e with
      | euop u e' =>
        cases u with
        | umkl => simp [*] at h; rw [←h]; exact SmallStep.casFst h'
        | umkr => simp [*] at h; rw [←h]; exact SmallStep.casSnd h'
        | _ => simp [*] at h
      | _ => simp [*] at h
    | isFalse h' =>
      simp [*] at h
      cases h'' : step e with
      | some e' => simp [*] at h; rw [←h]; exact SmallStep.casNext (Expr.small_step_of_step h'')
      | none => simp [*] at h
  | efix e => simp [*] at h; rw [←h]; exact SmallStep.fixApply

-- If SmallStep steps, Expr.step also will
theorem Expr.step_of_small_step {e e' : Expr 0} (h : SmallStep e e') : (Expr.step e = Option.some e') := by
  unfold Expr.step
  unfold Option.map
  cases h with
  | @uopNext e e' u s =>
    let h := Expr.step_of_small_step s
    let h' := s.noValue
    simp [*]
  | @bopLeft e₁ e₁' b e₂ s₁ =>
    let h' := s₁.noValue
    simp [*]
    rw [Expr.step_of_small_step s₁]
  | @bopRight e₁ e₂ e₂' b v₁ s₂ =>
    let h := Expr.step_of_small_step s₂
    let h' := s₂.noValue
    simp [*]
  | @appApply => simp [*]
  | @letLeft e₁ e₁' e₂ s₁ =>
    let h := Expr.step_of_small_step s₁
    let h' := s₁.noValue
    simp [*]
  | @letApply => simp [*]
  | @fstApply => simp [*]
  | @sndApply => simp [*]
  | @casNext e e' e₁ e₂ s =>
    let h := Expr.step_of_small_step s
    let h' := s.noValue
    simp [*]
  | @casFst => simp [*]
  | @casSnd => simp [*]
  | @fixApply => simp [*]

-- Two-way theorem that sums up two theorems above - Expr.step only steps when SmallStep does
theorem Expr.step_is_small_step : SmallStep e e' ↔ Expr.step e = Option.some e' := by
  apply Iff.intro
  exact Expr.step_of_small_step
  exact Expr.small_step_of_step

-- Small step is, in fact, determenistic
theorem SmallStep.deterministic : SmallStep e e₁ → SmallStep e e₂ → e₁ = e₂ := by
  intro s₁ s₂
  rw [@Expr.step_is_small_step e e₁] at s₁
  rw [@Expr.step_is_small_step e e₂, s₁] at s₂
  simp at s₂
  exact s₂

-- We can actually decide SmallStep relation
instance SmallStep.decidable (e e' : Expr 0) : Decidable (SmallStep e e') :=
  if h : e' = e.step
    then isTrue (Expr.small_step_of_step (Eq.symm h))
    else isFalse (by
      rw [Expr.step_is_small_step]
      intro h'
      let h'' := Eq.symm h'
      exact h h'')