公理可能单独或与其他公理共同引入不一致。

假定一个假命题，就能证明任何命题：

axiom false_is_true : False theorem two_eq_five : 2 = 5 := false_is_true.elim

与 Lean 的其他性质不相容的公理也可能导致不一致。 例如，在支持参数化性的语言中，参数化性是一种强大的推理技术，但它与 Lean 的标准公理不相容。 如果参数化性成立，那么 Wadler 的论文 Theorems for Free（1989）引言中的“自由定理”就会成立；该论文介绍了利用参数化性推导多态函数相关定理的技术。 将这个自由定理写成公理如下：

axiom List.free_theorem {α β} (f : {α : _} → List α → List α) (g : α → β) : f ∘ (List.map g) = (List.map g) ∘ f

然而，排中律的一个推论是所有命题都可判定；这意味着函数可以检查命题是真还是假。 这个函数无法编译，但它仍然存在。 由此可以定义不具参数化性的多态函数：

open Classical in noncomputable def nonParametric {α : _} (xs : List α) : List α := if α = Nat then [] else xs

这个函数的存在与“自由定理”矛盾：

theorem unit_not_nat : Unit ≠ Nat := by⊢ Unit ≠ Nat intro eqeq:Unit = Nat⊢ False have ⟨allEq⟩ := eq ▸ (inferInstance : Subsingleton Unit)eq:Unit = NatallEq:∀ (a b : Nat), a = b⊢ False specialize allEq 0 1eq:Unit = NatallEq:0 = 1⊢ False contradictionAll goals completed! 🐙 example : False := by⊢ False have := List.free_theorem nonParametric (fun () => 42)this:(nonParametric ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ nonParametric⊢ False unfold nonParametric at thisthis:((fun xs => if Nat = Nat then [] else xs) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => if Unit = Nat then [] else xs⊢ False simp [unit_not_nat] at thisthis:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xs⊢ False have := congrFun this [()]this✝:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xsthis:((fun xs => []) ∘ List.map fun x => 42) [()] = ((List.map fun x => 42) ∘ fun xs => xs) [()]⊢ False contradictionAll goals completed! 🐙

用公理为 Nat 添加一个额外的 0，会使某些定义归约卡住。 在此例中，归约成功地将两个 Nat.succ 构造器移到项的外层，但 Nat.rec 遇到 Nat.otherZero 后就无法继续推进。

axiom Nat.otherZero : Nat ((Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) Nat.otherZero).1 4).succ.succ#reduce 4 + (Nat.otherZero + 2)

((Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) Nat.otherZero).1 4).succ.succ

用公理为 Nat 添加一个额外的 0，会使使用它的函数无法编译。 特别地，List.length' 将公理 Nat.otherZero 而不是 Nat.zero 作为空列表的长度返回。

axiom Nat.otherZero : Nat def `Nat.otherZero` not supported by code generator; consider marking definition as `noncomputable`List.length' : List α → Nat | [] => Nat.otherZero | _ :: _ => Unknown identifier `xs.length`xs.length

`Nat.otherZero` not supported by code generator; consider marking definition as `noncomputable`

在证明而非程序中使用的公理不会妨碍函数编译。 编译器不为证明生成代码，因此证明中的公理不会造成问题。 nextOdd 根据一个 Nat 计算下一个奇数；结果可能就是该数本身，也可能比它大一：

