feat: add missing theorems for + 1 and - 1 normal form

[markusschmaus]

Nat.succ_eq_add_one and Nat.pred_eq_sub_one are now simp lemmas. For theorems about Nat.succ or Nat.pred without corresponding theorem for + 1 or - 1, this adds the corresponding theorem.

[markusschmaus]

This comment will track theorems involving Nat.succ, Nat.pred, and Nat.zero and whether there is an analogue for + 1, - 1, and 0.

Init.Prelude

I don't think the corresponding add_one theorems should be added to Init.Prelude, since this file is probably purposely kept small and the normal form hasn't been introduced yet. So I will add them to Init.Data.Nat.Basic

• Nat.not_succ_le_zero
  new: Nat.not_add_one_le_zero
• Nat.succ_le_succ: Nat.add_le_add_right
• Nat.zero_lt_succ: exists in Mathlib as Nat.add_one_pos
  new: Nat.zero_lt_add_one
• Nat.le_step: Nat.add_lt_add_right
• Nat.le_succ: Nat.le_add_right
• Nat.le_succ_of_le
  new: Nat.le_add_right_of_le
• Nat.succ_pos: exactly the same as Nat.zero_lt_succ
• Nat.pred_le_pred: Nat.sub_le_sub_right
• Nat.le_of_succ_le_succ: Nat.le_of_add_le_add_right
• Nat.le_of_lt_succ:
  new: Nat.le_of_lt_add_one
• Nat.not_succ_le_self
  new: Nat.not_add_one_le_self
• Nat.ble_succ_eq_true, skipped as per review
• List.length_cons: this is probably the worst offender, it's a simp lemma, that not only uses, but introduces succ. I think a proper solution is to rename this and remove @[simp], and define a new lemma with the same name using + 1 with @[simp]. This is a bigger change, which deserves its own PR.

Init.Data.Nat.Basic

• Nat.succ_add: Nat.add_right_comm
• Nat.add_succ: ←Nat.add_assoc
• Nat.pred_succ (simp):
  Nat.add_sub_cancel is simp
  Nat.add_one_sub_one is not simp
• Nat.succ_eq_one_add: Nat.add_comm
• Nat.mul_succ: Nat.mul_add introduces an additional 1 *
  new: Nat.mul_add_one
• Nat.succ_mul: Nat.mul_add introduces an additional 1 *
  new: Nat.add_one_mul
• Nat.succ_lt_succ: Nat.add_lt_add_right
• Nat.lt_succ_of_le
  new: Nat.lt_add_one_of_le
• Nat.succ_sub_succ_eq_sub: Nat.add_sub_add_right
• Nat.pred_le (simp): Nat.sub_le, but this isn't a simp lemma
• Nat.pred_lt: Nat.sub_lt, slightly different precondition, so probably worth addition a specialized theorem
  new: Nat.sub_one_lt
• Nat.sub_succ: Nat.sub_add_eq
• Nat.succ_sub_succ: Nat.add_sub_add_right
• Nat.lt.step: same as Nat.lt_succ_of_lt below
• Nat.le_of_succ_le: I would have expected a theorem of the form n + k ≤ m → n ≤ m, which would include this for k = 1, but I can't find such a theorem
  new: Nat.le_of_add_right_le
• Nat.lt_of_succ_lt: again there is no theorem for n + k < m → n < m
  new: Nat.lt_of_add_right_lt
• Nat.lt_of_succ_lt_succ: Nat.add_lt_add_right
• Nat.lt_of_succ_le: stating this for + k requires the condition 0 < k, so it makes sens to just state this for + 1
  new: Nat.lt_of_add_one_le
• Nat.succ_le_of_lt
  new: Nat.add_one_le_of_lt
