Simplify dite statements

Stream: general

[Rob Lewis]

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]

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]

interestingly, this works:

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

[Kenny Lau]

is it so interesting that it works?

[Mario Carneiro]

it is interesting that simp won't connect the two parts together in the original version

[Mario Carneiro]

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]

No? What is its simp normal form?

[Rob Lewis]

It still fails if you make the > a <.

[Rob Lewis]

@Gabriel Ebner Thanks, that's useful! Somehow I assumed split_ifs did something different based on its name.

[Mario Carneiro]

in mathlib it will rewrite to n <= 5

[Rob Lewis]

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]

Even better, it works without only:

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

[Gabriel Ebner]

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]

Aha! Thanks.