LEAN中命名引发Prop与Type转换？定理调用异常困惑求解

我正试图理解Lean中类型匹配和定理参数传递的基础问题，以下是具体场景：

1. Commute_Or定理的应用矛盾 #

先看定义的析取交换律定理：

theorem Commute_Or {p q : Prop} (h : p ∨ q) : q ∨ p :=
  h.elim
    (λ hp:p => Or.inr hp)
    (λ hq:q => Or.inl hq)

直接调用时都会失败：

variable (j k : Prop)
#check Commute_Or j k         -- 失败
#check Commute_Or (j ∨ k)     -- 同样失败

针对Commute_Or (j ∨ k)的错误信息：

argument 'j ∨ k' has type 'Prop : Type' but is expected to have type '?m.178 ∨ ?m.179 : Prop'.

但给析取式命名后调用却正常：

variable (ex1 : j ∨ k)
#check Commute_Or ex1

这里的疑问是：(j ∨ k)和被定义为它的ex1到底有什么区别？

2. Equiv_Or定理的反向矛盾 #

基于Commute_Or证明的双向蕴含定理：

variable (y z : Prop)

theorem Equiv_Or : y ∨ z ↔ z ∨ y :=
  Iff.intro
    (λ h: (y ∨ z) => Commute_Or h)
    (λ j: (z ∨ y) => Commute_Or j)

以下调用均正常：

#check Equiv_Or y z           -- 正常运行
#check Equiv_Or (y ∨ z)       -- 同样正常

但传入命名后的析取式却失败：

variable (ex1 : j ∨ k)
#check Equiv_Or ex1           -- 失败

对应的错误信息：

argument ex1 has type 'j ∨ k : Prop' but is expected to have type 'Prop : Type'.

这和Commute_Or (j ∨ k)的错误恰好相反，实在搞不懂问题出在哪。

问题本质：命题与证明项的核心区别 #

对于Commute_Or #

先看它的类型签名：{p q : Prop} → p ∨ q → q ∨ p

• {p q : Prop}是隐式参数，Lean会自动推导这两个命题
• 第一个显式参数h : p ∨ q，要求的是命题p ∨ q的证明项（类型为p ∨ q），而非命题本身

你写Commute_Or (j ∨ k)时，传入的是命题j ∨ k（类型为Prop），但定理需要的是这个命题的证明项（类型为j ∨ k）。而ex1 : j ∨ k中，ex1正是类型为j ∨ k的证明项，所以匹配成功。

错误信息里的?m.178 ∨ ?m.179 : Prop，指的是Lean期望一个类型为“某个析取命题”的证明项，而你传的是命题本身，因此不匹配。

对于Equiv_Or #

它的类型签名是Prop → Prop → Prop：

• 前两个参数是命题本身（类型为Prop），而非证明项

所以：

• Equiv_Or y z：y和z都是Prop类型，符合要求
• Equiv_Or (y ∨ z)：Lean自动补全了第二个隐式参数（传入一个Prop后，定理会变成Prop → Prop的函数），因此正常
• Equiv_Or ex1：ex1的类型是j ∨ k（具体命题），而非Prop类型，不符合参数要求，因此报错

总结 #

核心混淆点是命题和命题的证明项的区别：

• 命题是Prop类型的对象，比如j ∨ k
• 证明项是类型为该命题的对象，比如ex1 : j ∨ k中的ex1

Commute_Or接收证明项，Equiv_Or接收命题本身，这就是两种场景报错相反的原因。

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