• Nat.lt.base, Nat.lt_succ_self (simp)
  new: `Nat.lt_add_one_self (simp)
• Nat.le_or_eq_of_le_succ: Mathlib has the corresponding iff theorem: Nat.le_add_one_iff
  new: Nat.le_or_eq_of_le_add_one
• Nat.lt_succ_iff: this exists in Mathlib: Nat.lt_add_one_iff
  new: Nat.lt_add_one_iff', I think it would be good to have this theorem in core, I'm using the primed name for now
• Nat.lt_succ_iff_lt_or_eq
  new: Nat.lt_add_one_iff_lt_or_eq
• Nat.eq_of_lt_succ_of_not_lt: name uses succ, but statement uses + 1, maybe rename?
• Nat.eq_of_le_of_lt_succ: name uses succ, but statement uses + 1, maybe rename?
• Nat.succ_ne_self
  new: `Nat.add_one_ne_se
• Nat.succ_le, this exists in Mathlib as Nat.add_one_le_iff
  new: Nat.add_one_le_iff
• Nat.lt_succ: exactly the same as Nat.lt_succ_iff above
• Nat.lt_succ_of_lt: also see Nat.lt.step above
  new: Nat.lt_add_one_of_lt
• Nat.succ_pred_eq_of_ne_zero: exact Nat.sub_one_add_one_eq_of_pos
• Nat.eq_zero_or_eq_succ_pred
  new: Nat.eq_zero_or_eq_add_one_sub_one
• Nat.succ_inj': Nat.add_right_cancel_iff, maybe a specialized theorem for + 1 could be useful
• Nat.succ_le_succ_iff: Nat.add_le_add_iff_right
• Nat.succ_lt_succ_iff: Nat.add_lt_add_iff_right
• Nat.pred_inj
  new: Nat.sub_one_cancel
• Nat.pred_ne_self
  new: Nat.sub_one_ne_self
• Nat.pred_lt_self: Nat.sub_lt
• Nat.pred_lt_pred: generalization in Mathlib as Nat.sub_lt_sub_iff_right
  new: Nat.sub_lt_sub_right, proof could maybe be golfed
• Nat.pred_le_iff_le_succ: Nat.sub_le_iff_le_add
• Nat.le_succ_of_pred_le: Nat.le_add_of_sub_le
• Nat.pred_le_of_le_succ: Nat.sub_le_of_le_add
• Nat.lt_pred_iff_succ_lt: in Mathlib as Nat.lt_sub_iff_add_lt, skip for now due to name clash
• Nat.succ_lt_of_lt_pred: Nat.add_lt_of_lt_sub
• Nat.lt_pred_of_succ_lt: Nat.lt_sub_of_add_lt
• Nat.le_pred_iff_lt, there is no corresponding Nat.le_iff_lt_succ, only Nat.lt_succ_of_le and Nat.le_of_lt_succ
  new: Nat.le_sub_one_iff_lt
• Nat.le_pred_of_lt: Nat.le_sub_one_of_lt
• Nat.lt_of_le_pred:
  new: Nat.lt_of_le_sub_one
• Nat.exists_eq_succ_of_ne_zero
  new: Nat.exists_eq_add_one_of_ne_zero
• Nat.succ_ne_zero: Nat.add_one_ne_zero
• Nat.pow_succ: Nat.pow_add introduces an additional ^1
  new: Nat.pow_add_one
• Nat.pred_lt'
  new: Nat.sub_one_lt'
• Nat.succ_pred
  new: Nat.sub_one_add_one
• Nat.succ_pred_eq_of_pos: exact Nat.sub_one_add_one_eq_of_pos
• Nat.sub_le_succ_sub
  new: Nat.sub_le_add_right_sub
• Nat.sub_succ_lt_self: name uses succ, but statement uses + 1, maybe rename?
• Nat.succ_sub: Nat.sub_add_comm
• Nat.lt_of_sub_eq_succ
  new: Nat.lt_of_sub_eq_sub_one
• Nat.mul_pred_left
  new: Nat.mul_sub_one_left
• Nat.mul_pred_right
  new: Nat.mul_sub_one_right

