Lean 4‘未知标识符证明’

Question

我在使用Lean4时遇到了一个问题。

我在浏览文档的命题与证明部分时遇到了它。在作为类型的命题下，文档引入了Proof类型：

然后我们可以为每个元素p : Prop引入另一种类型的Proof p，用于p的证明类型。

下面，它显示了对Proof类型的代码片段检查，它返回Proof : Prop → Type

#check Proof   -- Proof : Prop → Type

当我尝试运行这个片段时，我会得到以下错误：

example.lean:3:7: error: unknown identifier 'Proof'

这意味着Lean找不到Proof类型。这是我的问题，我如何让Lean4识别到Proof？

谢谢!

Answer 1

“Lean4中的定理证明”仍在进行中(实际上，Lean4本身仍在迅速变化)，因此您可能会在其中发现许多问题。然而，在这种情况下，我相信问题是，它是在假设一种方式，可以建立的东西，实际上并不是Lean中完成的方式。

下面是使这些代码块实际编译的一种方法：

namespace TPIL

axiom Prop' : Type
axiom And : Prop' → Prop' → Prop'
axiom Or : Prop' → Prop' → Prop'
axiom Not : Prop' → Prop'
axiom Implies : Prop' → Prop' → Prop'
axiom Proof : Prop' → Type

variable (p q r : Prop')
#check And p q                      -- Prop'
#check Or (And p q) r               -- Prop'
#check Implies (And p q) (And q p)  -- Prop'

#check Proof   -- Proof : Prop' → Type

axiom and_comm (p q : Prop') : Proof (Implies (And p q) (And q p))

variable (p q : Prop')
#check and_comm p q     -- Proof (Implies (And p q) (And q p))

axiom modus_ponens : (p q : Prop') → Proof (Implies p q) →  Proof p → Proof q

axiom implies_intro : (p q : Prop') → (Proof p → Proof q) → Proof (Implies p q)

但是，您必须使用Prop'或«Prop»，因为Prop是关键字。

Answer 2

没有这样的类型称为Proof。文档提到它是如何实现Lean的一个例子，但是继续解释为什么它不是那样实现的。