feat: upstream lemmas about basic List/Array operations

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

feat: upstream lemmas about basic List/Array operations #4059

Closed semorrison closed 1 week ago

semorrison commented 2 weeks ago

This PR upstreams lemmas about List/Array operations already defined in Lean from std/batteries.

Happy to take suggestions about increasing or decreasing scope.

digama0 commented 2 weeks ago

For this and future moves, would it be possible to follow the same protocol we used during the port, and have the initial commit be a plain copy/paste job so that the diffs needed to make it compile (and any additional changes) stand out more clearly?

semorrison commented 2 weeks ago

For this and future moves, would it be possible to follow the same protocol we used during the port, and have the initial commit be a plain copy/paste job so that the diffs needed to make it compile (and any additional changes) stand out more clearly?

Ah, yes, sorry, I know you've asked this before. I'll try to remember. It's a bit difficult to know where exactly to make that commit here: I initially copy-pasted in the entire files that I was drawing from, and then whittled down as dependencies weren't available or I decided I didn't want something upstreamed.

digama0 commented 2 weeks ago

As long as the diff isn't a complete mess, I think it's okay if the first commit includes the entirety of the affected files and hence subsequent commits contain a lot of red

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e733149134a9fa9e92bc589afbe6c2cbb665835c --onto b470eb522bfd68ca96938c23f6a1bce79da8a99f. (2024-05-03 04:25:49)
❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e733149134a9fa9e92bc589afbe6c2cbb665835c --onto 00cf5771f31e7de7f6ab3089cb4b9ffa606a35ed. (2024-05-06 03:54:35)