Zulip Chat Archive

Stream: new members

Topic: get ∃ witness


view this post on Zulip Valéry Croizier (Jul 14 2020 at 16:24):

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

view this post on Zulip Alex J. Best (Jul 14 2020 at 16:27):

You can do cases h with wit hw.

view this post on Zulip Alex J. Best (Jul 14 2020 at 16:27):

If h is the name of your hypothesis.

view this post on Zulip Valéry Croizier (Jul 14 2020 at 16:28):

Looks good, thanks!

view this post on Zulip Jason Orendorff (Jul 14 2020 at 21:03):

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

view this post on Zulip 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

view this post on Zulip 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 --?

view this post on Zulip Johan Commelin (Dec 28 2020 at 10:25):

yup, such let statements work

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 28 2020 at 10:36):

docs#classical.indefinite_description

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Dec 28 2020 at 10:45):

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

view this post on Zulip Eric Wieser (Dec 28 2020 at 10:47):

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

view this post on Zulip Eric Wieser (Dec 28 2020 at 10:52):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 10:55):

This function is just classical.some.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 28 2020 at 10:56):

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

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 10:57):

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

view this post on Zulip 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

view this post on Zulip 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