# Zulip Chat Archive

## Stream: new members

### Topic: Definite description operator

#### Patrick Johnson (Nov 16 2021 at 09:07):

Is there something like

```
def the {P : α → Prop} : (∃! (x : α), P x) → α := ...
```

to obtain the unique element for which a predicate is true? In Isabelle, there exists axiomatically defined function `THE`

which does exactly this. In Lean, destructuring an existential quantifier works only if the goal is a proposition.

#### Kevin Buzzard (Nov 16 2021 at 09:09):

There's docs#classical.some. Uniqueness isn't necessary (and doesn't help in Lean's type theory, you still need to apply a classical axiom).

#### Patrick Johnson (Nov 16 2021 at 09:35):

I'm trying to implement something like this:

```
universes u v
variable {α : Sort u}
variable {β : Sort v}
def func (P : α → Prop) (f : α → β) (z : β) : β :=
/-
If exists unique `(x : α)` such that `P x`
then return `f x`
else return `z`
-/
```

#### Ruben Van de Velde (Nov 16 2021 at 09:46):

Something like

```
def func (P : α → Prop) (f : α → β) (z : β) : β :=
if h : (∃! (x : α), P x) then classical.choice h else z
```

(untested since it wasn't a #mwe)

#### Scott Morrison (Nov 16 2021 at 09:47):

```
import tactic.basic
variables {α β : Type*}
open_locale classical
noncomputable def func (P : α → Prop) (f : α → β) (z : β) : β :=
if h : ∃ x, P x then f (classical.some h) else z
```

#### Sebastien Gouezel (Nov 16 2021 at 10:04):

Also called docs#classical.epsilon

#### Stuart Presnell (Nov 16 2021 at 11:13):

Do you know about Martin Escardo's work on "searchable sets"? https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-revised.pdf

By his definition, a set `X`

is searchable if it has a function `ε : (X → 2) → X`

such that for any `p : (X → 2)`

, iff `p`

has a root (i.e. a value `x ∈ X`

such that `p x = 0`

) then `ε p ∈ X`

is a root of `p`

.

He's formalised this in Agda (https://www.cs.bham.ac.uk/~mhe/agda/CantorSearch.html) and shown, for example, that the one-point compactification of `ℕ`

is searchable.

I don't know if any of this has been done in Lean yet. I made a bit of progress with it a couple of months ago.

#### Mario Carneiro (Nov 16 2021 at 11:24):

This notion kind of falls apart if the ambient logic is classical - every set is searchable

#### Eric Wieser (Nov 16 2021 at 11:34):

What is the type `2`

there? is it `fin 2`

or something isomorphic like `bool`

?

#### Stuart Presnell (Nov 16 2021 at 11:39):

It's defined here: https://www.cs.bham.ac.uk/~mhe/agda/Two.html

#### Mario Carneiro (Nov 16 2021 at 11:44):

it's `bool`

#### Stuart Presnell (Nov 16 2021 at 11:49):

Is it possible to work in a constructive setting in Lean and mathlib?

#### Mario Carneiro (Nov 16 2021 at 11:53):

it's possible, but I don't think these results hold. I am very suspicious of the claim that 2^N_infty has decidable equality by lean's interpretation

#### Eric Wieser (Nov 16 2021 at 12:04):

Stuart Presnell said:

Is it possible to work in a constructive setting in Lean and mathlib?

Yes, search for a post on Zulip that defines the `@[intuit]`

attribute that requires a theorem to be constructive

#### Reid Barton (Nov 16 2021 at 12:14):

Mario Carneiro said:

it's possible, but I don't think these results hold. I am very suspicious of the claim that 2^N_infty has decidable equality by lean's interpretation

I think this one is okay (only needs `funext`

), but the one about searching the Cantor set requires internalizing some Brouwerian uniform continuity hypothesis

#### Reid Barton (Nov 16 2021 at 12:15):

(I don't know if it's *required*, but that's what the Agda formalization does)

#### Mario Carneiro (Nov 16 2021 at 12:49):

I think you're right:

```
import data.bool data.nat.basic
def enat' := { x : ℕ → bool // ∀ i, x (i+1) → x i }
def inf : enat' := ⟨λ i, tt, λ _, id⟩
theorem enat'.ext (x : enat') (H : ∀ i, x.1 i) : x = inf :=
subtype.ext $ funext H
theorem enat'.mono (x : enat') (i j) (h : i ≤ j) : x.1 j → x.1 i :=
nat.le_induction id (λ n _ h h', h (x.2 _ h')) j h
instance : has_coe ℕ enat' :=
⟨λ n, ⟨λ i, i < n, λ i, by simp; exact lt_trans (lt_add_one i)⟩⟩
theorem enat'.eq_nat (x : enat') (n) (H : ¬ x.1 n) : ∃ i:ℕ, i ≤ n ∧ x = ↑i :=
begin
let m := nat.find ⟨n, H⟩,
refine ⟨m, nat.find_min' _ H, subtype.ext $ funext $ λ i, bool.coe_bool_iff.1 _⟩,
refine iff.trans _ (to_bool_iff _).symm,
by_cases h : i < m; simp [h],
{ exact decidable.not_not.1 ((@nat.find_min _ _ ⟨n, H⟩) _ h) },
{ simp at h,
rcases h with ⟨j, h₁, h₂⟩,
have := mt (enat'.mono x j i h₁),
simp at this,
exact this h₂ },
end
def selection (α : Type) :=
{ ε : (α → bool) → α // ∀ p : α → bool, p (ε p) → ∀ x, p x }
def eps (p : enat' → bool) : enat' :=
⟨λ n, to_bool $ ∀ k ≤ n, p k,
λ n, by simp; exact λ H k h, H _ (nat.le_succ_of_le h)⟩
def has_sel : selection enat' :=
⟨eps, λ p H n, begin
have : eps p = inf,
{ refine enat'.ext _ (λ n, _),
by_contra H',
rcases enat'.eq_nat _ _ H' with ⟨n, -, h⟩,
rw h at H,
have : ∀ i:ℕ, to_bool (∀ k ≤ i, p k) = to_bool (i < n) := λ i, congr_arg (λ x:enat', x.1 i) h,
have A := this n,
simp at A,
rcases A with ⟨i, h₁, h₂⟩,
rw ← eq_ff_eq_not_eq_tt at h₂,
rcases lt_or_eq_of_le h₁ with h₁ | rfl,
{ have B := this i,
simp [h₁] at B,
exact h₂ (B _ (le_refl _)) },
{ exact h₂ H } },
rw this at H,
by_contra h, apply h,
suffices : n = inf, { rwa this },
refine enat'.ext _ (λ i, _),
by_contra H',
rcases enat'.eq_nat _ _ H' with ⟨n, -, rfl⟩,
apply h,
have := congr_arg (λ x:enat', x.1 n) this,
simp [inf, eps] at this,
exact this _ (le_refl _)
end⟩
instance : decidable_eq (enat' → bool) :=
λ p q,
let x := eps (λ i, p i = q i) in
decidable_of_iff (p x = q x) ⟨λ H, begin
have : to_bool (p x = q x) → ∀ i, to_bool (p i = q i) := has_sel.2 (λ i, p i = q i),
simp at this,
exact funext (this H)
end, λ H, congr_fun H x⟩
```

Last updated: Dec 20 2023 at 11:08 UTC