## Stream: new members

### Topic: Simplifying decidable propositions

#### Pedro Minicz (Jun 14 2020 at 02:06):

How do I simplify decidable propositions?

#### Pedro Minicz (Jun 14 2020 at 02:06):

def f (n : ℕ) : bool :=
if n = 0 then tt else if n = 1 then tt else ff

example : f 1 = tt :=
begin
unfold f,
sorry
end


#### Pedro Minicz (Jun 14 2020 at 02:07):

On sorry the goal is ite (1 = 0) tt (ite (1 = 1) tt ff) = tt. I know that 0 ≠ 1, so how do I simplify past the first ite.

#### Pedro Minicz (Jun 14 2020 at 02:09):

I know that comp_val can close this particular goal, but it wouldn't be able to if the whole expression wasn't computable.

#### Jalex Stark (Jun 14 2020 at 02:11):

norm_num closes the goal

#### Jalex Stark (Jun 14 2020 at 02:11):

split_ifs does something useful

#### Jalex Stark (Jun 14 2020 at 02:12):

example : f 1 = tt :=
begin
unfold f,
split_ifs; simp,
end


#### Jalex Stark (Jun 14 2020 at 02:13):

I think this is closer to the answer you were looking for,

def f (n : ℕ) : bool :=
if n = 0 then tt else if n = 1 then tt else ff

example : f 1 = tt :=
begin
unfold f,
rw if_neg, swap, { norm_num },
rw if_pos, refl,
end


#### Pedro Minicz (Jun 14 2020 at 02:15):

Thank you! if_pos/if_neg work perfectly!

#### Jalex Stark (Jun 14 2020 at 02:19):

split_ifs does something like "rw with if_pos or if_neg at all the ites in the goal"

#### Jalex Stark (Jun 14 2020 at 02:19):

well, that's my mental model of it, tactic#split_ifs can say something more accurate

#### Pedro Minicz (Jun 14 2020 at 02:45):

Is there a tactic that does something like this:

import data.real.basic

def f (n : ℕ) : bool :=
if n = 0 then tt else if n = 1 then tt else ff

example : ∀ n > 1, f n = ff
| 0 h := false.elim (not_lt_bot h)
| 1 h := false.elim (irrefl 1 h)
| (n+2) h := by { simp [f], split, cc, linarith }


#### Pedro Minicz (Jun 14 2020 at 02:47):

I'd like to have a convenient cases on ℕ, without having to apply casesmultiple times or refine a monstrous λ x, match x with ... end.

#### Bryan Gin-ge Chen (Jun 14 2020 at 02:58):

For this example, you don't need to pattern match at all:

import data.real.basic

def f (n : ℕ) : bool :=
if n = 0 then tt else if n = 1 then tt else ff

example {n : ℕ} (h : n > 1) : f n = ff :=
by { simp [f], split; linarith }


#### Pedro Minicz (Jun 14 2020 at 03:02):

Yes, I am aware. It is just a toy example for demonstration.

#### Reid Barton (Jun 14 2020 at 03:08):

For a small number of cases you could write rcases n with _|_|_|_... otherwise it depends on what you want to do.

#### Pedro Minicz (Jun 14 2020 at 03:23):

Thanks that works perfectly.

#### Pedro Minicz (Jun 14 2020 at 03:24):

I had tried rcases n with ⟨_|_|_⟩ with no success. Good to know rcases can handle it.

#### Scott Morrison (Jun 14 2020 at 04:13):

Occasionally it's useful to do something like by_cases h : x < 5 and then in the "true" branch, interval_cases h, which explodes into individual cases.

Last updated: May 08 2021 at 18:17 UTC