Rewrite applies the wrong equational rule

[BrunoDutertre]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

On the following example, the rw tactic does not unfold a function definition (as it used to prior to 4.12.0).

structure LoopRange where
  start: Nat
  end_: Option Nat

namespace LoopRange
def isZero (r: LoopRange): Prop :=
  r = ⟨0, some 0⟩

def isZeroVar2 (r: LoopRange): Prop :=
  match r with
  | ⟨0, some 0⟩ => True
  | _ => False

example (r: LoopRange): r.isZeroVar2 ↔ r.isZero := by
  rw [isZeroVar2]
  sorry

end LoopRange

Instead, it looks as if rw [isZeroVar2] applies isZeroVar2.eq_2 which results in two unprovable subgoals:

Tactic state
 2 goals

 r : LoopRange
 ⊢ False ↔ r.isZero

 case x_1
 r : LoopRange
 ⊢ r = { start := 0, end_ := some 0 } → False

This variant does the right thing::

example (r: LoopRange): r.isZeroVar2 ↔ r.isZero := by
  rw [isZeroVar2.eq_def]
  sorry

Versions

4.12.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

I fear that's now the expected behavior. It always has been like this for recursive functions, and has become more uniform. Using rw [foo.eq_def] is the right work around.

[BrunoDutertre]

In other places, I've seen an error message like this

failed to rewrite using equation theorems for 'Option.isSome'. Try rewriting with 'Option.isSome.eq_def'.

But here, it's silently applying the wrong rewrite and there's no warning or hint at what to do.

[nomeata]

Yes, this only happens with function definitions that have a catch-all clause in the pattern match. These lead to rewrite rules that always apply, but introduce side goals. With simp that's fine, it won't apply the rule unless it can discharge these side goals. But rw is a bit too primitive for that, at least at the moment.

[Kha]

Closing as (new) expected behavior

[BrunoDutertre]

Is this documented somewhere? What is the new expected behavior of rw [<function-name>]?

[nomeata]

It's not new behavior of rw; it has always behaved like this with functions with multiple equational rules and overlapping patterns. Until 0.11 only recursive functions has multiple equational rules, since 0.12 all functions are treated the same in this regard. See breaking changes section in https://github.com/leanprover/lean4/releases/tag/v4.12.0 (although it's not explicitly calling out the this particular effect.)