Separation logic in Rocq

In this chapter, we introduce the basic separation logic facilities of Eris. By virtue of building on Iris, Eris inherits a lot of technical machinery and many concepts are directly transferable. The core Iris separation logic framework is parameterized by the type of ghost state that is needed to carry out a proof. This manifest in the Rocq-level type of propositions in Iris, iProp Σ, that is indexed by a Σ of type gFunctors. To make our proofs generic, we typically abstract over any such Σ and use type classes to ensure that the necessary constructions are present in Σ. For this tutorial, however, we will not be concerned with these matters–we will just assume some Σ is in scope.

The theorems we can prove in Iris have the form P ⊢ Q (type \vdash), saying that the separation logic assertion P implies the assertion Q. Iris is built on top of Rocq and has a custom interface called the Iris Proof Mode (IPM). IPM has its own versions of many Rocq tactics, which maintain a new context, called the spatial context, in addition to the usual Rocq-level context. goal. The regular Rocq tactics can still be used when we work within the non-spatial context, but, in general, we shall use the new tactics that work natively with the spatial context. These new tactics start with 'i', and since many of them simply 'lift' the regular tactics to also work with the spatial context, they borrow the regular names but with the 'i' prefixed. For instance, the tactic intros H becomes iIntros "H", and instead of apply H we use iApply "H". For technical reasons, identifiers for hypotheses in the spatial context are strings Let us start by provin prove the statement ⊢ P -∗ P, for all P.

We start by introducing the assumption P.

This adds P to the spatial context with the identifier "H" and we are left with the goal P. In a typical Rocq proof, we would continue by either exact or apply. In Iris, we use either iExact or iApply.

Separation Logic Connectives

The core connective in separation logic is the `separating conjunction', written P ∗ Q (type \sep or \star), for propositions P and Q. Separating conjunction differs from regular conjunction, particularly in its introduction rule: P1 ⊢ Q1 P2 ⊢ Q2

---

P1 ∗ P2 ⊢ Q1 ∗ Q2 That is, if we want to prove Q1 ∗ Q2, we must decide which of our owned resources we use to prove Q1 and which we use to prove Q2. To see this in action, let us prove that separating conjunction is commutative.

To eliminate a separating conjunction we use the tactic iDestruct with the usual destruction pattern.

Alternatively, we can introduce and destruct resources simultaneously.

Unlike ∧, the separating conjunction ∗ is not idempotent. That is, there are Iris propositions for which P ⊢ P ∗ P is not the case. Because of this, it is generally not possible to use iSplit to introduce ∗. The iSplit tactic would duplicate the spatial context and is therefore not available when the context is non-empty.

Instead, Iris introduces the tactics iSplitL and iSplitR that allow you to specify how you want to separate your resources to prove each subgoal. The hypotheses mentioned by iSplitL are given to the left subgoal, and the remaining to the right. Conversely for iSplitR.

Separating conjunction has an analogue to implication which, instead of introducing the antecedent to the assumptions with conjunction, introduces it with separating conjunction. This connective is written as P -∗ Q and pronounced `magic wand' or simply `wand'.

Just as with Rocq tactics, Iris supports complex nested introduction and destruction patterns. For example, you can use a pattern like (H1 & .. & H2 & H3) as a shorthand for [H1 .. [H2 H3] ..]. Exercise: use an introduction pattern of with parentheses to prove associativity of ∗. Note that ∗ is right-associative, so P ∗ Q ∗ R is parsed as P ∗ (Q ∗ R).

Manually splitting separating conjunctions quickly becomes tedious. To alleviate this, the iFrame tactic automatically pairs up hypotheses with conjuncts in the goal separation sequence.

For assertions with multiple assumptions, i.e. nested magic wands, it is often necessary specify which part of the context should go where. This is done using iApply ("H" with "[H1 H2 H3] [H4 H5]"). Each set of square brackets specifies the part of the context going to that argument. Let's try it out.

When applying "H", we get the subgoals P and Q. To specify that we want to use "HP" to prove the first subgoal, and "HQ" the second, we add "HP" in the first square bracket, and "HQ" in the second.

Here is another proof strategy based on forward-reasoning instead.

Instead of applying "H", we can also just "feed the arguments" to the implication. This allows us to deducing more assertions from our assumptions instead of working backwards from the goal.

Finally, we can use the specialized implication, now exactly matching our goal.

Hypotheses that fit arguments exactly can be supplied directly without a square bracket to avoid trivial subgoals, as in the above. Try this in the following exercise.

As usual, from a contradiction, any assertion P follows.

In particular, if P is contradictory, then Q follows from P.

Disjunctions ∨ are treated just like disjunctions in Rocq. The introduction pattern [ _ | _ ] allows us to eliminate a disjunction, while the tactics iLeft and iRight let us introduce them. Prove that disjunction commutes.

We can even prove the usual elimination rule for or-elimination written with separation. This version is, however, not very useful, as it does not allow the two cases to share resources.

Separating conjunction distributes over disjunction (for the same reason as ordinary conjunction).

Iris propositions can be existentialy and universally quantified over any Rocq type. Existential quantifiers are proved using the iExists tactic, using the same syntax as for exists. Elimination of existentials is done through the pattern "[%x Hx]" or as part of a "(_ & .. & _)" with a % in front of the existential variable. (type \exists).

Likewise, universal quantification works almost as in Rocq. To introduce a universal qunatifier, you can either use iIntros (x y z) or iIntros "%x %y %z". These patterns are interchangeable. To specify the parameters of hypotheses, we write iApply ("H" $! x y z). (type \forall)

More useful introduction and elmination patterns can be found in the Iris documentation at https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md?ref_type=heads#introduction-patterns-ipat