From b9cceacaa737c3273e2a6434da16c1e51d717f88 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 10 Apr 2024 14:48:49 +0200 Subject: [PATCH 1/3] doc: Classical.choice --- src/Init/Classical.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 0d52a62e2ebe..e5c59b30a6ce 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -15,9 +15,17 @@ namespace Classical noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} := choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩ +/-- +Given that there exists an element satisfying `p`, returns one such element. + +This is a straightforward consequence of, and equivalent to, `Classical.choice`. +-/ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α := (indefiniteDescription p h).val +#check Classical.choice +#check Classical.choose + theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) := (indefiniteDescription p h).property From bb80917bb7d058dd9c709b07d5d7d628d57d484a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 10 Apr 2024 14:56:11 +0200 Subject: [PATCH 2/3] oops --- src/Init/Classical.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index e5c59b30a6ce..fda5b0cd407f 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -23,9 +23,6 @@ This is a straightforward consequence of, and equivalent to, `Classical.choice`. noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α := (indefiniteDescription p h).val -#check Classical.choice -#check Classical.choose - theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) := (indefiniteDescription p h).property From 9126b3a654d5acf5ad4d7142ad00d302521f0610 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 17 Apr 2024 13:26:04 +0200 Subject: [PATCH 3/3] Update src/Init/Classical.lean Co-authored-by: Mario Carneiro --- src/Init/Classical.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index fda5b0cd407f..1c6edb7978a3 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -19,6 +19,8 @@ noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ Given that there exists an element satisfying `p`, returns one such element. This is a straightforward consequence of, and equivalent to, `Classical.choice`. + +See also `choose_spec`, which asserts that the returned value has property `p`. -/ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α := (indefiniteDescription p h).val