2.3. Basic Separation Logic🔗

The core connective in separation logic is the separating conjunction, written P ∗ Q, for propositions P and Q. Separating conjunction differs from regular conjunction, particularly in its introduction rule:

       P₁ ⊢ Q₁     P₂ ⊢ Q₂
       ─────────────────────
         P₁ ∗ P₂ ⊢ Q₁ ∗ Q₂

That is, if we want to prove Q₁ ∗ Q₂, we must decide which of our owned resources we use to prove Q₁ and which we use to prove Q₂. To see this in action, let us prove that separating conjunction is commutative.

To eliminate a separating conjunction we use the cases pattern ⟨HP, HQ⟩ in iintro — analogous to Lean's anonymous-constructor notation.

Unlike ∧, ∗ is not idempotent. Specifically, there are Iris propositions for which ¬(P ⊢ P ∗ P). 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. These allow you to specify how you want to separate your resources to prove each subgoal. The hypotheses listed in brackets — space-separated, e.g. [HP HQ] — are passed to the left subgoal (for isplitl), 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". Separation is so widely used that P -∗ Q is treated specially; instead of writing P ⊢ Q, we can write P -∗ Q, with the ⊢ being implicit. That is, ⊢ P -∗ Q is notationally equivalent to P -∗ Q.

Writing a wand instead of entailment makes currying more natural. Here is the Iris version of modus ponens. It is provable using only iintro and iapply.

Just as with Lean tactics, Iris allows nesting of introduction patterns. In fact, like Lean, Iris supports patterns of the form ⟨H1, H2, H3⟩ as a shorthand for nested ⟨H1, ⟨H2, H3⟩⟩.

Note that ∗ is right-associative, so P ∗ Q ∗ R is parsed as P ∗ (Q ∗ R).

Manually splitting a separation can become tedious. To alleviate this, we can use the iframe tactic. This tactic pairs up hypotheses with pieces of a separation sequence.

Bi-entailment of Iris propositions is denoted P ⊣⊢ Q. It is an equivalence relation, and most connectives preserve it. Bi-entailment is defined as the conjunction of P -∗ Q and Q -∗ P, so it can be decomposed using the isplit tactic (which is permitted here because the spatial context is empty at the point of splitting).

For hypotheses with multiple curried wands, we use the proof-mode term syntax of iapply: the form iapply H $$ pat₁ … patₙ supplies arguments for the wand premises of H.

Hypotheses that fit arguments exactly can be supplied directly without generating a trivial subgoal.

Disjunctions ∨ are treated just like disjunctions in Lean. The introduction pattern (HP | HQ) allows us to eliminate a disjunction, while the tactics ileft and iright let us introduce them.

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 has existential and universal quantifiers over any Lean type. Existential quantifiers are proved using the iexists tactic. Elimination of existentials uses the pattern %x (with a % in front of the bound variable) to move it to the pure (Lean) context.

Likewise, forall quantification works almost as in Lean. To introduce a universally quantified variable in the Iris context, you use the intro pattern %x. To specialise a hypothesis at a concrete value x, you write H $$ %x.