Zulip Chat Archive

Stream: maths

Topic: Eliminating into Prop woes


view this post on Zulip Koundinya Vajjha (Apr 09 2019 at 16:35):

I have defined the following

import algebra.archimedean

def pow_two_near (n : ) : (n > 1)   k : , (2 ^ k  n  n < 2^(k+1)) :=
by intro h ; exact (exists_nat_pow_near h one_lt_two)

Is there any way to get ahold of the k without doing this?

noncomputable def index_pow_two_near (n : ) (h : n > 1) :  := classical.some $ pow_two_near n h

If I try to destruct the exists I get an error:

def index_pow_two_near' (n : ) (h : n > 1) :  :=
begin
have h := pow_two_near n h,
cases h, --induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
end

view this post on Zulip Johan Commelin (Apr 09 2019 at 16:41):

@Koundinya Vajjha Try choose k hk using h.

view this post on Zulip Koundinya Vajjha (Apr 09 2019 at 16:42):

Thanks Johan


Last updated: May 18 2021 at 07:19 UTC