Init.Data.Nat.Lemmas

• Nat.one_add: Nat.add_comm
• Nat.succ_eq_one_add: Nat.add_comm
• Nat.succ_add_eq_add_succ: There is no matching theorem, it would be possible to prove n + k + m = n + (m + k), but I'm hesitant to add it
• sub_one: ←Nat.pred_eq_sub_one
• Nat.succ_sub_sub_succ
  new: Nat.add_sub_sub_add_right
• Nat.succ_sub_one: Nat.add_one_sub_one
• Nat.sub_lt_succ
  new: Nat.sub_lt_add_one
• Nat.succ_min_succ: Nat.add_min_add_right
• Nat.succ_max_succ: Nat.add_max_add_right
• Nat.pred_min_pred: Nat.sub_min_sub_right
• Nat.pred_max_pred: Nat.sub_max_sub_right
• Nat.succ_mul_succ
  new: Nat.add_one_mul_add_one
• Nat.succ_mul_succ_eq: exactly equal to Nat.succ_mul_succ, maybe deprecate one of them?
• Nat.pow_succ'
  new: Nat.pow_add_one'
• Nat.pow_lt_pow_succ: name uses succ, statement uses + 1
• Nat.shiftLeft_succ_inside: name uses succ, statement uses + 1
• Nat.shiftLeft_succ: name uses succ, statement uses + 1
• Nat.shiftRight_succ_inside: name uses succ, statement uses + 1

Init.Data.Nat.Bitwise

• Nat.testBit_succ
  new: Nat.testBit_add_one
• Nat.succ_mod_two (private): since it's private, I'm not going to add this
• Nat.testBit_succ_zero (private)
• Nat.testBit_two_pow_sub_succ: name uses succ, statement uses + 1

Init.Data.Nat.Div

• Nat.add_div_right: introduces a succ should be handled in different PR
• Nat.add_div_left: introduces a succ, should be handled in different PR
• Nat.div_eq_of_lt_le: uses succ in the hypothesis (hi : m < succ k * n), I don't know what to call the + 1 theorem
• Nat.mul_sub_div: uses succ, but what should the alternative be called?

Init.Data.Nat.Gcd

• Nat.gcd_succ
  new: Nat.gcd_add_one

Init.Data.Nat.Mod

• Nat.mod_pow_succ: name uses succ, statement uses + 1

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-4242 built against this PR, but testing failed. (2024-05-21 15:58:34) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-05-24 13:35:52) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-05-24 20:52:16) View Log
• ❌ Mathlib branch lean-pr-testing-4242 built against this PR, but the archive failed. (2024-05-26 10:54:02) View Log
• ❌ Mathlib branch lean-pr-testing-4242 built against this PR, but testing failed. (2024-05-28 19:28:28) View Log
• ❌ Mathlib branch lean-pr-testing-4242 built against this PR, but testing failed. (2024-05-28 20:25:54) View Log
• ❌ Mathlib branch lean-pr-testing-4242 built against this PR, but testing failed. (2024-05-28 21:50:12) View Log
• ❌ Mathlib branch lean-pr-testing-4242 built against this PR, but testing failed. (2024-05-29 14:38:28) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-05-29 21:17:16) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-05-30 12:07:23) View Log
• ✅ Mathlib branch lean-pr-testing-4242 has successfully built against this PR. (2024-05-30 12:27:37) View Log
• 🟡 Mathlib branch lean-pr-testing-4242 build this PR didn't complete normally. (2024-05-30 19:13:46) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-01 16:44:00) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-01 17:44:17) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-02 23:03:09) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-03 09:04:47) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-03 09:08:37) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-03 11:32:56) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-03 13:29:48) View Log
• ✅ Mathlib branch lean-pr-testing-4242 has successfully built against this PR. (2024-06-04 10:27:02) View Log
• 💥 Mathlib branch lean-pr-testing-4242 build failed against this PR. (2024-06-05 15:45:54) View Log
• ✅ Mathlib branch lean-pr-testing-4242 has successfully built against this PR. (2024-06-05 16:53:20) View Log

