19.1. 真与假🔗

从根本上说，Lean 中只有两个命题：True 和 False。命题外延公理（propext）允许将逻辑等价的命题视为相等；每个真命题都与 True 逻辑等价。同样，每个假命题都与 False 逻辑等价。

True 是一个归纳定义的命题，只有一个不接受参数的构造器。证明 True 总是可能的。另一方面，False 是一个没有构造器的归纳定义命题。证明它需要在当前上下文中找到矛盾。

True 和 False 都是至多单元素类型；这意味着它们可用于计算非命题类型的元素。对于 True，这相当于忽略证明，因为证明并不携带信息。对于 False，这表示当前代码不可达，因此无需完成。

归纳命题

True : Prop
True : Prop

True 是一个命题，只有一条引入规则 True.intro : True。换言之，True 就是真的，并具有规范证明 True.intro。更多信息：命题逻辑

构造子

True.intro : True

True 为真，True.intro（更常用的是 trivial）就是其证明。

归纳命题

False : Prop
False : Prop

False 是空命题，因此没有引入规则。它表示矛盾。False 的消去规则 False.rec 表达了从矛盾可推出任何命题这一事实。该规则有时称为 ex falso（ex falso sequitur quodlibet 的简称），或爆炸原理。更多信息：命题逻辑

构造子

定义

False.elim.{u} {C : Sort u} (h : False) : C
False.elim.{u} {C : Sort u} (h : False) :
  C

False.elim : False → C 表示由 False 可推出任意所需命题 C。它也称为 ex falso quodlibet（EFQ）或爆炸原理。

目标类型实际上是 C : Sort u，因此它对命题和类型都适用。执行时，它类似于“不可达”指令：运行它属于未定义行为，但很可能打印“unreachable code”。（无论如何，必须先构造假命题的证明才能运行它，而这只能借助 sorry 或不可靠的公理做到。）

死代码与至多单元素消去

f 的定义中的第四个分支不可达，因此无需提供具体的 String 值：

def f (n : Nat) : String :=
  if h1 : n < 11 then
    "Small"
  else if h2 : n > 13 then
    "Large"
  else if h3 : n % 2 = 1 then
    "Odd"
  else if h4 : n ≠ 12 then
    False.elim (byn:Nath1:¬n < 11h2:¬n > 13h3:¬n % 2 = 1h4:n ≠ 12⊢ False omegaAll goals completed! 🐙)
  else "Twelve"

在此例中，False.elim 向 Lean 表明当前局部上下文不一致：证明 False 就足以放弃该分支。

类似地，g 的定义看起来可能不会终止。然而，递归调用位于程序的一条不可达路径上。用于生成终止性证明的自动化能够检测出局部假设之间的矛盾。

def g (n : Nat) : String :=
  if n < 11 then
    "Small"
  else if n > 13 then
    "Large"
  else if n % 2 = 1 then
    "Odd"
  else if n ≠ 12 then
    g (n + 1)
  else "Twelve"
termination_by n

在线查看 ↪