`isDefEq` unfolds recursive definition

[nomeata]

This is something I have seen today during office hours, and is plausible the reason for significant slow downs.

Consider

def foo : Nat → Nat
  | 0 => 0
  | (n +1) => foo n + 1
termination_by n => n

example (h : n = m) (h2 : foo n > 42) : foo (m + 1) > 42 :=
  set_option trace.Meta.isDefEq true in
  (h ▸ h2)

The trace shows something like

[Meta.isDefEq] ❌ foo (n + 1) > 42 =?= foo n > 42 ▼
  [] ❌ foo (n + 1) =?= foo n ▼
    [] ❌ n + 1 =?= n ▶
    [] ❌ WellFounded.fix foo.proof_1
          (fun a a_1 =>
            (match (motive :=
                (x : Nat) → ((y : Nat) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Nat) → Nat) a with
              | 0 => fun x => 0
              | Nat.succ n => fun x => x n ⋯ + 1)
              a_1)
          (n +
            1) =?= WellFounded.fix foo.proof_1
          (fun a a_1 =>
            (match (motive :=
                (x : Nat) → ((y : Nat) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Nat) → Nat) a with
              | 0 => fun x => 0
              | Nat.succ n => fun x => x n ⋯ + 1)
              a_1)
          n ▶
  [] ❌ 42 < foo (n + 1) =?= 42 < foo n ▶

and I wonder if this means that ▶ is using isDefEq at the wrong reducibility setting.

Wrapping this in by with_reducible exact avoids going near WellFounded.fix, as expected.

Maybe unrelated, but it seems it tries the same equality twice, ordered differently:

[Meta.isDefEq] ❌ foo (n + 1) > 42 =?= foo n > 42 ▶

[Meta.isDefEq] ❌ foo n > 42 =?= foo (n + 1) > 42 ▶

Versions

4.7.0

Impact

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

[leodemoura]

This is an issue with isDefEq. I have revised the title. Yes, it is worth reconsidering whether we should unfold declarations defined using well-founded recursion in isDefEq. The current default behavior is to unfold them. This seldom produces desirable results, although some users rely on these definitions being unfolded. One option is to introduce a flag to control whether declarations defined by well-founded recursion can be unfolded by isDefEq. This flag would be set to false by default, but users could set it to true when needed. We could also provide better diagnostics (e.g., indicating functions that were not unfolded).

Remark: Declarations defined by structural recursion are unfolded all the time in practice by isDefEq, and many users rely on this.

We have been postponing the introduction of the flag because we will have a module system that will allow us to control much more precisely what can be unfolded and where it can occur.

[nomeata]

That is one way to ask the question - should wf-recursive functions be unfolded with default transparency (usually not).

But what about the alternative question we could ask: should a “rewriting-like” tactic like ▶ use default setting or should it use reducible setting? Especially as it seems to perform failing isDedEq checks even when the tactic is overall successful (now shown in this example).

For conv we recently changed the setting of the terminal try rfl to reducible. I have a gut feeling that here, too, we don't want to spend too much time on a backtracked DefEq check, independent of whether there is a wf-recursive or other function involved.

[leodemoura]

But what about the alternative question we could ask: should a “rewriting-like” tactic like ▶ use default setting or should it use reducible setting?

Users rely on default setting in multiple places.