Skip to content

Add derived ≼ connective on the BI level.

Ike Mulder requested to merge snyke7/iris:ike/internal_included into master

For !930 it was useful to have the ≼ connective on the BI level.

I originally defined it for uPreds, but since it has seen usage for non-uPred bis, I have generalized it.
Current location is at bi/lib/cmra.v.

This MR is turning out to be a bit larger than I expected, after I started moving all useful lemmas from !930 on ≼ here. It currently contains the following changes:

  • Defining the ≼ connective, proofmode support for it, and some useful lemmas
  • Moving some lemmas on excl and csum that were stated for uPreds, but provable for general bis with ≡.
  • Add two additional hints for ≼ on the Prop level, which makes eauto more useful.
Edited by Ike Mulder

Merge request reports