From 6ae31ea2d6e9d6d30c0e2bedac166377a15d07ef Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 29 Jul 2025 05:51:34 +0200 Subject: [PATCH] chore: simplify docstring for propext (#9593) This PR simplifies the docstring for `propext` significantly. The old docstring explained general concepts of axioms that are now covered in the reference manual, and had a large example that was out of date and has been subsumed by reference manual content. --- src/Init/Core.lean | 37 ++++++------------------------------- 1 file changed, 6 insertions(+), 31 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 0e2c10efa4..52bf35192e 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1536,38 +1536,13 @@ end Setoid /-! # Propositional extensionality -/ /-- -The axiom of **propositional extensionality**. It asserts that if propositions -`a` and `b` are logically equivalent (i.e. we can prove `a` from `b` and vice versa), -then `a` and `b` are *equal*, meaning that we can replace `a` with `b` in all -contexts. +The [axiom](lean-manual://section/axioms) of **propositional extensionality**. It asserts that if +propositions `a` and `b` are logically equivalent (that is, if `a` can be proved from `b` and vice +versa), then `a` and `b` are *equal*, meaning `a` can be replaced with `b` in all contexts. -For simple expressions like `a ∧ c ∨ d → e` we can prove that because all the logical -connectives respect logical equivalence, we can replace `a` with `b` in this expression -without using `propext`. However, for higher order expressions like `P a` where -`P : Prop → Prop` is unknown, or indeed for `a = b` itself, we cannot replace `a` with `b` -without an axiom which says exactly this. - -This is a relatively uncontroversial axiom, which is intuitionistically valid. -It does however block computation when using `#reduce` to reduce proofs directly -(which is not recommended), meaning that canonicity, -the property that all closed terms of type `Nat` normalize to numerals, -fails to hold when this (or any) axiom is used: -``` -set_option pp.proofs true - -def foo : Nat := by - have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩ - have := propext this ▸ (2 : Nat) - exact this - -#reduce foo --- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2 - -#eval foo -- 2 -``` -`#eval` can evaluate it to a numeral because the compiler erases casts and -does not evaluate proofs, so `propext`, whose return type is a proposition, -can never block it. +The standard logical connectives provably respect propositional extensionality. However, an axiom is +needed for higher order expressions like `P a` where `P : Prop → Prop` is unknown, as well as for +equality. Propositional extensionality is intuitionistically valid. -/ axiom propext {a b : Prop} : (a ↔ b) → a = b