recursive function does not get unfolded

Stream: lean4

[Tomas Skrivan]

I have this recursive function

def progress : ∀ (M : ∅ ⊢ A), Progress M
  | (# x) => by contradiction
  | (ƛ N) => done Value.lambda
  | (L ⬝ M) =>
      match progress L with
        | step L_to_L' => step (xi_app_1 L_to_L')
        | done v =>
            match progress M with
              | step M_to_M' => step (xi_app_2 v M_to_M')
              | done w =>
                  match v with
                    | Value.lambda => step (beta w)
  | o => done Value.zero
  | (M +1) =>
      match progress M with
        | step M_to_M' => step (xi_succ M_to_M')
        | done v => done (Value.succ v)
  | (switch L M N) =>
      match progress L with
        | step L_to_L' => step (xi_case L_to_L')
        | done v =>
            match v with
              | Value.zero => step beta_zero
              | Value.succ v => step (beta_succ v)
  | (μ N) => step beta_mu

I'm confused why

example : progress o = done Value.zero := by rfl

does not work. It works if I mark the function with abbrev.

mwe

code

import Lean
namespace Hoskinson

set_option pp.notation true
set_option pp.rawOnError true
set_option hygiene false
set_option maxRecDepth 1000000
set_option maxHeartbeats 1000000

inductive Tp : Type where
| natural : Tp
| function : Tp → Tp → Tp

notation:max "ℕ" => Tp.natural
infixr:70 "⇒" => Tp.function

example : Tp := ℕ ⇒ ℕ

inductive TpEnv : Type where
| empty : TpEnv
| extend : TpEnv → Tp → TpEnv

notation:max "∅" => TpEnv.empty
infixl:50 "▷" => TpEnv.extend

example : TpEnv := ∅ ▷ ℕ ⇒ ℕ ▷ ℕ

infix:40  "∋" => lookup

inductive lookup : TpEnv → Tp → Type where
  | stop :
       ----------------
       Γ ▷ A ∋ A
  | pop :
       Γ ∋ B
       ----------------
     → Γ ▷ A ∋ B
  deriving Repr

prefix:90 "S" => lookup.pop
notation:max "Z" => lookup.stop

infix:40  "⊢" => term

inductive term : TpEnv → Tp → Type where
  | var :
        Γ ∋ A
        ----------
      → Γ ⊢ A
  | lambda :
        Γ ▷ A ⊢ B
        -----------
      → Γ ⊢ A ⇒ B
  | application :
        Γ ⊢ A ⇒ B
      → Γ ⊢ A
        --------
      → Γ ⊢ B
  | zero :
        --------
        Γ ⊢ ℕ
  | succ :
        Γ ⊢ ℕ
        --------
      → Γ ⊢ ℕ
  | case :
        Γ ⊢ ℕ
      → Γ ⊢ A
      → Γ ▷ ℕ ⊢ A
        ---------------
      → Γ ⊢ A
  | mu :
        Γ ▷ A ⊢ A
        --------------
      → Γ ⊢ A
  deriving Repr

prefix:90 "#" => term.var
prefix:50 "ƛ" => term.lambda
infixl:70 "⬝" => term.application
notation:max "o" => term.zero
postfix:80 "+1" => term.succ
notation:max "switch" => term.case
prefix:50 "μ" => term.mu

