## Stream: new members

### Topic: get ∃ witness

#### Valéry Croizier (Jul 14 2020 at 16:24):

How to get a witness from a hypothesis that starts with "∃" ?

#### Alex J. Best (Jul 14 2020 at 16:27):

You can do cases h with wit hw.

#### Alex J. Best (Jul 14 2020 at 16:27):

If h is the name of your hypothesis.

#### Valéry Croizier (Jul 14 2020 at 16:28):

Looks good, thanks!

#### Jason Orendorff (Jul 14 2020 at 21:03):

Or equivalently, obtain ⟨v, hv⟩ := hexists, where the brackets are typed \< and \>.

#### Kevin Buzzard (Jul 14 2020 at 21:04):

You can even put obtain ⟨v, hv⟩ : ∃ v : V, f v = 0 := hexists -- the advantage of this is that it's very readable

#### Marcus Rossel (Dec 28 2020 at 10:20):

Is there a neat way of doing this, when not in a tactic-block?
Something like:

let ⟨v, hv⟩ := hexists in --?


#### Johan Commelin (Dec 28 2020 at 10:25):

yup, such let statements work

#### Marcus Rossel (Dec 28 2020 at 10:33):

Johan Commelin said:

yup, such let statements work

Doesn't work for me:

example (h : ∃ n : ℕ, n > 0) : ℕ :=
let ⟨n, _⟩ := h in n


Here I get:

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop


#### Eric Wieser (Dec 28 2020 at 10:36):

docs#classical.indefinite_description

#### Marcus Rossel (Dec 28 2020 at 10:38):

Eric Wieser said:

docs#classical.indefinite_description

Then the function would become noncomputable right? I thought in Lean it could somehow remain constructive. Or would I have to use something other than ∃ then?

#### Eric Wieser (Dec 28 2020 at 10:45):

Right, your function is impossible to make computable if it depends on extracting a witness

#### Eric Wieser (Dec 28 2020 at 10:47):

You could use {n : \N // n > 0}

#### Eric Wieser (Dec 28 2020 at 10:52):

Although maybe docs#nat.find will let you use exists anyway

#### Marcus Rossel (Dec 28 2020 at 10:55):

Eric Wieser said:

You could use {n : \N // n > 0}

Is this an approach used more generally in Lean? Returning a subtype instead of a ∃-proposition to stay in the constructive realm?

#### Kevin Buzzard (Dec 28 2020 at 10:55):

This function is just classical.some.

#### Mario Carneiro (Dec 28 2020 at 10:55):

Here's why such a function can't be defined:

constant magic (h : ∃ n : ℕ, n > 0) : ℕ
axiom magic_extract (n h) : magic ⟨n, h⟩ = n

example : false :=
have h1 : magic ⟨1, dec_trivial⟩ = 1, from magic_extract _ _,
have h2 : magic ⟨2, dec_trivial⟩ = 2, from magic_extract _ _,
have proof_irrel : magic ⟨1, dec_trivial⟩ = magic ⟨2, dec_trivial⟩, from rfl,
show false, from
absurd (h1.symm.trans \$ proof_irrel.trans h2) dec_trivial


#### Mario Carneiro (Dec 28 2020 at 10:56):

you can't extract a witness computably because all exists-witnesses are equal

#### Kevin Buzzard (Dec 28 2020 at 10:57):

Mathlib is not a constructive library (at least in most places).

#### Mario Carneiro (Dec 28 2020 at 10:57):

Actually I would say that most of the time we have computable witnesses when it can be done without too much effort

#### Mario Carneiro (Dec 28 2020 at 10:58):

However, instead of returning subtypes the preference is for a function and a theorem about that function

Last updated: May 14 2021 at 22:15 UTC