feat: port bi/Algebra

[markusdemedeiros]

Description

Finishes Algebra.v.

There are some lightweight tactics for dealing with sbi simplifications. sbi_unfold.v does this in Rocq, I'm not sure I understand what they're doing enough to determine if we should replicate them or ignore them. The tactics here seem to work alright. Polling you guys for your thoughts @Kaptch @MackieLoeffel. By your reading, is it doing anything that a simp set could not?

Checklist

• My code follows the mathlib naming and code style conventions
• 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.

[MackieLoeffel]

Instead of the hard coded simp only list, I would use a custom simp attribute defined with register_simp_attr. This makes it easier to extend this list.
See wp_expr_simp for an example.
(Not sure if this approach also works for sbi_fold. The p parameter might prevent one from using a custom simp attribute there.)

[markusdemedeiros]

Yes, I think I might roll sbi_unfold into this PR and just do it properly. Finally an occasion to learn about simpprocs.

[Kaptch]

Would it be okay to add those to simpset as well instead of adding a simp attribute?

[markusdemedeiros]

Probably a good idea. I'm going to redo the automation around sbi this morning and will re-request after.

[markusdemedeiros]

OK, I changed this PR to use a simp set for the sbi unfolding. It doesn't fully replicate Rocq's sbi_unfold.v--I think we need a simpproc to handle all the cases in this approach, or we can do something else. I don't quite know if sbi_unfold is meant to be useful in general or a tactic for mostly Iris use only, at the moment it helps us simplify our proofs, but it would have to be made more robust if Iris clients are expected to use it.