editing of equalities documentation

README.md

@@ -137,8 +137,9 @@ Getting along with Iris in Coq:
 
 * Iris proof patterns and conventions are documented in the
   [proof guide](docs/proof_guide.md).
-* Various notions of equality in Iris and their Coq interface are described in the [equality
-  docs](docs/equalities.md).
+* Various notions of equality and logical entailment in Iris and their Coq
+  interface are described in the
+  [equality docs](docs/equalities_and_entailments.md).
 * The Iris tactics are described in the
   [the Iris Proof Mode (IPM) / MoSeL documentation](docs/proof_mode.md) as well as the
   [HeapLang documentation](docs/heap_lang.md).

docs/equalities.md → docs/equalities_and_entailments.md

@@ -6,17 +6,20 @@ This document summarizes these relations and the subtle distinctions among them.
 This is not a general introduction to Iris: instead, we discuss the different
 Iris equalities and the interface to their Coq implementation. In particular, we
 discuss:
-- Equality from Iris metatheory vs Coq equality and setoid equivalence;
-- N-equivalence on OFEs;
-- Iris internal equality;
-- Iris entailment and bi-entailment.
+- Equality ("=") in the *on-paper* Iris metatheory
+- Coq equality (`=`) and setoid equivalence (`≡`);
+- N-equivalence on OFEs (`≡{n}≡`);
+- Iris internal equality (`≡` in `bi_scope`);
+- Iris entailment and bi-entailment (`⊢`, `⊣⊢`).
+
+We use `code font` for Coq notation and "quotes" for paper notation.
 
 ## Leibniz equality and setoids
 
 First off, in the metalogic (Coq) we have both the usual propositional (or
 Leibniz) equality `=`, and setoid equality `equiv` / `≡` (defined in `stdpp`).
-Notations for metalogic connectives like `≡` are declared in Coq scope
-`stdpp_scope`, which is "open" by default.
+Both of these are metalogic connectives from the perspective of Iris, and as
+such are declared in Coq scope `stdpp_scope`.
 
 Setoid equality for a type `A` is defined by the instance of `Equiv A`; this
 allows defining quotient setoids. To deal with setoids, we use Coq's
@@ -24,9 +27,11 @@ allows defining quotient setoids. To deal with setoids, we use Coq's
 rewriting](https://coq.inria.fr/refman/addendum/generalized-rewriting.html)
 facilities.
 
-Setoid equality can coincide with Leibniz equality:
-- `equivL` defines a setoid equality coinciding with Leibniz equality.
-- Some types enjoy `LeibnizEquiv`, which makes `equiv` be equivalent to `eq`.
+Setoid equality can coincide with Leibniz equality, which is reflected by the
+`LeibnizEquiv` typeclass. We say that types with this property are "Leibniz
+types". `equivL` provides a convenient way to define a setoid with Leibniz
+equality. The tactics `fold_leibniz` and `unfold_leibniz` can be used to
+automatically turn all equalities of Leibniz types into `≡` or `=`.
 
 Given setoids `A` and `B` and a function `f : A → B`, an instance `Proper ((≡)
 ==> (≡)) f` declares that `f` respects setoid equality, as usual in Coq. Such
@@ -34,31 +39,38 @@ instances enable rewriting with setoid equalities.
 
 Here, stdpp adds the following facilities:
 - `solve_proper` for automating proofs of `Proper` instances.
-- `f_equiv` generalizes `f_equal` to other relations; it will for instance turn
-  goal `R (f a) (f b)` into `R a b` given an appropriate `Proper` instance
-  (here, `Proper (R ==> R) f`).
+- `f_equiv` generalizes `f_equal` to setoids (and indeed arbitrary relations
+  registered with Coq's generalized rewriting). It will for instance turn the
+  goal `f a ≡ f b` into `a ≡ b` given an appropriate `Proper` instance (here,
+  `Proper ((≡) ==> (≡)) f`).
 
 ## Equivalences on OFEs
 
 On paper, OFEs involve two relations, equality "=" and distance "=_n". In Coq,
 equality "=" is formalized as setoid equality, written `≡` or `equiv`, as before;
 distance "=_n" is formalized as relation `dist n`, also written `≡{n}≡`.
-Tactics `solve_proper` and `f_equiv` also support distance.
+Tactics `solve_proper` and `f_equiv` also support distance. There is no
+correspondence to Coq's `=` on paper.
 
 Some OFE constructors choose interesting equalities.
 - `discreteO` constructs discrete OFEs (where distance coincides with setoid equality).
 - `leibnizO` constructs discrete OFEs (like `discreteO`) but using `equivL`, so
-  that both distance and setoid equality coincide with Leibniz equality.
+  that both distance and setoid equality coincide with Leibniz equality. This
+  should only be used for types that do not have a setoid equality registered.
 
 Given OFEs `A` and `B`, non-expansive functions from `A` to `B` are functions
-`f : A → B` with a proof of `NonExpansive f` (that is, `(∀ n, Proper (dist n
-==> dist n) f)`). The two can be packaged together via `A -n> B`.
+`f : A → B` with a proof of `NonExpansive f` (which is notation for `∀ n, Proper
+(dist n ==> dist n) f`).
+
+The type `A -n> B` packages a function with a non-expansiveness proof. This is
+useful because `A -n> B` is itself an OFE, but should be avoided whenever
+possible as it requires the caller to specifically package up function and proof
+(which works particularly badly for lambda expressions).
 
-Non-expansive functions from Leibniz OFEs can be given type `A -d> B` instead of
-`leibnizO A -n> B`; this spares the need for bundled `NonExpansive` instances.
-Moreover, `discreteO A -n> B` is isomorphic to `f : A -d> B` plus an instance
-for `∀ n, Proper ((≡) ==> (≡{ n }≡)) f`. However, in the second case the
-`Proper` instance can be omitted for proof convenience unless actively used.
+When an OFE structure on a function type is required but the domain is discrete,
+one can use the type `A -d> B`.  This has the advantage of not bundling any
+proofs, i.e., this is notation for a plain Coq function type. See the
+`discrete_fun` documentation in `iris.algebra.ofe` for further details.
 
 In both OFE function spaces (`A -n> B` and `A -d> B`), setoid equality is
 defined to be pointwise equality, so that functional extensionality holds for `≡`.
@@ -67,26 +79,35 @@ defined to be pointwise equality, so that functional extensionality holds for `
 
 Next, we introduce notions internal to the Iris logic. Such notions often
 overload symbols used for external notions; however, those overloaded notations
-are declared in scope `bi_scope`; when writing `(P)%I`, notations in `P` are
-resolved in `bi_scope` in preference over `stdpp_scope`.
-We also use `bi_scope` for the arguments of all variants of Iris entailments.
+are declared in scope `bi_scope`. When writing `(P)%I`, notations in `P` are
+resolved in `bi_scope`; this is done implicitly for the arguments of all
+variants of Iris entailments.
 
-The Iris logic has an internal concept of equality. If `a` and `b` are Iris
+The Iris logic has an internal concept of equality: if `a` and `b` are Iris
 terms of type `A`, then their internal equality is written (on paper) "a =_A b";
-in Coq, that's written `a ≡ b` (notation for `sbi_internal_eq` in scope `bi_scope`).
-
-As shown in the Iris appendix, an internal equality `a ≡ b` is interpreted using
-OFE distance. Many types have `_equivI` lemmas characterizing internal
-equality on them. For instance, if `f, g : A -d> B`, lemma
-`discrete_fun_equivI` shows that `f ≡ g` is equivalent to `∀ x, f x ≡ g x`.
-Typically, each `_equivI` lemma for type `T` lifts to internal equality on
-`T` properties of the distance on `T`.
+in Coq, that's written `(a ≡ b)%I` (notation for `bi_internal_eq` in scope
+`bi_scope`). The type annotation on paper only exist for the purpose of being
+fully explicit; it can be omitted as is common for other notions of equality and
+it is inferred in Coq.
+
+As shown in the Iris appendix, an internal equality `(a ≡ b)%I` is interpreted using
+OFE distance at the current step-index. Many types have `_equivI` lemmas
+characterizing internal equality on them. For instance, if `f, g : A -d> B`,
+lemma `discrete_fun_equivI` shows that `(f ≡ g)%I` is equivalent to
+`(∀ x, f x ≡ g x)%I`.
+
+An alternative to internal equality is to embed Coq equality into the Iris logic
+using `⌜ _ ⌝%I`.  For discrete types, `(a ≡ b)%I` is equivalent to `⌜a ≡ b⌝%I`,
+and the latter can be moved into the Coq context, making proofs more convenient.
+For types with Leibniz equality, we can even equivalently write `⌜a = b⌝%I`, so
+no `Proper` is needed for rewriting.  Note that there is no on-paper equivalent
+to using these embedded Coq equalities for types that are not discrete/Leibniz.
 
 ## Relations among Iris propositions
 
-In this section, we discuss relations among internal propositions.
+In this section, we discuss relations among internal propositions, and in particular equality/equivalence of propositions themselves.
 Even though some of these notes generalize to all internal logics (other
-`sbi`s), we focus on Iris propositions (`iProp Σ`), to discuss both their proof
+`bi`s), we focus on Iris propositions (`iProp`), to discuss both their proof
 theory and their model.
 As Iris propositions form a separation logic, we assume some familiarity with
 separation logics, connectives such as `-∗`, `∗`, `emp` and `→`, and the idea
@@ -94,58 +115,37 @@ that propositions in separation logics are interpreted with predicates over
 resources (see for instance Sec. 2.1 of the MoSEL paper).
 
 In the metalogic, Iris defines the entailment relation between uniform
-predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P` implies
-`Q` on _every_ resource (for details see Iris appendix [Sec. 6]).
-Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`, but
-equivalent, as `P ⊢ Q` is equivalent to `emp ⊢ P -∗ Q` (per Iris lemmas
-`entails_wand` and `wand_entails`).
-Notation `P ⊢ Q` is declared in `stdpp_scope`, but takes arguments in
-`bi_scope`, so that we can write conveniently `P ⊢ Q -∗ R` in `stdpp_scope`.
-For additional convenience, `P ⊢ Q` can also be written `P -∗ Q` in
-`stdpp_scope`, so that we can write `P -∗ Q -∗ R` instead of `P ⊢ Q -∗ R` or of
-the equivalent `emp ⊢ P -∗ Q -∗ R`.
-Using entailment, Iris defines an implicit coercion `bi_emp_valid`, mapping any
-Iris propositions `P` into the Coq propositions `emp ⊢ P`.
+predicates: intuitively, `P` entails `Q` (written `P ⊢ Q`) means that `P`
+implies `Q` on _every_ resource (for details see Iris appendix [Sec. 6]).
+Entailment `P ⊢ Q` is distinct from the magic wand, `(P -∗ Q)%I`: the former is
+a Coq-level statement of type `Prop`, the latter an Iris-level statement of type
+`iProp`.  However, the two are closely related: `P ⊢ Q` is equivalent to `emp ⊢
+P -∗ Q` (per Iris lemmas `entails_wand` and `wand_entails`).  Iris also defines
+a "unary" form of entailment, `⊢ P`, which is short for `emp ⊢ P`.
+We can also use bi-entailment `P ⊣⊢ Q` to express that both `P ⊢ Q` and `Q ⊢ P` gold.
 
 On paper, uniform predicates are defined by quotienting by an equivalence
-relation ([Iris appendix, Sec. 3.3]); that relation is used in Coq as setoid
-equivalence. That relation is also equivalent to bi-entailment (or entailment in
-both directions), per lemma `equiv_spec`:
+relation ([Iris appendix, Sec. 3.3]); in Coq, that relation is chosen as the
+setoid equivalent for the type of Iris propositions.
+This equivalence is actually equivalent to bi-entailment, per lemma `equiv_spec`:
 ```coq
 Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 ```
+Relying on this equivalence, bi-entailment `P ⊣⊢ Q` is defined as notation for `≡`.
 
-Hence, setoid equality `≡` on propositions is also written `⊣⊢`. For instance,
-our earlier lemma `discrete_fun_equivI` is stated using `⊣⊢`:
-
-```coq
-Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) :
-  f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
-```
+## Internal equality of Iris propositions
 
-Inside the logic, we can use internal equality `≡` (in `bi_scope`), which
-translates to distance as usual. Here is a pitfall: internal equality `≡` is in
-general strictly stronger than `∗-∗`, because `Q1 ≡ Q2` means that `Q1` and `Q2`
-are equivalent _independently of the available resources_.
-- When proving `P -∗ Q1 ∗-∗ Q2`, we can use `P` to show that `Q1` and `Q2` are
-  equivalent.
-- Instead, to prove `P -∗ Q1 ≡ Q2`, we cannot use `P` unless it's a plain
-  proposition (so, one that holds on the empty resource). Crucially, pure
-  propositions `⌜ φ ⌝` are plain.
-
-We can explain internal equality using the Iris plainly modality:
+Inside the logic, we can use internal equality `(≡)%I` on any type, including
+propositions themselves.  However, there is a pitfall here: internal equality
+`≡` is in general strictly stronger than `∗-∗` (the bidirectional version of the
+magic wand), because `Q1 ≡ Q2` means that `Q1` and `Q2` are equivalent
+_independently of the available resources_.  The two notions of internal
+equivalence and equality of propositions are related by the following law of
+propositional extensionality:
 ```coq
 Lemma prop_ext P Q : P ≡ Q ⊣⊢ ■ (P ∗-∗ Q).
 ```
-Looking at the Iris semantics for the plainly modality, to prove internal equality
-`P ≡ Q`, we must prove that `P` and `Q` are equivalent _without any resources
-available_.
-
-Last, metalevel propositions `φ : Prop` can be embedded as pure Iris
-propositions `⌜ φ ⌝`, and this allows embedding equalities from the metalogic.
-For instance, `⌜ a1 = a2 ⌝` can be useful for making some proofs more
-convenient, as Leibniz equality is the strongest equivalence available, is
-respected by all Coq functions, and can be used for rewriting in the absence of
-`Proper` instances. On the other hand, on-paper Iris does not allow writing
-`⌜ a1 = a2 ⌝`, only `⌜ a1 ≡ a2 ⌝`, unless setoid equality and Leibniz equality
-coincide.
+This uses the plainly modality `■` to reflect that equality corresponds to
+equivalence without any resources available: `■ R` says that `R` holds
+independent of any resources that we might own (but still taking into account
+the current step-index).