feat: `USize.size` inequalities

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

feat: `USize.size` inequalities #6203

Open tydeu opened 1 day ago

tydeu commented 1 day ago

This PR adds the theorems le_usize_size and usize_size_le, which make proving inequalities about USize.size easier.

It also deprecates usize_size_gt_zero in favor of usize_size_pos (as that seems more consistent with our naming covention) and adds USize.toNat_ofNat_of_lt32 for dealing with small USize literals.

It also moves USize.ofNat32 and USize.toUInt64 to Init.Data.UInt.Basic as neither are used in Init.Prelude anymore.

tydeu commented 1 day ago

These inequalities could also be named USize.le_size and USize.size_le, but I stuck with the current usize_size convention. This also avoids a clash with batteries, which already defines them and uses 2 ^ _ to represent the size instead of the computed value. I used the computed value as that is also current core convention.

leanprover-community-bot commented 23 hours ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6203 has successfully built against this PR. (2024-11-25 00:02:56) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 43dfc2a25fc64095fb76d576802a70d88773fea8 --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-25 13:49:54)