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 ofProper
instances.f_equiv
generalizesf_equal
to other relations; it will for instance turn goalR (f a) (f b)
intoR a b
given an appropriateProper
instance (here,Proper (R ==> R) f
).equivL
defines a setoid equality coinciding with Leibniz equality.
On paper, OFEs involve two relations, 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 usingequivL
, 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 ≡.
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
.
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 useP
to show thatQ1
andQ2
are equivalent. - Instead, to prove
P -∗ Q1 ≡ Q2
, usually we cannot useP
.
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.