axiom ::= ... | axiomdeclId`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe namesdeclSig`declSig` matches the signature of a declaration with required type: a list of binders and then `: type`
8. Axioms
Axioms are postulated constants.
While the axiom's type must itself be a type (that is, it must have type Sort u), there are no further requirements.
Axioms do not reduce to other terms.
Axioms can be used to experiment with the consequences of an idea before investing the time required to construct a model or prove a theorem. They can also be used to adopt reasoning principles that can't otherwise be accessed in Lean's type theory; Lean itself provides three such axioms that are known to be consistent. However, axioms should be used with caution: axioms that are inconsistent with one another, or just false, undermine the very foundations of proofs. Lean automatically tracks the axioms that each proof depends on so that they can be audited.
8.1. Axiom Declarations
Axioms declarations include a name and a type:
syntaxAxiom Declarations
Axioms declarations may be modified with all possible declaration modifiers.
Documentation comments, attributes, private, and protected have the same meaning as for other declarations.
The modifiers partial, nonrec, noncomputable and unsafe have no effect.
8.2. Consistency
Using axioms is risky. Because they introduce a new constant of any type, and an inhabitant of a type that is a proposition counts as a proof of the proposition, axioms can be used to prove even false propositions. Any proof that relies on an axiom can be trusted only to the extent that the axiom is both true and consistent with the other axioms used. By their very nature, Lean cannot check whether new axioms are consistent; please exercise care when adding axioms.
Inconsistencies From Axioms
Axioms may introduce inconsistency, either alone or in combination with other axioms.
Assuming a false statement allows any statement at all to be proved:
axiom false_is_true : False
theorem two_eq_five : 2 = 5 := false_is_true.elim
Inconsistency may also arise from axioms that are incompatible with other properties of Lean. For example, parametricity is a powerful reasoning technique when used in languages that support it, but it is not compatible with Lean's standard axioms. If parametricity held, then the “free theorem” from the introduction to Wadler's Theorems for Free (1989), which describes a technique for using parametricity to derive theorems about polymorphic functions, would be true. As an axiom, it reads:
axiom List.free_theorem {α β}
(f : {α : _} → List α → List α) (g : α → β) :
f ∘ (List.map g) = (List.map g) ∘ f
However, a consequence of excluded middle is that all propositions are decidable; this means that a function can check whether they are true or false. This function can't be compiled, but it still exists. This can be used to define polymorphic functions that are not parametric:
open Classical in
noncomputable def nonParametric
{α : _} (xs : List α) :
List α :=
if α = Nat then [] else xs
The existence of this function contradicts the “free theorem”:
theorem unit_not_nat : Unit ≠ Nat := ⊢ Unit ≠ Nat
eq:Unit = Nat⊢ False
eq:Unit = NatallEq:∀ (a b : Nat), a = b⊢ False
eq:Unit = NatallEq:0 = 1⊢ False
All goals completed! 🐙
example : False := ⊢ False
this:(nonParametric ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ nonParametric⊢ False
this:((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
this:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xs⊢ False
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
All goals completed! 🐙
8.3. Reduction
Even consistent axioms can cause difficulties. Definitional equality identifies terms modulo reduction rules. The ι-reduction rule specifies the interaction of recursors and constructors; because axioms are not constructors, it does not apply to them. Ordinarily, terms without free variables reduce to applications of constructors, but axioms can cause them to get “stuck,” resulting in large terms.
Axioms and Stuck Reduction
Adding an addtional 0 to Nat with an axiom results in some definitional reductions getting stuck.
In this example, two Nat.succ constructors are successfully moved to the outside of the term by reduction, but Nat.rec is unable to make further progress after encountering Nat.otherZero.
axiom Nat.otherZero : Nat
#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
Furthermore, the Lean compiler is not able to generate code for axioms.
At runtime, Lean values must be represented by concrete data in memory, but axioms do not have a concrete representation.
Definitions that contain non-proof code that relies on axioms must be marked noncomputable and can't be compiled.
Axioms and Compilation
Adding an addtional 0 to Nat with an axiom makes it so functions that use it can't be compiled.
In particular, List.length' returns the axiom Nat.otherZero instead of Nat.zero.
The function is marked partial to avoid further error messages from termination checking.
axiom Nat.otherZero : Nat
partial def List.length' : List α → Nat
| [] => Nat.otherZero
| _ :: xs => xs.length' + 1
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Nat.otherZero', and it does not have executable code
Axioms used in proofs rather than programs do not prevent a function from being compiled.
The compiler does not generate code for proofs, so axioms in proofs are no problem.
nextOdd computes the next odd number from a Nat, which may be the number itself or one greater:
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 := k: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)
k: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)k: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) k: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)k: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)
k:Nath✝:¬k % 2 = 1⊢ (k + 1) % 2 = 1 k:Nath✝:¬k % 2 = 1⊢ (k + 1) % 2 = 1 All goals completed! 🐙
The by_cases tactic uses the Law of the Excluded Middle, which is proved in the standard library using the Axiom of Choice.
Indeed, this definition uses three axioms:
#print axioms nextOdd
'nextOdd' depends on axioms: [propext, Classical.choice, Quot.sound]
Because they occur only in a proof, the compiler has no problem generating code:
#eval (nextOdd 4, nextOdd 5)
(5, 5)
8.4. Displaying Axiom Dependencies
The command Lean.Parser.Command.printAxioms : command#print axioms displays all the axioms that a declaration transitively relies on.
In other words, if a proof uses another proof, which itself uses an axiom, then the axiom is reported by Lean.Parser.Command.printAxioms : command#print axioms for both.
This can be used to audit the assumptions made by a proof.
Together with Lean.guardMsgsCmd : command`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.
Basic example:
```lean
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
```
This checks that there is such an error and then consumes the message.
By default, the command captures all messages, but the filter condition can be adjusted.
For example, we can select only warnings:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#guard_msgs(error) in
example : α := sorry
```
In the previous example, since warnings are not captured there is a warning on `sorry`.
We can drop the warning completely with
```lean
#guard_msgs(error, drop warning) in
example : α := sorry
```
In general, `#guard_msgs` accepts a comma-separated list of configuration clauses in parentheses:
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is `(all, whitespace := normalized, ordering := exact)`.
Message filters (processed in left-to-right order):
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.
Whitespace handling (after trimming leading and trailing whitespace):
- `whitespace := exact` requires an exact whitespace match.
- `whitespace := normalized` converts all newline characters to a space before matching
(the default). This allows breaking long lines.
- `whitespace := lax` collapses whitespace to a single space before matching.
Message ordering:
- `ordering := exact` uses the exact ordering of the messages (the default).
- `ordering := sorted` sorts the messages in lexicographic order.
This helps with testing commands that are non-deterministic in their ordering.
For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and drop
everything else.
The command elaborator has special support for `#guard_msgs` for linting.
The `#guard_msgs` itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for *all* top-level commands,
which would include `#guard_msgs` itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
#guard_msgs, it can also ensure that updates to libraries from other projects don't silently introduce unwanted dependencies on axioms.
8.5. Standard Axioms
Lean includes the following mathematical axioms:
-
propext {a b : Prop} : (a ↔ b) → a = b -
Classical.choice.{u} {α : Sort u} : Nonempty α → α -
Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} : r a b → Quot.mk r a = Quot.mk r b
Three additional axioms allow the Lean kernel to invoke code generated by the compiler, rather than using its internal reduction engine.
This can greatly improve performance of implementations of proof by reflection.
Rather than using these axioms directly, they are usually invoked via the native_decide tactic.
Both Lean.reduceBool and Lean.reduceNat contain references to Lean.trustCompiler, which ensures that the fact that a proof trusts the correctness of the compiler is tracked.
These axioms do not truly exist for their mathematical content; after all, Lean.reduceBool and Lean.reduceNat are essentially the identity function.
However, they allow the use of compiled code in proofs to be carefully controlled, and tracking them as axioms allows Lean.Parser.Command.printAxioms : command#print axioms to be used to audit theorems.
-
Lean.trustCompiler : True -
Lean.ofReduceBool (a b : Bool) : Lean.reduceBool a = b → a = b -
Lean.ofReduceNat (a b : Nat) : Lean.reduceNat a = b → a = b
Finally, the axiom sorryAx is used as part of the implementation of the sorry tactic and sorry term.
Uses of this axiom are not intended to occur in finished proofs, and this can be confirmed using Lean.Parser.Command.printAxioms : command#print axioms.