为什么要在精益中进行这种类型检查？

Question

我运行了这个程序，并对它的类型进行了检查感到非常惊讶：

def A : Type := sorry
def B : Type := sorry

def f (a : A) : B := a

这似乎是错误的，为什么它有效？

Answer 1

之所以有效，是因为在这两种情况下，

sorry

都是

sorryAx Type false

的缩写，而且

sorryAx Type false

在定义上等于

sorryAx Type false

（它们是相同的）。您应该将

sorryAx

视为有点像选择公理的一个版本 - 它挑选出某种类型的未知术语，但它始终是相同的未知术语。

但是，在下一个精益版本中，由于 #5757，这种行为正在发生变化。示例：

def f (a : A) : B := a
/-                  ~~~
type mismatch
  a
has type
  A : Type
but is expected to have type
  B : Type
-/

区别在于

sorry

现在创建一个包含唯一标记的术语。默认情况下，它仍然可以漂亮地打印为

sorry

，但是通过更改漂亮的打印机选项，差异是显而易见的：

set_option pp.explicit true
#print A
/-
def A : Type :=
sorryAx (Name → Type) false `[email protected]._hyg.123
-/
#print B
/-
def B : Type :=
sorryAx (Name → Type) false `[email protected]._hyg.128
-/

技巧在于

sorry

由编码令牌的

Lean.Name

参数化。由于标记不同，这允许

sorryAx

从

Type

选择“不同”的术语。 （更准确地说，可能存在一个模型，其中

sorryAx

在两种情况下都选择相同的

Type

，但还有另一种模型，它选择不同的

Type

，所以不仅

A

和

B

不是 defeq，但

A

是否等于

B

是无论如何都无法证明。）

唯一令牌对唯一部分以及源位置信息进行编码。源位置可以让您找出

sorry

的来源，可以通过在信息视图中执行“转到定义”，也可以通过一些元编程来查找给定定理的所有未完成结果可能在哪里。

---

此功能的动机是，对于大型形式化项目来说，使用旧版本的

sorry

来删除定义是危险的。它可以让您轻松证明假定理，一旦将

sorry

替换为实际定义，这些定理就会变为假。有了新的

sorry

，你可以写

def g : Nat → Nat := sorry

并且放心，没有人会证明它与其他任何东西相同。

警告的话，你必须这样写而不是

def g (n : Nat) : Nat := sorry

因为这定义了一个常数函数。

example : ∀ (m n : Nat), g m = g n := by intros; rfl