get ∃ witness

Stream: new members

[Valéry Croizier]

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

[Alex J. Best]

You can do cases h with wit hw.

[Alex J. Best]

If h is the name of your hypothesis.

[Valéry Croizier]

Looks good, thanks!

[Jason Orendorff]

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

[Kevin Buzzard]

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]

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

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

[Johan Commelin]

yup, such let statements work

[Marcus Rossel]

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]

docs#classical.indefinite_description

[Marcus Rossel]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Marcus Rossel]

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]

This function is just classical.some.

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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