在Lean中证明互递归良基性：互归纳类型递归定义报错解决方案

针对你遇到的不同参数数量互归纳类型定义互递归时的良基性报错，可以按以下步骤解决：

方法1：手动统一输入类型并指定良基关系 #

这是最通用的解决方案，核心是把所有互递归的输入统一包裹到同一个类型中，再基于语法树大小定义良基序：

1. 定义包裹类型统一覆盖所有互归纳类型的实例：

inductive TermWrapper : Type
| wrapCBlockList : ∀ Γ locals out, CBlockList Γ locals out → TermWrapper
| wrapBlock : ∀ Γ locals, Block Γ locals → TermWrapper
| wrapSwitchBody : ∀ Γ locals, SwitchBody Γ locals → TermWrapper
| wrapCExpr : ∀ Γ locals n, CExpr Γ locals n → TermWrapper
| wrapCStatement : ∀ Γ locals out, CStatement Γ locals out → TermWrapper

2. 基于Lean自动生成的互归纳类型sizeof属性定义度量函数，自然数序天然是良基的：

def termSize : TermWrapper → ℕ
| .wrapCBlockList _ _ _ t => sizeof t
| .wrapBlock _ _ t => sizeof t
| .wrapSwitchBody _ _ t => sizeof t
| .wrapCExpr _ _ _ t => sizeof t
| .wrapCStatement _ _ _ t => sizeof t

3. 定义互递归函数时用using_well_founded手动指定良基关系：

mutual
-- 替换为你自己的互递归函数实现
def checkCBlockList : ∀ Γ locals out, CBlockList Γ locals out → Prop
| Γ, l, o, b => /- 函数逻辑 -/
with checkBlock : ∀ Γ locals, Block Γ locals → Prop
| Γ, l, b => /- 函数逻辑 -/
with checkSwitchBody : ∀ Γ locals, SwitchBody Γ locals → Prop
| Γ, l, b => /- 函数逻辑 -/
with checkCExpr : ∀ Γ locals n, CExpr Γ locals n → Prop
| Γ, l, n, e => /- 函数逻辑 -/
with checkCStatement : ∀ Γ locals out, CStatement Γ locals out → Prop
| Γ, l, o, s => /- 函数逻辑 -/
end
using_well_founded { 
  rel := InvImage termSize (· < ·), 
  wf := InvImage.wf (· < ·) Nat.lt_wfRel.2 
}

如果Lean无法自动证明递归调用满足递减要求，在对应调用位置用decreasing_by策略补全子项sizeof小于父项的证明即可，互归纳类型的子项sizeof天然小于父项，证明复杂度很低。

方法2：简化参数的SizeOf实例（快速解决） #

你遇到的报错很大概率是因为set Identifier没有默认的SizeOf实例，导致Lean无法计算默认度量。你可以手动给不影响递归深度的参数类型设置固定大小：

-- 上下文、标识符集合都不影响语法树递归深度，统一设置sizeOf为0
instance : SizeOf FTContext where
  sizeOf _ := 0

instance : SizeOf (set Identifier) where
  sizeOf _ := 0

添加这两个实例后，Lean默认的良基关系推导逻辑就可以正确计算语法树的递归深度，大部分情况下可以直接解决报错，不需要额外手写包裹类型和良基证明。

深度函数的定义问题 #

你之前定义深度函数时遇到的同样报错，本质也是输入类型不统一导致的良基关系推导失败，使用上述任意一种方法后，都可以正常定义深度函数。

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