feat: Port the list part of bi/big_op.v

[lzy0505]

Description

Part of #113.

Ported big_[and/or/sep]L, and big_sepL2.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[markusdemedeiros]

Nice code, and thanks for the time you put into refactoring! I left comments with improvements, but didn't tag every instance of every improvement.

Some are just suggestions for style improvements, like you asked for. Some are refactoring opportunities I haven't tried, but would try if I were doing the final pass over this PR to try and clean up the bigger proofs--some of the bigger ones in BigSepList should be tried to be improved if at all possible. What you do with these are a judgment call on your end, because I'd say this code is pretty good :)

[markusdemedeiros]

In cases like this, where the matching is overwhelming, doesn't bind anything, and not very informative, I think using a first | · tac1 | · tac2 | ... is a lot cleaner. Here, try

cases l1, l1', l2, l2' <;> first | · exact .rfl | · simp at hl2 | · simp at hl1 | skip

and then put the last branch right below

[lzy0505]

I couldn't make it work.

[markusdemedeiros]

Done!

[lzy0505]

@markusdemedeiros Thank you so much for the review! I've passed over your comments. Feel free to make a final pass if you think some proofs should be further improved.

[markusdemedeiros]

Looks pretty good!