Regression in 4.15.0 for simp with match expressions

Stream: lean4

[Eric Wieser]

I was looking over some old code, and this works in Lean 4.14.0 but fails in 4.15.0 onwards:

def foo : Nat × Nat := sorry

theorem foo_eq : let (a, b) := foo; a = b := sorry

example : let (a, b) := foo; a = b := by
  simp [foo_eq]

example : foo.1 = foo.2 := by
  simp [foo_eq]

Was this a deliberate change, or one I can opt out of with a new flag to simp? Or was this never supposed to work in the first place?

[Shreyas Srinivas]

simp +decide [foo_eq] did the trick for me

[Shreyas Srinivas]

But so did just decide

[Jz Pan]

Interestingly, if a = b is only propositionally equal then you get the other way around:

variable (foo : Nat × Nat)
variable (foo_eq : let (a, b) := foo; a = b)

include foo_eq in
example : let (a, b) := foo; a = b := by
  simp [foo_eq] -- does not work, it says "unknown constant '_example.match_1'"

include foo_eq in
example : foo.1 = foo.2 := by
  simp [foo_eq] -- it works

[Eric Wieser]

Thanks @Jz Pan, indeed the decide success was an artifact of over-minimization, your version is more faithful to the original. I edited mine above to remove the defeq.

[Jz Pan]

And the error message is "unknown constant '_example.match_1'" which is very strange.

[Eric Wieser]

replacing the example with a theorem fixes that

[Eric Wieser]

It doesn't fix my version though

[Jz Pan]

And exact foo_eq; sorry works (it complains on sorry that "no goals to be solved"), exact foo_eq does not work

[Jz Pan]

Eric Wieser said:

It doesn't fix my version though

In your version, use rw instead of simp works, but foo is required to be irreducible otherwise it wants sorry.fst ???

@[irreducible] def foo : Nat × Nat := sorry

theorem foo_eq : let (a, b) := foo; a = b := sorry

theorem test1 : let (a, b) := foo; a = b := by
  simp only
  rw [foo_eq]

theorem test2 : foo.1 = foo.2 := by
  rw [foo_eq]

[Jz Pan]

Another solution is use simp [id foo_eq] instead of simp [foo_eq]. But interestingly, if foo is not irreducible then it will complains that the proof of test1 and test2 uses sorry...

@[irreducible] def foo : Nat × Nat := sorry

theorem foo_eq : let (a, b) := foo; a = b := sorry

theorem test1 : let (a, b) := foo; a = b := by
  simp [id foo_eq] -- works

theorem test2 : foo.1 = foo.2 := by
  simp [id foo_eq] -- works

[Jovan Gerbscheid]

Note that this does work:

def foo : Nat × Nat := sorry

theorem foo_eq : let (a, b) := foo; a = b := sorry

example : let (a, b) := foo; a = b := by
  simp -iota [foo_eq]