如何在Lean4中内联证明1+1=2？解决类型匹配报错

问题原因 #

你的两段代码差异源于Lean类型检查器的化简时机和Eq.refl的行为：

• Eq.refl _会根据传入的表达式生成x = x形式的证明。在第一段代码的have语句中，占位符_被推断为1+1，因此生成的证明类型是1+1=1+1，而类型检查器此时不会自动将1+1化简为2，导致与目标类型1+1=2不匹配。
• 当单独定义plus11定理时，Lean在处理定理类型1+1=2时会进行定义相等的化简，识别到1+1和2是定义等价的，因此Eq.refl _能正确匹配目标类型。

内联解决方案（无需外部定理或tactic） #

利用rfl证明项即可直接内联完成1+1=2的证明。rfl专门用于证明定义相等的等式（即两个表达式展开后完全相同），而1+1和2恰好满足这一点：

写法1：带have语句 #

def even (n : Nat) : Prop := ∃(m:Nat), m+m=n

theorem even2 : even 2 :=
  have e : 1+1=2 := rfl
  ⟨1,e⟩

写法2：直接内联 #

def even (n : Nat) : Prop := ∃(m:Nat), m+m=n

theorem even2 : even 2 := ⟨1, rfl⟩

补充说明 #

如果一定要用Eq.refl，可以显式指定目标值并通过类型转换，但这种写法不如rfl简洁：

def even (n : Nat) : Prop := ∃(m:Nat), m+m=n

theorem even2 : even 2 :=
  have e : 1+1=2 := Eq.refl 2 : 1+1=2
  ⟨1,e⟩

这里通过: 1+1=2强制指定证明的类型，Lean会识别到1+1和2的定义相等，因此接受这个转换。

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