[markusschmaus]

I think I've covered everything in Init.Data.Nat with a few exceptions. List.length_cons, Nat.add_div_right, and Nat.add_div_left are simp-lemmas which introduce succ, they should go into a separate PR. Two other minor exceptions are Nat.div_eq_of_lt_le1 and Nat.mul_sub_div primarily due to unclear naming. There are some more in Init.Data.Int, but I think that this also should be a separate PR.

CI keeps failing, is this because I changed to doc-string for Nat? Should I revert this? Or is this just some infrastructure trouble which will get resolved independently?

[kim-em]

There are four test failures, and they are caused by this PR. Have a go at fixing them, please, but feel free to ping if you get stuck.

[kim-em]

For such a potentially disruptive change, we'll also need a successful Mathlib build. You can push changes to the lean-pr-testing-4242 branch at Mathlib, and results will be reported back here. (If you don't have write access there, please ask.)

[markusschmaus]

I think I understand what is happening.

[04:30 (00.000366)] lean-test-stage1> -  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
[04:30 (00.001027)] lean-test-stage1> +  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form 

I changed the doc-string of Nat.succ to make clear that + 1 is the preferred choice. But hover.lean.expected.out still contains the old doc-string.

Is my change to the doc-string good? Should I revert to the prior doc-string? Or do you have a better suggestion?

If the doc-string is good, I would just copy-paste the output as it currently is produced into hover.lean.expected.out.

[markusschmaus]

I fixed some failing tests. Keeping the doc-string as is and changing the tests.

The remaining failures also show up in PR #4263, so I wait until they are resolved there, in the hopes it will resolve them here as well.

[markusschmaus]

@markusschmaus, could you provide a link showing the diff required at Mathlib? (i.e. the diff from the head of lean-pr-testing-4242 back to where it departed from nightly-testing). I'd like to be able to review that at the same time.

I'm not sure what you mean, lean-pr-testing-4242 shows the diff at the bottom. Do you want me to create a Mathlib PR? The only meaningful change is the one in test/LibrarySearch/basic.lean. But there will be two more changes if I move the theorems from Mathlib to core as I mention above.

[kim-em]

@markusschmaus, could you provide a link showing the diff required at Mathlib? (i.e. the diff from the head of lean-pr-testing-4242 back to where it departed from nightly-testing). I'd like to be able to review that at the same time.

I'm not sure what you mean, lean-pr-testing-4242 shows the diff at the bottom. Do you want me to create a Mathlib PR? The only meaningful change is the one in test/LibrarySearch/basic.lean. But there will be two more changes if I move the theorems from Mathlib to core as I mention above.

That link is all I was looking for. Sorry, could have made it myself!

[kim-em]

Would you mind clicking resolve on conversations above that you're sure have been resolved satisfactorily?

[kim-em]

Okay, I think I am mostly happy. It would be great if you could get a builds-mathlib label again (it's possible that would require rebasing onto nightly-with-mathlib again, and then rebasing or merging Mathlib's lean-pr-testing-4242 so it builds off the corresponding nightly-testing-YYYY-MM-DD).

Or at least assure me that once this lands, merging lean-pr-testing-4242 into nightly-testing will go smoothly!

[markusschmaus]

Nat.add_one_pos already exists in Mathlib, I created the same theorem in core with the name Nat.zero_lt_add_one analogous to Nat.zero_lt_succ. First, what is the correct name? Second, should I remove the theorem in Mathlib with a deprecated abbrev?

[kim-em]

Let's go with the _pos name.

[markusschmaus]

Everything is green. What's next?

[kim-em]

Sorry, I'd lost track of this one. Reviewing again now. (I ran into problems where this PR would have helped, and was surprised it hadn't landed, oops!)