Lean4中包装Fin n的Idx为何需termination_by？求示例优化

你遇到的问题核心在于Lean的终止检查器对原始类型和自定义类型的处理差异：

问题代码对比 #

使用自定义包装类型Idx n时必须显式指定termination_by：

import Mathlib.Tactic.Linarith

def Idx (n:Nat) := Fin n

def sum(k:Idx n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Idx n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum km1)
  termination_by sum k => k.val

直接使用Fin n时无需声明：

def sum2(k:Fin n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Fin n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum2 km1)

原因解释 #

Lean的终止检查器对**原始类型Fin**有内置的优化逻辑：它默认知道Fin的val字段是衡量实例大小的关键，并且能自动识别递归调用中km1.val严格小于k.val，从而判定递归会终止。

但你定义的Idx n是Fin n的非透明类型别名，Lean不会自动将Fin的内置规则迁移到自定义类型上。终止检查器无法直接推断出Idx实例之间的大小递减关系，因此必须显式通过termination_by指定用k.val作为终止度量。

优化方案 #

方案1：让Idx成为透明别名

给Idx添加@[reducible]注解，让Lean将其视为Fin n的透明别名，这样终止检查器就能复用Fin的内置逻辑，无需手动声明termination_by：

import Mathlib.Tactic.Linarith

@[reducible] def Idx (n:Nat) := Fin n

def sum(k:Idx n) : Nat :=
  if p:k.val=0 then 0
  else
    have p : k.val-1 < k.val := (Nat.pred_lt p);
    let km1 : Idx n := {val:=k.val-1,isLt:=(by linarith [k.isLt])};
    1+(sum km1)

方案2：使用Fin的内置递归器

直接用Fin.recOn替代手动的条件判断和实例构造，Lean的内置递归器自带终止保证，代码更简洁：

import Mathlib.Tactic.Linarith

def Idx (n:Nat) := Fin n

def sum(k:Idx n) : Nat :=
  Fin.recOn k (fun _ => 0) (fun val _ ih => 1 + ih)

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