# Zulip Chat Archive

## Stream: general

### Topic: Simplify dite statements

#### Rob Lewis (Aug 10 2018 at 12:12):

I've noticed the following:

def p : ℕ → ℕ := λ n, if h : n > 5 then 10 else 0 example (n : ℕ) (hn : n > 5) : p n = 10 := begin simp only [dif_pos, hn, p] end -- works example (n : ℕ) (hn : ¬n > 5) : p n = 0 := begin simp only [dif_neg, hn, p] end -- fails

What additional simp lemmas are needed to solve the second example? And is there a tactic in Mathlib with roughly this behavior, reducing dite statements where the positive or negative proof is in the context?

#### Gabriel Ebner (Aug 10 2018 at 12:17):

There is `split_ifs`

:

import tactic.split_ifs def p : ℕ → ℕ := λ n, if h : n > 5 then 10 else 0 example (n : ℕ) (hn : n > 5) : p n = 10 := by unfold p; split_ifs; refl example (n : ℕ) (hn : ¬n > 5) : p n = 0 := by unfold p; split_ifs; refl

#### Mario Carneiro (Aug 10 2018 at 12:19):

interestingly, this works:

example (n : ℕ) (hn : ¬n > 5) : p n = 0 := begin simp only [dif_neg hn, p] end

#### Kenny Lau (Aug 10 2018 at 12:19):

is it so interesting that it works?

#### Mario Carneiro (Aug 10 2018 at 12:20):

it is interesting that `simp`

won't connect the two parts together in the original version

#### Mario Carneiro (Aug 10 2018 at 12:20):

I suppose it is because `¬n > 5`

is not in simp normal form, so it gets rewritten and then the assumption `hn`

doesn't match

#### Rob Lewis (Aug 10 2018 at 12:21):

No? What is its simp normal form?

#### Rob Lewis (Aug 10 2018 at 12:22):

It still fails if you make the > a <.

#### Rob Lewis (Aug 10 2018 at 12:22):

@Gabriel Ebner Thanks, that's useful! Somehow I assumed `split_ifs`

did something different based on its name.

#### Mario Carneiro (Aug 10 2018 at 12:22):

in mathlib it will rewrite to `n <= 5`

#### Rob Lewis (Aug 10 2018 at 12:24):

constant A : ℕ → Prop constant had : decidable_pred A attribute [instance] had noncomputable def p : ℕ → ℕ := λ n, if h : A n then 10 else 0 example (n : ℕ) (hn : A n) : p n = 10 := begin simp only [dif_pos, hn, p] end -- works example (n : ℕ) (hn : ¬ A n) : p n = 0 := begin simp only [dif_neg, hn, p] end -- fails

#### Gabriel Ebner (Aug 10 2018 at 12:26):

Even better, it works without `only`

:

example (n : ℕ) (hn : ¬n > 5) : p n = 0 := by simp [p, hn]

#### Gabriel Ebner (Aug 10 2018 at 12:26):

It needs one extra lemma:

example (n : ℕ) (hn : ¬n > 5) : p n = 0 := by simp only [p, hn, dif_neg, not_false_iff]

#### Rob Lewis (Aug 10 2018 at 12:29):

Aha! Thanks.

Last updated: May 14 2021 at 03:27 UTC