Should wfrec defs require an @[irreducible] annotation?

Stream: lean4

[Jannis Limperg]

It feels like we're getting a lot of questions by people who are (reasonably) confused about their wfrec definitions being silently marked as irreducible. Would it be better to require that every wfrec definition has an explicit @[irreducible] annotation (or @[semireducible], @[reducible], abbrev to override the default)? This way the error message for a wfrec definition with no annotation could explain the situation.

[Jannis Limperg]

cc @Joachim Breitner

[Joachim Breitner]

That sounds like a very big hammer, and quite annoying.

Do you have a sense of whether most questions are by people upgrading their code and who have previously relied on the semireducibility of the wf construction (in which case the confusion might get less over time), or also users without much prior expectation?

[Shreyas Srinivas]

Joachim Breitner said:

That sounds like a very big hammer, and quite annoying.

Do you have a sense of whether most questions are by people upgrading their code and who have previously relied on the semireducibility of the wf construction (in which case the confusion might get less over time), or also users without much prior expectation?

Seconded. I think if people want wf rec functions to be reducible, it should be their call.

[Shreyas Srinivas]

Ideally this should be a config option one can set at a file level or a project level.

[Shreyas Srinivas]

But I don't know where this default should be instantiated. Should the tactic monads handle this issue automatically (which means they look at lakefiles ), or should it be the tactic implementers job to get this config information.

[Jannis Limperg]

Joachim Breitner said:

Do you have a sense of whether most questions are by people upgrading their code and who have previously relied on the semireducibility of the wf construction (in which case the confusion might get less over time), or also users without much prior expectation?

A mix of both I think. Certainly a bunch of new users. It doesn't help that at least FPIL and the Lean manual haven't yet been updated to reflect the new behaviour.

But even with these doc updates, I would argue that forcing an annotation would be good language design. A definition that doesn't reduce by default is very surprising, both from a general type theory perspective (where we rely on implicit computation all the time) and in comparison with any other DTT system I know of. It's even more surprising when the definition reduces in some contexts but not others (cf #lean4 > Why can't reduce?).

[Sebastian Ullrich]

A wfrec definition reducing is the surprising result. It is the only place in Lean where we have to reduce proofs. And because of that, it can get stuck for various reasons, in completely inscrutable ways for the user. Irreducibility is the only robust default for wfrec, and the robust way to reason about them is via their equation theorems.

[Sebastian Ullrich]

And there is a "choose one" dilemma between reducing as many wfrecs as possible and not importing proofs, which will be necessary to further scale big libraries in Lean in CPU, memory, and disk space

[Joachim Breitner]

Hmm, I see the issue, but I’m doubtful that forcing everyone to write something here is the right approach. It’s ugly (subjective aesthetics, I know), it’s requires a fair amount of technical expertise to make the right call here, and thus adds additional burden to every users, even those who don’t care (yet) about this distinction.

I’d expect that there is a fair fraction of users who are perfectly happy to use simp and rw in their proofs and shouldn’t be bothered about reducibility.

If anything, I could imagine requiring an explicit opt-in to well-founded recursion in the first place – this would provide some syntax that one can hover about and learn more, including the various pitfalls of well-founded recursion.

[Jannis Limperg]

Sebastian Ullrich said:

A wfrec definition reducing is the surprising result. It is the only place in Lean where we have to reduce proofs. And because of that, it can get stuck for various reasons, in completely inscrutable ways for the user. Irreducibility is the only robust default for wfrec, and the robust way to reason about them is via their equation theorems.

I'm not arguing against any of this. I'm just saying that new users (and perhaps some old users) have no idea about any of this proof reduction business. So to them, the fact that termination_by makes your function irreducible is surprising.

[Joachim Breitner]

(Or, worse, even without termination_by if the default termination tactics do their job.)

[Eric Wieser]

Perhaps we could address this with a linter that recommends adding the @[irreducible] explicitly?

[Eric Wieser]

(as opposed to actually making it required)

[Jannis Limperg]

Joachim Breitner said:

I’d expect that there is a fair fraction of users who are perfectly happy to use simp and rw in their proofs and shouldn’t be bothered about reducibility.

I don't think you can hide the complexity for long. Some silly examples:

def f (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => (f n) + 1
  termination_by n

-- works, special support I guess
example : f 0 = 0 := by
  rfl

-- fails
example : f 0 = 0 := by
  exact rfl

-- fails
example {P : Nat → Prop} (h : P 5) : P (f 5) := by
  exact h

[Jannis Limperg]

The linter is a good idea I think.

[Joachim Breitner]

That the first rfl works is in my opinion a bug (it ignores the current transparency setting in some cases) with a proposed fix in https://github.com/leanprover/lean4/pull/3772

[Sebastian Ullrich]

Jannis Limperg said:

Sebastian Ullrich said:

A wfrec definition reducing is the surprising result. It is the only place in Lean where we have to reduce proofs. And because of that, it can get stuck for various reasons, in completely inscrutable ways for the user. Irreducibility is the only robust default for wfrec, and the robust way to reason about them is via their equation theorems.

I'm not arguing against any of this. I'm just saying that new users (and perhaps some old users) have no idea about any of this proof reduction business. So to them, the fact that termination_by makes your function irreducible is surprising.

But consider also that both Lean and the whole field of DTT are slowly moving away from making reducible the default. Gratzer et al first discussed this in Controlling Unfolding in Type Theory, then implemented in various ways in various systems. Lean now has seal/unseal. We are not going to prevent people from making something reducible if they really want to but like with proofs, reducibility for everything, all the time, turns out not to be a great default if you also want scalability, modularity, and robustness. So expectations may shift in the future.

[Jannis Limperg]

I don't disagree with this direction, but Lean is currently very happy to implicitly reduce almost every definition. Wfrec is the odd one out. So unless you have plans to make everything irreducible by default in the near future, you will have confused users.

[Kim Morrison]

If there is a missing linter here (but I don't think there is!) it is one checking (how?) for useful rewriting lemmas after the definition, not for enforcing a redundant annotation.

[Shreyas Srinivas]

Maybe this belongs on the type theory channel, not sure, but why is unfolding proofs tricky?

[Shreyas Srinivas]

To add to the question, is the trickiness limited to pathological examples, or is it a major practical headache?

[Shreyas Srinivas]

A third question: when is it safe to use unseal?

[Shreyas Srinivas]

Is it okay to use it on an API lemma for a definition, while increasingly unsafe for definitions which are more downstream?

[Kyle Miller]

Acc.rec reduction in Lean 3 was really hit-or-miss, and then in 2021 it was disabled completely: https://github.com/leanprover-community/lean/pull/562

[Kyle Miller]

It could be feasible to have an error message on type mismatch errors that explains which definitions it ran into that were irreducible, explains why they might be, suggests using tactics, and explains, as a last resort that unseal exists.