## 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