Revise the theory of the monotone CMRA

In reference to #414 (closed): I just used monotone, and I have some relevant suggestions with a concrete implementation.

I've also simplifies some proofs using set_solver.

• Type inference sometimes prefers principal_injN over principal_inj_instance (as shown by the included test), which hinders some proofs — that's easily fixed, but principal_injN might warrant more revisions (see below).
• Because of CmraDiscrete (mraR R), maybe the theory about dist (A := mra R) should be removed.
  • This MR removes almost all of this theory.
• I used the mra_over_ofe theory over a leibnizO OFE, but that theory holds for an arbitrary relation S over A, as long as R "respects S" in the right way — tying it to ofes seems potentially artificial.
  • Here I make such instances opt-in via #[export]; by default, I only export the theory relevant to S := (=), which is only principal_inj.

marked this merge request as draft

changed the description

changed title from Draft: Monotone tweaks to Draft: Revise the theory of the monotone CMRA

added 5 commits

• fb53144d - Test problem with monotone cmra
• df553039 - Some proof tweaks
• e98b672f - Theory revisions
• 65049067 - Replace some proofs with set_solver
• 2112f9e1 - Make [mra_over_rel] an opt-in module

Compare with previous version

changed the description

changed the description

cc @amintimany .

marked this merge request as ready

added 3 commits

• cf1a8937 - Theory revisions
• 5e2d2fc1 - Replace some proofs with set_solver
• ce34fef3 - Make [mra_over_rel] an opt-in module

Compare with previous version

Thanks @Blaisorblade :-) These are all good suggestions. The code also looks good to me.

Thanks! Just some nits.

mentioned in issue #414 (closed)

Overall, it seems Ralf agrees with me the current dist theory can be taken out even more completely, and that should help the next revision.

added 34 commits

• ce34fef3...95f3a05f - 26 commits from branch iris:master
• 2ffdad74 - Test problem with monotone cmra
• 29c0b0ce - Some proof tweaks
• 1a528fbd - Theory revisions
• 2dd90962 - Replace some proofs with set_solver
• eae1b7ba - Make [mra_over_rel] an opt-in module
• 77bdb4c8 - Tweak `mra`.
• 5bc923f1 - Make `R` argument of `principle` implicit, it can be infered from the type of `mra R`.
• 5d4507f9 - Rename `monotone` into `mra`; move out of unstable.

Compare with previous version