# Zulip Chat Archive

## Stream: new members

### Topic: Triggering reduction of ifthenelse in case analysis

#### 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`

?

#### 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`

.

#### Reid Barton (Feb 28 2020 at 14:51):

Or more likely you should try `split_ifs`

instead where you used case analysis.

#### Reid Barton (Feb 28 2020 at 14:51):

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

#### 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?

#### 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.

#### 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: Dec 20 2023 at 11:08 UTC