Zulip Chat Archive

Stream: new members

Topic: Triggering reduction of ifthenelse in case analysis


view this post on Zulip Donald Sebastian Leung (Feb 28 2020 at 14:44):

In part of a proof involving real and natural numbers, I defined a natural number n as follows: let n : ℕ := if N < 0 then 0 else int.nat_abs (some (exists_floor N) + 1). Note here that N is a real number. I then perform case analysis on N < 0 and expected n to reduce to 0 in the case where the inequality holds and int.nat_abs (some (exists_floor N) + 1) in the other case. However, in both cases, I still have n : ℕ := ite (N < 0) 0 (int.nat_abs (some _ + 1)). How do I trigger reduction for n?

view this post on Zulip Reid Barton (Feb 28 2020 at 14:50):

Well, it's not a "reduction" in the sense of definitional equality. You can rewrite using if_pos/if_neg.

view this post on Zulip Reid Barton (Feb 28 2020 at 14:51):

Or more likely you should try split_ifs instead where you used case analysis.

view this post on Zulip Reid Barton (Feb 28 2020 at 14:51):

Which is just a more automated way of doing the same thing.

view this post on Zulip Donald Sebastian Leung (Feb 28 2020 at 14:54):

Hmmm ... I tried split_ifs at * (with the definition of n in my context as shown above) and Lean complained that there are no if-then-else expressions to split. Why might that be?

view this post on Zulip Reid Barton (Feb 28 2020 at 15:25):

Oh, when the if is in the body of a let I don't know if there is a convenient way.

view this post on Zulip Donald Sebastian Leung (Feb 28 2020 at 16:20):

Reid Barton said:

Well, it's not a "reduction" in the sense of definitional equality. You can rewrite using if_pos/if_neg.

Thanks, rw if_pos/rw if_neg worked for me after I solved the issue involving a let binding


Last updated: May 11 2021 at 23:11 UTC