Exists.choose and equality

Stream: new members

[Martin Dvořák]

My brain isn't braining today...

import Mathlib

open Classical in
noncomputable def represent (R : Char → Prop) : Option Char :=
  if hc : (∃ c : Char, R c) then
    some hc.choose
  else
    none

def singleton_A (c : Char) : Prop := (c = 'A')

example : represent singleton_A = 'A' := by
  sorry

Is it provable?

[Markus Himmel]

Sure:

example : represent singleton_A = 'A' := by
  rw [represent]
  have : ∃ c, singleton_A c := ⟨_, rfl⟩
  simpa [this, singleton_A] using this.choose_spec

[Martin Dvořák]

Oh, so we can have something like:

import Init.Classical

open Classical in
noncomputable def represent (R : Char → Prop) : Option Char :=
  if hc : (∃ c : Char, R c) then
    some hc.choose
  else
    none

theorem represent_unique {R : Char → Prop} {x y : Char}
    (hRx : represent R = some x) (hRy : represent R = some y) :
    x = y := by
  simp_all

def doubleton_AB (c : Char) : Prop := (c = 'A') ∨ (c = 'B')

example : represent doubleton_AB = 'A' ∨ represent doubleton_AB = 'B' := by
  have existence : ∃ c, doubleton_AB c := ⟨'A', by simp [doubleton_AB]⟩
  cases existence.choose_spec with
  | inl hA => left; simpa [represent, hA]
  | inr hB => right; simpa [represent, hB]

We don't know whether represent doubleton_AB chooses A or B as the result, but we still know that the result will be the same every time we refer to it? Did I get it right?