Lean中Prop类型的内核特殊处理及相关特性问询

嗨！很高兴看到你刚从自然数游戏入坑Lean，还开始啃《Theorem Proving in Lean 4》啦～先结合你的问题和书中内容，给你逐一拆解：

你的原始提问背景与问题 #

It may be a bit early for me to ask this question, perhaps. I haven't used Lean beyond The Natural Numbers Game (Which was a lot of fun).

I'm reading Theorem Proving in Lean 4. It says stuff like:

Prop has some special features

and

if p : Prop is any proposition, Lean's kernel treats any two elements t1 t2 : p as being definitionally equal, [...]. This is known as proof irrelevance.

The Question:

Does Prop get any special treatment in core? If not, how is proof irrelevance created? Is it just "naturally" a property of the bottom of the hierarchy of universes?

The related thing I've stumbled across is Propositional extensionality which has the following axiom:

axiom propext {a b : Prop} : (a ↔ b) → a = b

Is this the axiom that sort of creates proof irrelevance? Could I create a proof irrelevant analog to Prop with all the same properties/behaviors and start proving the same theorems again? (Not that I'd want to! of'c)

问题解答 #

• Prop在Lean内核中确实有特殊待遇
  证明无关性（proof irrelevance）不是从公理推导出来的，而是Lean内核直接内置的规则。内核会主动把同一个命题p : Prop的任意两个证明t1 t2 : p判定为定义相等，这是内核层面的硬编码逻辑，和宇宙层级的“自然属性”无关——哪怕Prop是最小的宇宙，这个特性也是专门给它加的特殊处理。

• propext和证明无关性是完全独立的特性
  你看到的propext公理是命题外延性，它解决的是“两个逻辑等价的命题是否相等”的问题：如果a ↔ b，那么a = b。而证明无关性是关于“同一个命题的不同证明是否相等”，两者完全不是一回事。所以propext根本不是用来生成证明无关性的，它是另一个可选的公理（Lean默认不启用，需要你手动导入或声明），用来让等价命题可以在类型层面互相替换。

• 可以模拟类似Prop的证明无关类型，但没法完全复刻原生Prop的特性
  理论上你可以自定义一个类似的类型，比如MyProp，然后给它加一个公理来模拟证明无关性：

  axiom my_prop_proof_irrel {p : MyProp} (t1 t2 : p) : t1 = t2
  

  但这样的自定义类型没法享受到Lean内核给Prop的其他特殊处理：比如Prop的消除规则被限制为“不能从命题中提取非命题的计算信息”（确保命题只用来做证明，不参与计算），还有内核对Prop的各种优化。所以虽然能实现证明无关性，但没法做到和原生Prop完全一致的行为，实际用起来远不如原生Prop顺手——正如你说的，完全没必要这么做！

备注：内容来源于stack exchange，提问作者Mrk Sef