experiment making `succ_eq_add_one` @[simp]`

Stream: mathlib4

[Kim Morrison]

I've been experimenting with adding @[simp] to Nat.succ_eq_add_one. I got a fair way, but have run out of time for now.

If anyone would like to see if they can push it through, please use the lean-pr-testing-3579 branch.

[Kim Morrison]

Mostly, fixing it consists of finding places where simp is looping because it is being given lemmas that introduce succ.

[Kim Morrison]

But the current errors on that branch look a bit weirder.

[Kim Morrison]

I think it would be nice to be certain that Nat.succ never appeared in the simp normal form of a Nat expression.

[Johan Commelin]

There were also plans to make +1 the default syntax used in induction/recursion. I guess that should maybe be done first?

[Kim Morrison]

It doesn't seem necessary to do that first.

[Johan Commelin]

I think Kyle Miller was working on that.

[Kim Morrison]

Both make sense to do, but it hasn't been on obstacle on this toolchain/branch.

[Johan Commelin]

Right, it's not a "formal" prerequisite.

[Johan Commelin]

But I always refrained from adding that simp attribute, because it felt to me like you're fighting a tide if induction doesn't cooperate.

[Kim Morrison]

Better to fight the tide than drown in succs. :-)

[Eric Wieser]

Scott Morrison said:

I've been experimenting with adding @[simp] to Nat.succ_eq_add_one. I got a fair way, but have run out of time for now.

If anyone would like to see if they can push it through, please use the lean-pr-testing-3579 branch.

Might it make more sense to add this attribute in mathlib initially so that it doesn't end up tied to the cadence of lean releases? Or is there too much stuff about succ in core/std for that to work?

[Kim Morrison]

Yes, it requires changes in the lean4 repository, and I would like to have the benefits there, too.

[Kim Morrison]

Moreover, I would like to reduce the discrepancies between the simp normal forms in different libraries, rather than increase them!

[Kim Morrison]

We're starting to add test files in Lean verifying various simp reductions. It would be great if we could start running these automatically post-Mathlib to guard against breakages.

[Kim Morrison]

(obviously this requires coordination, and there's no obligation on Mathlib to not break things, but if we can pull it off it makes life better for everyone)

[Kyle Miller]

Johan Commelin said:

I think Kyle Miller was working on that.

The obstruction so far has been issue lean4#3022, where the custom induction principle ends up with expressions such as Nat.add n 0 instead of n.

[Kim Morrison]

Leo has just fixed this!

[Kim Morrison]

Unfortunately Mathlib's lean-pr-testing-3579 branch is an unusable state right now, but hopefully I will get it working soon. I would love to add @[simp] to succ_eq_add_one now!

[Kyle Miller]

Thanks to lean4#3616, I've now gone ahead and made lean4#3629 for making custom induction/cases principles (thanks @Adam Topaz for the initial work on creating these attributes) and giving Nat the custom principles we've long wanted.

[Kyle Miller]

Beyond needing to be reviewed, merging will also need to wait for a mathlib that includes lean4#3616, to create the likely large bump PR

[Kim Morrison]

nightly-testing currently has lots fo failures from lean4#3616. Fixes welcome!

[Markus Schmaus]

Making · + 1 the normal form looks like the right decision to me, and adding @[simp] to Nat.succ_eq_add_one is a great first step. However this transition is as of now incomplete even for core, for example docs#List.length_cons still introduces Nat.succ, and there is no theorem equivalent to docs#Nat.pred_succ for · + 1 and · - 1.

I would like to create a PR which addresses some of these issues, which I find easy to fix. This would be my first PR for Lean. Would such a PR be welcomed? Is there enough bandwidth to review such a PR? How long should I expect a review cycle to take?

[Kim Morrison]

Yes, I can review a PR to change the RHS of length_cons, and similarly (separately?) to add an analogue of pred_succ.

Please make sure you base it off the nightly-with-mathlib tag, so we get automatic testing of downstream projects.

[Markus Schmaus]

There are quite a few more such theorems with missing analogues, my first instinct would have been to collect them all into a single PR. But it sounds that I should make a separate PR for each.

I'm looking at CONTRIBUTING.md, does it make sense to create a RFC issue for this?

[Kim Morrison]

I think two PRs will suffice: one that tries to avoid Nat.succ or Nat.pred on the RHS of a lemma, when the arithmetical version suffices, and then a second one that introduces the missing analogues.

[Kim Morrison]

For the second such PR, perhaps tell me something more about how many lemmas you anticipate adding?

[Kim Morrison]

For the first such PR, no RFC necessary, this discussion will do.

[Markus Schmaus]

So far in my personal project I organically encountered three cases: Nat.succ_eq_one_add, Nat.succ_le_of_lt, Nat.pred_lt, which all belong in the second PR. I found the examples I gave here (Nat.pred_succ, and List.length_cons) using loogle.

They all fall into the useful, but trivially to prove, category, so the work is primarily to find each theorem, check if an analogous theorem already exists and add it otherwise. That's why my plan is to fix them all in one go. I don't know how many theorems these are. To avoid disruption, I don't plan to remove any theorems, just to add the missing ones.

Next step for me is to set up the two PRs with the examples I already have, and see if they look good. Then add additional examples later.

[Markus Schmaus]

I've started a draft PR. I based it on nightly-with-mathlib and the first commit only changed documentation (for Nat.succ), but the CI test failed nevertheless.

Most of the work consists of identifying the functions and checking if a substitute exists, as I do in this comment. A ✓ means that I found a theorem that I believe is a suitable substitute, while "new" is the name of the new theorem.

[Kim Morrison]

Sorry about the Mathlib CI failure. This may be an interaction with recent changes in Lake, I'll investigate. I'm hoping it may just come good when you get your PR to build next, and or rebase it onto nightly-with-mathlib again (this tag gets overwritten every day).

[Derrik Petrin]

I've been going through TPIL recently and ran into this change breaking several of the examples in the Inductive Types chapter (basically all of the tactic proofs at the end of Defining the Natural Numbers).

[Derrik Petrin]

And as a minimal case, this proof leads to simp looping:

example (m n : Nat) : m + Nat.succ n = Nat.succ (m + n) := by
  simp [Nat.add_succ]

[Kim Morrison]

Thanks @Derrik Petrin for the heads up on this. I guess that PRs for #tpil are welcome? I think @Patrick Massot and @Jeremy Avigad are the most likely people to do an overall update.

[Derrik Petrin]

Is there a different lemma that the TPIL examples should be using?

[Kim Morrison]

Well, in my opinion it should be proving a different statement, now that we try to hide Nat.succ as much as possible from users!

[Kim Morrison]

example (m n : Nat) : m + Nat.succ n = Nat.succ (m + n) := by
  simp [Nat.add_assoc]

[Kim Morrison]

I do wonder if turning Nat.add_assoc into a global simp lemma would be fine. I am increasingly in favour of including associativity lemmas in the simp set.

[Derrik Petrin]

Since that particular section/chapter is using Nat to demonstrate defining and using inductive types, it probably wants to keep succ explicit. But I'll see if using assoc works for the affected example proofs.

[Kim Morrison]

Yes, it really needs to be updated to use a MyNat!

[Derrik Petrin]

Ah, yep, that sounds like the overall best move here :)

[Derrik Petrin]

Considering one of the proofs is for add_assoc itself, using simp [add_assoc] feels a little like cheating :yum:

[Derrik Petrin]

In the meantime, simp only [...] seems to work fine.

[Kim Morrison]

We'll see what happens to Mathlib on lean#4539.

[Patrick Massot]

Kim Morrison said:

Thanks Derrik Petrin for the heads up on this. I guess that PRs for #tpil are welcome? I think Patrick Massot and Jeremy Avigad are the most likely people to do an overall update.

I have nothing to do with TPIL, I’m only an author of #mil.

[Jeremy Avigad]

TPIL is due for a major overhaul. I added an issue on Github.

[Kim Morrison]

Kim Morrison said:

We'll see what happens to Mathlib on lean#4539.

It's not good. I think we would need to reverse the direction of Nat.add_assoc before we could consider making it a @[simp] lemma, but this first step would itself be highly disruptive.

[Yaël Dillies]

What' s your general rationale behind associativity lemmas becoming simp lemmas?

[Kim Morrison]

They don't seem to hurt, generally, it improves canonicalisation, and often with some additional lemmas (e.g. as generated by @[reassoc] in the category theory library) you can effectively to rewriting up to associativity without any additional automation.

[Yaël Dillies]

Yes, but the counterargument is that you don't want a nonterminal simp to shuffle your goal around. As in, I'm fine with simp reassociating my goal when it closes it anyway, but I'm not fine with having to remove the associativity lemmas one by one from a nonterminal simp only to make sure my goal isn't shuffled around.

[Yaël Dillies]

Commutativity lemmas also improve canonicalisation, yet there is a pretty clear consensus that they shouldn't be simp lemmas

[Yaël Dillies]

In fact, distributivity lemmas also improve canonicalisation, yet we have decided that they really shouldn't be simp lemmas, at least when they are not affine

[Peter Nelson]

and_congr_left_iff and and_congr_right_iff are two useful simp lemmas, and they can’t both be simp if associativity is simp in either direction.

These are the ones I come across personally, but there are analogues where the goals are arithmetic rather than logic.

[Peter Nelson]

Edit: I guess they can be simp, but would compete with simped associativity in cases where they are the better choice.

[Kim Morrison]

We can restore confluence by adding additional lemmas, e.g.

@[simp] theorem foo {a a' b c : Prop} : ((a ∧ b) ∧ c ↔ (a' ∧ b) ∧ c) ↔ (b ∧ c) → (a ↔ a') :=
  by simp only [and_assoc, and_congr_left_iff]

Of course there may be too many for this to be viable. Joachim has a lovely automated tool for identifying missing confluence lemmas.

[Markus Schmaus]

I've started the experiment of making the inverse of Nat.add_assoc a simp lemma in this draft PR and CI succeeds for Lean.

I needed to fix a lot of proofs, but the fixes where pretty trivial, and only in one place I had to use simp [..., - Nat.add_assoc]and at least a few proofs became simpler in the sense, that simp required fewer additional lemmas.

I will check how this would impact Mathlib and Batteries, when I find the time in the next few days.

[Kim Morrison]

Thanks for investigating. I will be curious what you find!

[Markus Schmaus]

The fixes for batteries are done. Just like in core search and replacing ← Nat.add_assoc with Nat.add_assoc' and Nat.add_assoc with Nat.add_assoc' works for most cases. This leads to a few rfl becoming superfluous which need to be deleted. There were a few places where bigger changes were needed, almost all of them were in Batteries/Data/String/Lemmas.

[Markus Schmaus]

Mathlib now builds as well with these fixes.

[Kim Morrison]

Those are surprisingly good.

[Kim Morrison]

We'll need to think a bit further on this, and consult, but I am cautiously optimistic that we can at least add this lemma, and possibly make it @[simp]. It's good to see that this does not actually break anything in Mathlib in the manner Yaël was concerned about above. (Is that right?)

[Yaël Dillies]

Changes like this one do look suspicious

[Kim Morrison]

That proof should be by simp [choose]; omega in any case. We shouldn't be fighting with Nat by hand unnecessarily anymore. :-)

[Markus Schmaus]

There were a couple of proofs where omega would have significantly simplified things. For this experiment I decided to avoid it and tried to stick as close as possible to the style of proofs that I found, so I could better understand the impact of adding this simp lemma. Here is another example in which omega would have worked wonders.

Many of the proofs that needed manual adjustments used docs#Nat.add_comm and docs#Nat.add_left_comm to arrange the summands in an order which allowed another lemma to be used, this often conflicted with the normal form defined by Nat.add_assoc', sometimes switching to docs#Nat.add_right_comm fixed things, in other cases I used the Nat.add_rotate lemma I introduced (analogous to docs#add_rotate), since it goes from normal form to normal form.

[Kim Morrison]

Yes, I think you've taken the right approach for this experiment, being conservative about replacing Nat-fighting with omega. It was more intended as "in future, I hope we will do less Nat-fighting".

[Michael Rothgang]

Kim Morrison said:

Joachim has a lovely automated tool for identifying missing confluence lemmas.

:tada: Can this tool run on mathlib? What is its current output there? Should this run more regularly, after fixing things if needed?

[Kim Morrison]

It probably could, but it will suggest a lot! I am planning on starting to run it on the List API in Lean soon(*), and hopefully gain some experience there before we try it at larger scales.

[Michael Rothgang]

Kim Morrison said:

It probably could, but it will suggest a lot! I am planning on starting to run it on the List API in Lean soon(*), and hopefully gain some experience there before we try it at larger scales.

But mathlib also has a lot it would like fixed, right? So I see that as a good thing (and agree with a gradual roll-out).