Zulip Chat Archive

Stream: general

Topic: Simplify dite statements


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 10 2018 at 12:19):

is it so interesting that it works?

view this post on Zulip Mario Carneiro (Aug 10 2018 at 12:20):

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

view this post on Zulip 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

view this post on Zulip Rob Lewis (Aug 10 2018 at 12:21):

No? What is its simp normal form?

view this post on Zulip Rob Lewis (Aug 10 2018 at 12:22):

It still fails if you make the > a <.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 12:22):

in mathlib it will rewrite to n <= 5

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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]

view this post on Zulip Rob Lewis (Aug 10 2018 at 12:29):

Aha! Thanks.


Last updated: May 14 2021 at 03:27 UTC