Lean 4无效字段符号问题咨询：#check Or.intro_left触发报错

为什么会出现这个错误？ #

这个问题的本质是Lean 4对字段符号（.语法）的使用限制：.只能用来访问类型构造器（比如归纳类型、结构这类常量构造器）的成员，而你本地环境中的Or是一个普通的函数类型（Prop → Prop → Prop），并非Lean标准库中默认的归纳类型构造器。

当你尝试用Or.intro_left这种.语法时，Lean会自动尝试把Or当作一个带成员的类型构造器去解析，但普通函数根本没有所谓的"字段"或"内置成员"，所以就抛出了invalid field notation, type is not of the form (C ...) where C is a constant这个错误。

另外，我猜测你可能是自己定义了一个名为Or的函数（比如def Or (a b : Prop) := a ∨ b），覆盖了标准库中默认的Or归纳类型——标准库的Or是一个归纳类型构造器，本身自带inl/inr（对应你说的intro_left/intro_right）这类构造器成员，用.访问是完全合法的。

怎么解决这个问题？ #

根据你的需求，有三种可行的解决方案：

方案1：改用标准库的Or归纳类型

检查你的代码中是否存在自定义的Or函数定义，如果有的话直接删除它，Lean会自动使用标准库的Or归纳类型。此时你就可以正常使用Or.inl（对应你说的intro_left）来构造析取命题，比如：

#check Or.inl -- 正常通过，类型为：{a b : Prop} → a → Or a b

方案2：保留自定义Or，适配.语法使用

如果你确实需要保留自定义的Or函数，同时想使用.语法访问相关辅助函数，可以把Or包装成一个结构（structure），并在其命名空间下定义所需的构造函数，示例代码如下：

-- 把Or定义为结构，包装原有的析取逻辑
structure Or (a b : Prop) : Prop where
  inner : a ∨ b

-- 在Or命名空间下定义构造函数
namespace Or
def intro_left (h : a) : Or a b := ⟨Or.inl h⟩
def intro_right (h : b) : Or a b := ⟨Or.inr h⟩
end Or

-- 现在可以正常使用.语法访问了
#check Or.intro_left -- 不会再报错，类型为：{a b : Prop} → a → Or a b

方案3：避免.语法，直接使用命名空间引用

如果你不想修改Or的定义，也可以放弃.语法，直接通过命名空间引用辅助函数。比如先在独立的命名空间下定义构造函数：

def Or (a b : Prop) : Prop := a ∨ b

namespace OrHelper
def intro_left (a b : Prop) (h : a) : Or a b := h
def intro_right (a b : Prop) (h : b) : Or a b := h
end OrHelper

-- 直接用命名空间引用，不会触发字段符号错误
#check OrHelper.intro_left

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