wrong splitting of dif in v4.9.0-rc2

Stream: general

[Ira Fesefeldt]

when apply splitting to dependent if in the following proof, I get a wrong second case - its the same as the first one. This seems to be reproducible. When proving that goal, lean does not even seem to have a problem with that? I am a bit puzzled where the problem comes from.

I just switched to v.4.9.0-rc2.

import Mathlib
open unitInterval

noncomputable instance unitDiv : Div I :=
    ⟨fun i j => if h : i < j then ⟨i/j, sorry⟩ else 1⟩

lemma unitDiv_def {i j : I} :
    i / j = if h : i < j then ⟨i/j, sorry⟩ else 1 := rfl

lemma coe_div {i j : I} :
    ↑(i / j) = if i < j then (i/j : ℝ) else 1 := by
  rw [unitDiv_def]
  split <;> rfl

lemma zero_unit_div (i : I) (h : 0 < i) : 0 / i = 0 := by
  rw [Subtype.mk_eq_mk, coe_div]
  norm_cast
  split
  sorry -- goals: 0 / ↑i = 0, 0 / ↑i = 0 but should be 0 / ↑i = 0, 1 = 0

[Eric Wieser]

split_ifs behaves correctly here

[Kyle Miller]

Minimized it. The problem is that it's realizing that it notices the second case can't happen given the fact that the context says the condition is true, so it simplifies it as if it's the first case, when it should eliminate the second case. It's not generating incorrect proofs.

example (p : Prop) [Decidable p] (hp : p) (x y : Nat) :
    (if p then x else y) = 0 := by
  split
  /-
  case isTrue
  p : Prop
  inst✝ : Decidable p
  hp : p
  x y : ℕ
  h✝ : p
  ⊢ x = 0

  case isFalse
  p : Prop
  inst✝ : Decidable p
  hp : p
  x y : ℕ
  h✝ : ¬p
  ⊢ x = 0
  -/

[Kyle Miller]

Reported: lean4#4491