mono_nat algebra: add dfrac support and notation

This implements the mono_nat algebra part of #412.

mentioned in merge request !761 (merged)

added 3 commits

• 400e58dd - mono_nat algebra: add dfrac support and notation
• da63a90f - swap direction of mono_nat_lb_op
• eed5c0a8 - changelog

Compare with previous version

resolved all threads

added 44 commits

• eed5c0a8...f85824ee - 40 commits from branch master
• 1b6addea - mono_nat algebra: add dfrac support and notation
• 465c3e3d - swap direction of mono_nat_lb_op
• c833e59e - remove _frac_ lemmas, the corresponding _dfrac_ lemmas are sufficient
• 05dca5b4 - changelog

Compare with previous version

resolved all threads

added 2 commits

• 73f66890 - remove _frac_ lemmas, the corresponding _dfrac_ lemmas are sufficient
• 81549fc6 - changelog

Compare with previous version

resolved all threads

added 8 commits

• 81549fc6...347533aa - 4 commits from branch master
• c7cda88a - mono_nat algebra: add dfrac support and notation
• 1503fb75 - swap direction of mono_nat_lb_op
• 41e81796 - remove _frac_ lemmas, the corresponding _dfrac_ lemmas are sufficient
• 230ff113 - changelog

Compare with previous version

enabled an automatic merge when the pipeline for 230ff113 succeeds

@iris-users this affects users of the mono_nat algebra (the base_logic library remains unchanged):

• Equip mono_nat algebra with support for dfrac, make API more consistent, and add notation for algebra elements. See iris/algebra/lib/mono_nat.v for details. This affects some existing terms and lemmas:
  • mono_nat_auth now takes a dfrac, but the recommendation is to port to the notation.
  • mono_nat_lb_op: direction of equality is swapped.
  • mono_nat_auth_frac_op, mono_nat_auth_frac_op_valid, mono_nat_auth_frac_valid, mono_nat_both_frac_valid: use dfrac variant instead.

merged

mentioned in commit ec624937