Definite description operator

Stream: new members

[Patrick Johnson]

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]

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]

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]

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]

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]

Also called docs#classical.epsilon

[Stuart Presnell]

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]

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

[Eric Wieser]

What is the type 2 there? is it fin 2 or something isomorphic like bool?

[Stuart Presnell]

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

[Mario Carneiro]

it's bool

[Stuart Presnell]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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⟩