Lean 中如何在 tactic 模式或 match 表达式内实现函数的递归自调用

开发者在Lean中实现带大小索引的栈数据结构sstack时，需要编写sget'函数完成指定索引位置的元素读取，在两种实现思路下均遇到递归调用报unknown identifier sget'的问题：

尝试1：tactic块实现 #

对应代码如下：

def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
begin
  cases n with n0 nn,
  begin
    have f : false, from nat.lt_asymm h1 h1,
    tauto,
  end,
  induction s,
  cases s_val,
  begin
    have : stack.empty.size = 0, from @stack_size_0 α,
    tauto,
  end,
  cases i with i0 ri,
  exact s_val_x,
  exact sget' (pred i) s_val_s,
end

尝试2：match表达式实现 #

对应代码如下：

def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
match i, s with
  | 0, ⟨stack.push x s, _⟩ := x
  | i, ⟨stack.push _ s, _⟩ := sget' (pred i) ⟨s, _⟩
  | _, ⟨stack.empty, _⟩    := sorry  -- just ignore this

Lean对递归函数的自调用有严格的作用域绑定规则：如果函数定义没有显式触发递归注册流程，当前函数的标识符不会被注入到自身函数体的作用域内，直接调用就会触发未知标识符错误。
之前的两种写法都没有满足递归注册的触发条件：

• tactic块实现中，普通的begin...end块是独立的作用域，没有在块内绑定当前递归函数的引用，裸写sget'自然无法被识别
• match表达式实现中，因为函数签名把隐参数全部前置，没有把作为递归测度的参数（i、栈的结构值）放到def定义后的递归匹配位置，Lean不会自动开启递归注册流程，也就不会把函数名放进match分支的作用域

match表达式场景 #

需要调整def的签名结构，把作为递归测度的参数紧跟在函数类型声明后，触发Lean的结构化递归注册流程，让函数标识符自动注入到match分支作用域：

def sget' {α : Type} : 
  {n : ℕ} → (i : ℕ) → {h1 : n > 0} → {h2 : i < n} → sstack α n → α
| 0 ⟨stack.push x s, _⟩ := x
| (i+1) ⟨stack.push _ s, hsize⟩ := sget' i ⟨s, _⟩

这种写法下，Lean会自动识别递归分支中入参i从i+1降到i的递减关系，完成递归合法性校验，同时把当前函数名放入分支作用域，不会报未知标识符错误。

tactic块场景 #

不能在普通tactic块中直接调用全局的sget'标识符，需要通过fix tactic显式绑定递归函数的本地引用，再完成tactic推导：

def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
begin
  fix f : {n' : ℕ} → (i' : ℕ) → {h1' : n' > 0} → {h2' : i' < n'} → sstack α n' → α,
  -- 后续所有递归调用直接使用绑定的本地引用f，而非全局未完成定义的sget'
  cases n with n0 nn,
  { have f : false, from nat.lt_asymm h1 h1, tauto },
  induction s,
  cases s_val,
  { have : stack.empty.size = 0, from @stack_size_0 α, tauto },
  cases i with i0 ri,
  { exact s_val_x },
  { exact f (pred i) s_val_s },
end

开发者提到在模式守卫场景下可以正常完成递归调用，本质是因为带守卫的match写法会自动触发Lean的递归注册流程，将当前函数名注入分支作用域，并非守卫语法本身有特殊的标识符权限。 #

内容的提问来源于stack exchange，提问作者Daniil Kolesnichenko