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

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