feat: examples of printing axioms (#601)

This PR rearranges the discussion of axioms, primarily in order to add
several more examples of the use of `#print axioms <ident>`. Also links
the #print axioms spec back to the docs on axioms.

Follow-up from discussion with @jcreedcmu.

Author: robsimmons

Manual/Axioms.lean

@@ -176,41 +176,33 @@ Because they occur only in a proof, the compiler has no problem generating code:
 ```
 :::
 
-# Displaying Axiom Dependencies
-%%%
-tag := "print-axioms"
-%%%
-
-The command {keywordOf Lean.Parser.Command.printAxioms}`#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 {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` for both.
-This can be used to audit the assumptions made by a proof.
-Together with {keywordOf Lean.guardMsgsCmd}`#guard_msgs`, it can also ensure that updates to libraries from other projects don't silently introduce unwanted dependencies on axioms.
-
 # Standard Axioms
 %%%
 tag := "standard-axioms"
 %%%
 
-Lean includes the following mathematical axioms:
+There are seven standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean:
  * ```signature
-   propext {a b : Prop} : (a ↔ b) → a = b
+   Classical.choice.{u} {α : Sort u} : Nonempty α → α
    ```
  * ```signature
-   Classical.choice.{u} {α : Sort u} : Nonempty α → α
+   propext {a b : Prop} : (a ↔ b) → a = b
    ```
  * ```signature
    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 {tactic}`native_decide` tactic.
-Both {name}`Lean.reduceBool` and {name}`Lean.reduceNat` contain references to {name}`Lean.trustCompiler`, which ensures that the fact that a proof trusts the correctness of the compiler is tracked.
+All three of these axioms are discussed in the book [Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean4/find/?domain=Verso.Genre.Manual.section&name=axioms-and-computation).
+
+The axiom {name}`sorryAx` is used as part of the implementation of the {tactic}`sorry` tactic and {lean}`sorry` term.
+Uses of this axiom are not intended to occur in finished proofs, as it can be used to prove anything:
+ * ```signature
+   sorryAx {α : Sort u} (synthetic := true) : α
+   ```
 
-These axioms do not truly exist for their _mathematical_ content; after all, {name}`Lean.reduceBool` and {name}`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 {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` to be used to audit theorems.
+Three final axioms do not truly exist for their _mathematical_ content; from a mathematical perspective they prove trivial statements:
 
  * ```signature
     Lean.trustCompiler : True
@@ -223,10 +215,110 @@ However, they allow the use of compiled code in proofs to be carefully controlle
     Lean.ofReduceNat (a b : Nat) : Lean.reduceNat a = b → a = b
    ```
 
-:::keepEnv
-```lean -show
-axiom Anything : Type
+These axioms instead track proofs that depend on the correctness of the entire compiler, and not just on the much smaller {tech}`kernel`.
+
+:::example "Creating and Tracking Proofs That Trust the Compiler"
+The functions {name}`Lean.reduceBool` and {name}`Lean.reduceNat` can be invoked to have the compiler perform a calculation; this can greatly improve performance of implementations of proof by reflection.
+
+```lean
+def largeNumber : Nat := Lean.reduceNat (230_000 + 4_500 + 1_000_067)
+```
+
+The resulting term depends on the axiom {name}`Lean.trustCompiler` in order to track the fact that this calculation depends on the correctness of the compiler.
+
+```lean (name := printAxExC1)
+#print axioms largeNumber
+```
+```leanOutput printAxExC1
+'largeNumber' depends on axioms: [Lean.trustCompiler]
+```
+
+The most common way that proofs end up trusting the compiler is through the {tactic}`native_decide` tactic:
+
+```lean (name := printAxExC2)
+def bigSum : (List.range 1_001).sum = 500_500 := by native_decide
+#print axioms bigSum
+```
+```leanOutput printAxExC2
+'bigSum' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler]
+```
+:::
+
+# Displaying Axiom Dependencies
+%%%
+tag := "print-axioms"
+%%%
+
+The command {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`, followed by a defined identifier, displays all the axioms that a definition transitively relies on.
+In other words, if a proof uses another proof, which itself uses an axiom, then the axiom is reported by {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` for both.
+
+::::keepEnv
+
+This can be used to audit the assumptions made by a proof, for instance detecting that a proof transitively depends on the {tactic}`sorry` tactic.
+
+```lean
+def lazy : 4 == 2 + 1 + 1 := by sorry
+```
+```lean (name := printAxEx4)
+#print axioms lazy
+```
+```leanOutput printAxEx4
+'lazy' depends on axioms: [sorryAx]
+```
+
+:::example "Printing Axioms of Simple Definitions" (keep := true)
+
+Consider the following three constants:
+
+```lean
+def addThree (n : Nat) : Nat := 1 + n + 2
+theorem excludedMiddle (P : Prop) : P ∨ ¬ P := Classical.em P
+theorem simpleEquality (P : Prop) : (P ∨ False) = P := or_false P
+```
+
+Regular functions like {lean}`addThree` that we might want to actually evaluation typically do not depend on any axioms:
+
+```lean (name := printAxEx2)
+#print axioms addThree
+```
+```leanOutput printAxEx2
+'addThree' does not depend on any axioms
+```
+
+The excluded middle theorem is only true if we use classical reasoning, so the foundation for classical reasoning shows up alongside other axioms:
+
+```lean (name := printAxEx1)
+#print axioms excludedMiddle
+```
+```leanOutput printAxEx1
+'excludedMiddle' depends on axioms: [propext, Classical.choice, Quot.sound]
+```
+
+Finally, the idea that two equivalent propositions are equal directly relies on {tech}[propositional extensionality].
+
+```lean (name := printAxEx3)
+#print axioms simpleEquality
+```
+```leanOutput printAxEx3
+'simpleEquality' depends on axioms: [propext]
 ```
-Finally, the axiom {name}`sorryAx` is used as part of the implementation of the {tactic}`sorry` tactic and {lean  (type := "Anything")}`sorry` term.
-Uses of this axiom are not intended to occur in finished proofs, and this can be confirmed using {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
 :::
+
+:::example "Using {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` with {keywordOf Lean.guardMsgsCmd}`#guard_msgs`"
+
+You can use {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` together with {keywordOf Lean.guardMsgsCmd}`#guard_msgs` to ensure that updates to libraries from other projects cannot silently introduce unwanted dependencies on axioms.
+
+Perhaps you are worried that some future update to {lean}`or_false` in the previous example's {lean}`simpleEquality` proof might quietly introduce a new axiom dependency.
+You can guard against this by writing a command that will fail if {lean}`simpleEquality` uses any axioms besides {lean}`propext`:
+
+```lean
+/--
+info: 'simpleEquality' depends on axioms: [propext]
+-/
+#guard_msgs in
+#print axioms simpleEquality
+```
+:::
+
+
+::::

Manual/Interaction.lean

@@ -307,7 +307,7 @@ Adds the string literal to Lean's {tech}[message log].
 #print axioms $t
 ```
 
-Lists all axioms that the constant transitively relies on.
+Lists all axioms that the constant transitively relies on. See {ref "print-axioms"}[the documentation for axioms] for more information.
 :::
 
 :::example "Printing Axioms"