Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade
Last active July 13, 2020 15:52
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Blaisorblade/855b5c99b3827c306433c6da4cb689c5 to your computer and use it in GitHub Desktop.
Save Blaisorblade/855b5c99b3827c306433c6da4cb689c5 to your computer and use it in GitHub Desktop.
Docs on Iris equalities; superseded by https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/300

Equalities in Iris

Using Iris involves dealing with a few subtly different equivalence and equality relations, especially among propositions. This document summarizes these relations and the subtle distinctions among them. It does not replace the Iris appendix, nor "Iris from the grounds up", but it expands on how Iris is mapped into Coq, tho we focus on issues affecting equalities.

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.

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 generalized rewriting facilities.

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 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).
  • equivL defines a setoid equality coinciding with Leibniz equality.

Equivalences on OFEs

On paper, OFEs involve two relations, equality $=$ and distance $=_n$. In Coq, equality is implemented via setoid equality , and distance via ≡{n}≡; solve_proper and f_equiv also support distance.

Some OFE constructors choose interesting equalities.

  • discreteO constructs discrete OFEs (where distance coincides with setoid equality).
  • leibnizO constructs discrete OFEs using equivL, where all equalities coincide with Leibniz equality.

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.

Non-expansive functions from Leibniz OFEs can be given type A -d> B instead of leibnizO A -n> B; this spares the need for NonExpansive instances.

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 ≡.

Inside the Iris logic

Next, we introduce notions internal to the Iris logic. Such notions often overload symbols used for external notions; however, those overloads are declared in scope bi_scope; when writing (e)%I, notations in e are resolved in bi_scope in preference over stdpp_scope. Arguments of -∗ are automatically parsed in bi_scope as well. TODO: explain -∗ for wand vs entailment.

The Iris logic has an internal concept of equality. If a and b are Iris terms of type τ, then their internal equality is written (on paper) a =_τ b; in Coq, that's written sbi_internal_eq a b or a ≡ b (in scope bi_scope).

As shown in the Iris appendix, an internal equality a ≡ b is interpreted using distance. To unfold the definition of distance on a certain type, one must use the appropriate equivI lemma. For instance, if f, g : A -d> B, lemma discrete_fun_equivI shows that f ≡ g is equivalent to ∀ x, f x ≡ g x.

Relations among Iris propositions

Here, we discuss relations among Iris propositions. As explained by the appendix, Iris propositions (iProp Σ) are uniform predicates (uPred M), so we discuss the latter. As Iris propositions form a separation logic, we assume some familiarity with separation logics, connectives such as -∗, , emp and , and the idea that propositions in separation logics are interpreted with predicates over resources (see for instance Sec. 2.1 of 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). Using entailment, Iris defines an implicit coercion bi_emp_valid, mapping any Iris propositions P into the Coq propositions emp ⊢ P.

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.

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:

Lemma equiv_spec P Q : P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P).

Hence, setoid equality on propositions is also written ⊣⊢. For instance, our earlier lemma discrete_fun_equivI is stated using ⊣⊢:

Lemma discrete_fun_equivI {A} {B : A → ofeT} (f g : discrete_fun B) :
  f ≡ g ⊣⊢ ∀ x, f x ≡ g x.

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, usually we cannot use P.

We can explain internal equality using the Iris plainly modality:

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 P can be embedded using ⌜ P ⌝, and this allows embedding equalities from the metalogic. For instance, ⌜ a1 = a2 ⌝ can be useful, 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment