From 3fa48930804d5caa3e8e1c29c2102ecaf11aac35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 Jul 2023 13:54:50 +0200
Subject: [PATCH] rename `singleton_mono` to `singleton_included_mono`

---
 CHANGELOG.md        | 1 +
 docs/style_guide.md | 5 +----
 iris/algebra/gmap.v | 2 +-
 3 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4b290acc6..f04394dfd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,6 +47,7 @@ Coq 8.13 is no longer supported.
 * Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` /
   `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
   proofs. (by Ike Mulder)
+* Rename `singleton_mono` to `singleton_included_mono`.
 
 **Changes in `bi`:**
 
diff --git a/docs/style_guide.md b/docs/style_guide.md
index 66a069dc8..c09039634 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -210,10 +210,6 @@ theories/base_logic/lib is for constructions in the base logic (using own)
 * `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
 * Injectivity theorems are instances of `Inj` and then are used with `inj`
 * Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant).
-* Entailments at the top level are typically written `P -* Q`, which is notation
-  for `P ⊢ Q`. If you have a theorem which has no premises you have to write ⊢ P
-  explicitly (for example, it is common to have `⊢ |==> ∃ γ, …` for an allocation
-  theorem)
 * Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
   these since the name doesn't convey how `foo'` is related to `foo`.
 * Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work.
@@ -224,6 +220,7 @@ theories/base_logic/lib is for constructions in the base logic (using own)
     M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
     M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
     ```
+* Monotonicity lemmas where the relation can be ambiguous are called `<f>_<relation>_mono`, e.g. `Some_included_mono`.
 
 ### Naming algebra libraries
 
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 58ce801bb..ead5b1e59 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -369,7 +369,7 @@ Qed.
 Lemma singleton_included_total `{!CmraTotal A}  i x y :
   {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≼ y.
 Proof. rewrite singleton_included Some_included_total. done. Qed.
-Lemma singleton_mono i x y :
+Lemma singleton_included_mono i x y :
   x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
 Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
 
-- 
GitLab