Bupdalt

[ahuoguo]

The motivation for this alternative definition can be found here: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/211 https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/186

Questions and TODOs:

• Should this file be place in src/Iris/BI/? I was in iris/base_logic/ in the iris-rocq repo?
• For own_updateP, the variable own_updateP_plainly disappears after := by. So I have to state it as a parameter. nvm
• #iris-lean > pure propositions @ 💬

[markusdemedeiros]

Good stuff!

Some notes:

• Use Mathlib style docstrings instead of -- ...
• For definitions, use the syntax typeclasses: BIBase instead of BI and Plainly instead of BIPlainly
• I moved around the code. Since this amounts to a helper function for constructing BUpd instances, I moved it to the ProofMode folder and split it into two files (the generic construction, and the compatibility with the UPred instance)
• Opening frequently namespaces in sections
• Removing unused names
• General cleanup of the proofs. I think it's nice that you used the proofmode here, I wouldn't have done the same but it's a great test case.
  • The AI proofs were really obvious. They seem to generate lots of "have" statements that are only used once, these should typically be inlined. Doing so for some proofs (eg. own_updateP) revealed plenty of unnecessary have statements and calc statements that could be combined. In the future, it is good practice to try doing this yourself.

Look over my changes, and let me know when you think it's good to go.

[ahuoguo]

I moved around the code. Since this amounts to a helper function for constructing BUpd instances, I moved it to the ProofMode folder and split it into two files (the generic construction, and the compatibility with the UPred instance)

Why does the generic construction of BupdAlt goes into proof mode? Isn't this a syntactic construct on top of BI?

[markusdemedeiros]

I was running into some cyclic dependency problems because you used Iris tactics instead of doing a plain Lean proof. There's already a dependency on all of BI in some of the tactics, so if I added the BUpdPlain to the top-level import of BI it creates a cycle. I figured this would be a one-off problem, but now that you brought it up again, I looked closer through Iris-Rocq and realized many files will run into this problem.

I pushed a change to have a separate Lib folder in BI that is not included in the top-level import. This avoids the cycle, and in fact, I think Iris-Rocq ends up doing the same thing too. I always wondered why some things were in Lib folders!

[ahuoguo]

Thanks for looking into this! LGTM to merge now.

[markusdemedeiros]

Another one in the books, great work!