From c04e8a48fb698e50076c283eabc985c42f01604c Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 31 Aug 2021 09:04:36 +0000 Subject: [PATCH] feat(logic/basic): equivalence of by_contra and choice (#8912) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Based on an email suggestion from Freek Wiedijk: `classical.choice` is equivalent to the following Type-valued variation on `by_contradiction`: ```lean axiom classical.by_contradiction' {α : Sort*} : ¬ (α → false) → α ``` --- src/logic/basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/logic/basic.lean b/src/logic/basic.lean index aed809947fffa..82c587e53870e 100644 --- a/src/logic/basic.lean +++ b/src/logic/basic.lean @@ -1144,6 +1144,14 @@ hpq _ $ some_spec _ noncomputable def subtype_of_exists {α : Type*} {P : α → Prop} (h : ∃ x, P x) : {x // P x} := ⟨classical.some h, classical.some_spec h⟩ +/-- A version of `by_contradiction` that uses types instead of propositions. -/ +protected noncomputable def by_contradiction' {α : Sort*} (H : ¬ (α → false)) : α := +classical.choice $ peirce _ false $ λ h, (H $ λ a, h ⟨a⟩).elim + +/-- `classical.by_contradiction'` is equivalent to lean's axiom `classical.choice`. -/ +def choice_of_by_contradiction' {α : Sort*} (contra : ¬ (α → false) → α) : nonempty α → α := +λ H, contra H.elim + end classical /-- This function has the same type as `exists.rec_on`, and can be used to case on an equality,