def nextOdd (k : Nat) : { n : Nat // n % 2 = 1 ∧ (n = k ∨ n = k + 1) } where val := if k % 2 = 1 then k else k + 1 property := byk:Nat⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1) by_cases k % 2 = 1posk:Nath✝:k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1)negk:Nath✝:¬k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1) <;>posk:Nath✝:k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1)negk:Nath✝:¬k % 2 = 1⊢ (if k % 2 = 1 then k else k + 1) % 2 = 1 ∧ ((if k % 2 = 1 then k else k + 1) = k ∨ (if k % 2 = 1 then k else k + 1) = k + 1) simp [*]negk:Nath✝:¬k % 2 = 1⊢ (k + 1) % 2 = 1 <;>negk:Nath✝:¬k % 2 = 1⊢ (k + 1) % 2 = 1 omegaAll goals completed! 🐙

该策略证明生成的项传递地依赖三个公理：

'nextOdd' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms nextOdd

'nextOdd' depends on axioms: [propext, Classical.choice, Quot.sound]

由于这些公理只出现在证明中，编译器可以顺利生成代码：

(5, 5)#eval (nextOdd 4, nextOdd 5)

(5, 5)

调用函数 Lean.reduceBool 和 Lean.reduceNat 可以让编译器执行计算；这能大幅提升反射式证明实现的性能。

set_option linter.deprecated false in def largeNumber : Nat := Lean.reduceNat (230_000 + 4_500 + 1_000_067)

所得项依赖公理 Lean.trustCompiler，以追踪该计算依赖编译器正确性这一事实。

'largeNumber' depends on axioms: [Lean.trustCompiler]#print axioms largeNumber

'largeNumber' depends on axioms: [Lean.trustCompiler]

native_decide 策略并不诉诸 Lean.trustCompiler，而是为每次调用创建一个专用公理。 这样就能针对每个公理所证明的确切命题进行审查。

set_option linter.defProp false in def bigSum : (List.range 1_001).sum = 500_500 := by⊢ (List.range 1001).sum = 500500 native_decideAll goals completed! 🐙 'bigSum' depends on axioms: [bigSum._native.native_decide.ax_1]#print axioms bigSum

'bigSum' depends on axioms: [bigSum._native.native_decide.ax_1]

可以直接检查该公理的类型：

bigSum._native.native_decide.ax_1 : decide ((List.range 1001).sum = 500500) = true#check bigSum._native.native_decide.ax_1

bigSum._native.native_decide.ax_1 : decide ((List.range 1001).sum = 500500) = true

考虑以下三个常量：

def addThree (n : Nat) : Nat := 1 + n + 2 theorem excluded_middle (P : Prop) : P ∨ ¬ P := Classical.em P theorem simple_equality (P : Prop) : (P ∨ False) = P := or_false P

像 addThree 这样可能确实需要求值的普通函数通常不依赖任何公理：

'addThree' does not depend on any axioms#print axioms addThree

'addThree' does not depend on any axioms

排中律定理只有使用经典推理时才成立，因此经典推理的基础会与其他公理一同出现：

'excluded_middle' depends on axioms: [propext, Classical.choice, Quot.sound]#print axioms excluded_middle

'excluded_middle' depends on axioms: [propext, Classical.choice, Quot.sound]

最后，等价命题相等这一观念直接依赖命题外延性。

'simple_equality' depends on axioms: [propext]#print axioms simple_equality

'simple_equality' depends on axioms: [propext]

可以将 Lean.Parser.Command.printAxioms : command显示一个声明直接或间接使用的公理。请参阅[参考手册](https://lean-lang.org/doc/reference/4.34.0-rc1/find/?domain=Verso.Genre.Manual.section&name=validating-proofs)，了解如何解释输出。#print axioms 与 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档 注释的内容匹配。 基本示例： ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` 这会检查确有此错误，然后消费该消息。 默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告： ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` 或只选择错误： ```lean #guard_msgs(error) in example : α := sorry ``` 在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告： ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` 一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句： ``` #guard_msgs (configElt,*) in cmd ``` 默认配置列表为 `(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。 消息过滤器按严重程度选择消息： - `info`、`warning`、`error`：具有相应严重程度的非跟踪消息； - `trace`：跟踪消息； - `all`：所有消息。 过滤器可带有指定操作的前缀： - `check`（默认）：捕获并检查消息； - `drop`：丢弃消息； - `pass`：让消息继续传递。 若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式 添加 `pass all`。 空白处理（先去除开头和末尾的空白）： - `whitespace := exact` 要求空白完全匹配； - `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行； - `whitespace := lax` 在匹配前把连续空白压缩为一个空格。 消息排序： - `ordering := exact` 使用消息的原始顺序（默认）； - `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。 位置信息： - `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围； - `positions := false` 不报告位置信息。 子串匹配： - `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心 消息一部分的情况； - `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。 稳定输出： 消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。 使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留 `?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为 `?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的 松散自由变量名替换为 `_fvar._`。 例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。 命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码 检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令 运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。 因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 配合使用，以确保 其他项目的库更新不会悄然 引入不需要的公理依赖。

例如，如果下面 double_neg_elim 的证明发生变化，使用了比所列公理更多的公理， 那么 Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` 捕获命令 `cmd` 生成的消息，并检查它们是否与文档 注释的内容匹配。 基本示例： ```lean /-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x ``` 这会检查确有此错误，然后消费该消息。 默认情况下，该命令捕获所有消息，但可调整过滤条件。例如，只选择警告： ```lean /-- warning: declaration uses 'sorry' -/ #guard_msgs(warning) in example : α := sorry ``` 或只选择错误： ```lean #guard_msgs(error) in example : α := sorry ``` 在上一个示例中，因为警告未被捕获，`sorry` 上仍会产生警告。可用下述写法彻底丢弃警告： ```lean #guard_msgs(error, drop warning) in example : α := sorry ``` 一般而言，`#guard_msgs` 接受一组置于圆括号内、以逗号分隔的配置子句： ``` #guard_msgs (configElt,*) in cmd ``` 默认配置列表为 `(check all, whitespace := normalized, ordering := exact, positions := false, substring := false)`。 消息过滤器按严重程度选择消息： - `info`、`warning`、`error`：具有相应严重程度的非跟踪消息； - `trace`：跟踪消息； - `all`：所有消息。 过滤器可带有指定操作的前缀： - `check`（默认）：捕获并检查消息； - `drop`：丢弃消息； - `pass`：让消息继续传递。 若未指定过滤器，则假定为 `check all`。否则从左至右处理这些过滤器，并在末尾隐式 添加 `pass all`。 空白处理（先去除开头和末尾的空白）： - `whitespace := exact` 要求空白完全匹配； - `whitespace := normalized` 在匹配前把所有换行符转换为空格（默认），从而允许拆分长行； - `whitespace := lax` 在匹配前把连续空白压缩为一个空格。 消息排序： - `ordering := exact` 使用消息的原始顺序（默认）； - `ordering := sorted` 按字典序排列消息，便于测试消息顺序不确定的命令。 位置信息： - `positions := true` 报告所有消息相对于 `#guard_msgs` 所在行的范围； - `positions := false` 不报告位置信息。 子串匹配： - `substring := true` 检查文档注释是否为输出的子串（在空白归一化之后），适用于只关心 消息一部分的情况； - `substring := false`（默认）要求精确匹配（允许空白归一化造成的差异）。 稳定输出： 消息含有自动生成的名称（例如元变量 `?m.47`）时，输出可能随运行或 Lean 版本而变化。 使用 `set_option pp.mvars.anonymous false` 可把匿名元变量替换为 `?_`，同时保留 `?a` 等用户命名的元变量。也可使用 `set_option pp.mvars false` 把所有元变量替换为 `?_`。类似地，`set_option pp.fvars.anonymous false` 会把 `_fvar.22` 之类的 松散自由变量名替换为 `_fvar._`。 例如，`#guard_msgs (error, drop all) in cmd` 表示检查错误并丢弃其他一切消息。 命令精译器对 `#guard_msgs` 的代码检查有特殊支持。`#guard_msgs` 本身希望捕获代码 检查器的警告，因此会把所附命令当作顶层命令精译。然而，命令精译器会对所有顶层命令 运行代码检查器，其中也包括 `#guard_msgs` 自身，这会导致重复警告或警告未被捕获。 因此，仅当顶层命令中不存在 `#guard_msgs` 时，顶层命令精译器才运行代码检查器。#guard_msgs 命令就会报告错误。

theorem double_neg_elim (P : Prop) : (¬ ¬ P) = P := propext Classical.not_not /-- info: 'double_neg_elim' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms double_neg_elim