leanprover/lean4

Rewrite applies the wrong equational rule

Closed this issue · 8 comments

BrunoDutertre commented

Prerequisites

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

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 commented

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 commented

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 commented

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 commented

Closing as (new) expected behavior

BrunoDutertre commented

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

nomeata commented

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.)

BrunoDutertre commented

Yes, I saw the release notes. Let me try to clarify my question.

My function definition looks like this:

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

There are four equational rules for this definition:

LoopRange.isZeroVar2.eq_1 : { start := 0, end_ := some 0 }.isZeroVar2 = True

LoopRange.isZeroVar2.eq_2 (r : LoopRange) (x_1 : r = { start := 0, end_ := some 0 } → False) : r.isZeroVar2 = False

LoopRange.isZeroVar2.eq_def (r : LoopRange) :
  r.isZeroVar2 =
    match r with
    | { start := 0, end_ := some 0 } => True
    | x => False

LoopRange.isZeroVar2.eq_unfold :
  isZeroVar2 = fun r =>
    match r with
    | { start := 0, end_ := some 0 } => True
    | x => False

How does the tactic rw [isZeroVar2] decide which of these four rules to apply?

nomeata commented

It tries .eq_1 and then .eq_2.

Unfortunately the second applies even when the user probably doesn't want it to apply, because it's a conditional rule, and rw will apply it always, leaving the side-condition as a new goal (unlike simp, which only applies it if it can discharge the side-condition).