Triggering reduction of ifthenelse in case analysis

Stream: new members

[Donald Sebastian Leung]

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?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Donald Sebastian Leung]

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?

[Reid Barton]

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

[Donald Sebastian Leung]

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