def suc_c : Γ ⊢ ℕ ⇒ ℕ :=
  ƛ (# Z +1)

def rmap (Γ Δ : TpEnv) : Type :=
  ∀ {A : Tp}, (Γ ∋ A) → (Δ ∋ A)

def smap (Γ Δ : TpEnv) : Type :=
  ∀ {A : Tp}, (Γ ∋ A) → (Δ ⊢ A)

def tmap (Γ Δ : TpEnv) : Type :=
  ∀ {A : Tp}, (Γ ⊢ A) → (Δ ⊢ A)

infix:30 "→ʳ" => rmap
infix:30 "→ˢ" => smap
infix:30 "→ᵗ" => tmap

def ren_ext {Γ Δ : TpEnv} {A :Tp} (ρ : Γ →ʳ Δ) : (Γ ▷ A →ʳ Δ ▷ A)
  | _ , Z  =>  Z
  | _ , S x  =>  S (ρ x)

def ren {Γ Δ : TpEnv} (ρ : Γ →ʳ Δ) : Γ →ᵗ Δ
  | _ , (# x) => # (ρ x)
  | _ , (ƛ N) => ƛ (ren (ren_ext ρ) N)
  | _ , (L ⬝ M) => ren ρ L ⬝ ren ρ M
  | _ , o => o
  | _ , M +1 => ren ρ M +1
  | _ , switch L M N =>
        switch (ren ρ L) (ren ρ M) (ren (ren_ext ρ) N)
  | _ , μ N => μ (ren (ren_ext ρ) N)

def lift {Γ : TpEnv} {A : Tp} : Γ →ᵗ Γ ▷ A := ren (fun x => S x)

def sub_ext {Γ Δ : TpEnv} {A : Tp} (σ : Γ →ˢ Δ) : (Γ ▷ A →ˢ Δ ▷ A)
  | _ , Z  =>  # Z
  | _ , S x  =>  lift (σ x)

def sub {Γ Δ : TpEnv} (σ : Γ →ˢ Δ) : Γ →ᵗ Δ
  | _ , (# x) => σ x
  | _ , (ƛ N) => ƛ (sub (sub_ext σ) N)
  | _ , (L ⬝ M) => sub σ L ⬝ sub σ M
  | _ , o => o
  | _ , M +1 => sub σ M +1
  | _ , switch L M N =>
        switch (sub σ L) (sub σ M) (sub (sub_ext σ) N)
  | _ , μ N => μ (sub (sub_ext σ) N)

def sigma_0 (M : Γ ⊢ A) : Γ ▷ A →ˢ Γ
  | _ , Z    =>  M
  | _ , S x  =>  # x

def subst {Γ : TpEnv} {A B : Tp} (N : Γ ▷ A ⊢ B) (M : Γ ⊢ A) : Γ ⊢ B
  := sub (sigma_0 M) N

example : subst (ƛ (# S Z ⬝ (# S Z ⬝ # Z))) suc_c = (ƛ (suc_c ⬝ (suc_c ⬝ # Z)) : ∅ ⊢ ℕ ⇒ ℕ) := rfl

inductive Value : Γ ⊢ A → Type where
  | lambda :
      Value (ƛ N)
  | zero :
      Value o
  | succ :
      Value V → Value (V +1)
  deriving Repr

inductive reduce : Γ ⊢ A → Γ ⊢ A → Type where
  | xi_app_1 :
      reduce L L' → reduce (L ⬝ M) (L' ⬝ M)
  | xi_app_2 :
      Value V → reduce M M' → reduce (V ⬝ M) (V ⬝ M')
  | beta :
      Value W → reduce ((ƛ N) ⬝ W) (subst N W)
  | xi_succ :
      reduce M M' → reduce (M +1) (M' +1)
  | xi_case :
      reduce L L' → reduce (switch L M N) (switch L' M N)
  | beta_zero :
      reduce (switch o M N) M
  | beta_succ :
      Value V → reduce (switch (V +1) M N) (subst N V)
  | beta_mu :
      reduce (μ N) (subst N (μ N))
  deriving Repr

open reduce

infix:20 "~>" => reduce


inductive Progress : Γ ⊢ A → Type where
  | step :
      (M ~> N) → Progress M
  | done :
      Value V → Progress V
  deriving Repr

open Progress

def progress : ∀ (M : ∅ ⊢ A), Progress M
  | (# x) => by contradiction
  | (ƛ N) => done Value.lambda
  | (L ⬝ M) =>
      match progress L with
        | step L_to_L' => step (xi_app_1 L_to_L')
        | done v =>
            match progress M with
              | step M_to_M' => step (xi_app_2 v M_to_M')
              | done w =>
                  match v with
                    | Value.lambda => step (beta w)
  | o => done Value.zero
  | (M +1) =>
      match progress M with
        | step M_to_M' => step (xi_succ M_to_M')
        | done v => done (Value.succ v)
  | (switch L M N) =>
      match progress L with
        | step L_to_L' => step (xi_case L_to_L')
        | done v =>
            match v with
              | Value.zero => step beta_zero
              | Value.succ v => step (beta_succ v)
  | (μ N) => step beta_mu


example : progress o = done Value.zero := by rfl -- fails
example : progress o = done Value.zero := by dsimp[progress] -- fails
example : progress o = done Value.zero := by unfold progress; rfl -- works
example : progress o = done Value.zero := by simp[progress] -- works

[Tomas Skrivan]

cc @Philip Wadler

[Yan Yablonovskiy]

(deleted)

[Kyle Miller]

If you #print progress and then #print progress._unary, you can see that it's using WellFounded.fix, so it's well-founded recursion. Definitions using well-founded recursion are irreducible.

Here's this week's discussion about the issue: #lean4 > opaque recursion definitions break mergeSort decidability @ 💬

[Tomas Skrivan]

Nice, I was wondering if it has something to do with well-founded recursion but had no idea how to check it.