Skip to content

feat: remove Quot.sound axiom from em, provide em_eq without propext #13826

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
lyphyser wants to merge 2 commits into from
+12 −33
Closed

feat: remove Quot.sound axiom from em, provide em_eq without propext #13826

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
63c3b82
feat: remove Quot.sound axiom from em, shorten proof
lyphyser May 24, 2026
40d066a
feat: use em_eq in typeDecidableEq, removing Quot.sound and propext deps
lyphyser May 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 12 additions & 33 deletions src/Init/Classical.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,39 +32,16 @@ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :
theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property

/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality. -/
/-- **Diaconescu's theorem** for equalities: excluded middle from choice using proof irrelevance. -/
theorem em_eq {α : Sort u} (a b : α) : a = b ∨ a ≠ b :=
let E m := ∃ c, a = m ∧ c ∨ m = b ∧ ¬c
(.inl ·.1) |> (choose_spec (⟨True, .inl ⟨rfl, ⟨⟩⟩⟩ : E a)).elim fun h =>
(choose_spec (⟨False, .inr ⟨rfl, id⟩⟩ : E b)).imp (·.1) fun
| hn, rfl => hn.2 h.2

/-- **Diaconescu's theorem**: excluded middle from choice and propositional extensionality, using proof irrelevance. -/
theorem em (p : Prop) : p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := by simp [hvf, hut]
Or.inl hne
have p_implies_uv : p → u = v :=
fun hp =>
have hpred : U = V :=
funext fun x =>
have hl : (x = True ∨ p) → (x = False ∨ p) :=
fun _ => Or.inr hp
have hr : (x = False ∨ p) → (x = True ∨ p) :=
fun _ => Or.inr hp
show (x = True ∨ p) = (x = False ∨ p) from
propext (Iff.intro hl hr)
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
rw [hpred]; intros; rfl
show u = v from h₀ _ _
match not_uv_or_p with
| Or.inl hne => Or.inr (mt p_implies_uv hne)
| Or.inr h => Or.inl h
(em_eq p True).imp of_eq_true (mt eq_true)

theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
| ⟨x⟩ => ⟨x, trivial⟩
Expand All @@ -90,7 +67,9 @@ noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
instance (a : Prop) : Nonempty (Decidable a) := ⟨propDecidable a⟩

noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
fun _ _ => inferInstance
(choice <| match em_eq · · with
| .inl h => ⟨isTrue h⟩
| .inr h => ⟨isFalse h⟩)

noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
match (propDecidable (Nonempty α)) with
Expand Down
Loading