Zulip Chat Archive

Stream: general

Topic: split_ifs weirdness


Reid Barton (Sep 28 2020 at 18:59):

Does anyone understand why split_ifs is producing two copies of 1 = 1 here?

import data.set.basic

open_locale classical

example {X Y : Type*} {f : X  Y} {s : set Y} {x : X} {t : set }
  {k : x  f ⁻¹' s} :
  (if h : f x  s then 1 else 0)  t :=
begin
  have : (if h : f x  s then 1 else 0) = 1,
  { split_ifs,
    refl, refl /- !! -/ },
  sorry
end

Reid Barton (Sep 28 2020 at 19:00):

There are a couple behaviors I could understand... but this is not one of them

Reid Barton (Sep 28 2020 at 19:02):

With trace.simplify.rewrite I can see that dif_pos was applied twice

Reid Barton (Sep 28 2020 at 19:03):

while if the hypothesis k is removed then it applies dif_pos once and dif_neg once as expected, and the second goal is 0 = 1

Gabriel Ebner (Sep 29 2020 at 06:46):

Apparently split_if uses all assumptions to simplify the ifs. If you change k : x ∈ f ⁻¹' s to k : f x ∈ s then it would produce only a single goal.


Last updated: Dec 20 2023 at 11:08 UTC