Proof Rules

This page is the catalogue of separation-logic rules that C*‘s proof kernel makes available. Each entry gives the rule’s registered name — the name you pass to get_theorem_by_nameget_theorem_by_name, and the name that appears in the get_*get_* accessor of proof_kernel.hproof_kernel.h — together with the exact statement of the theorem as it exists in the kernel.

The vocabulary used below — hprophprop, ****, -*-*, &&&&, ||||, -->-->, empemp, purepure, factfact, |--|--, -|--|-, and the quantifiers existsexists and forallforall — is defined in Memory Model and Assertions. Two notational reminders are worth repeating here, because every statement below depends on them: |--|-- is entailment (hentailhentail, a boolbool), and -|--|- is HOL equality between assertions (-|--|- is == at type hprophprop), not a separate equivalence relation. The kernel proves heqheq, namely !hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)!hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2), which is what licenses using mutual entailment and equality interchangeably; because -|--|- really is equality, every -|--|- rule below can be used as a rewrite in either direction.

Everything else rests on four theorems about the memory-join relation. They are stated over the abstract signature join : model->model->model->booljoin : model->model->model->bool and is_unit : model->boolis_unit : model->bool, which the kernel instantiates to mem_joinmem_join and mem_emptymem_empty. The C* development does not postulate them: each one is a proveprove against the concrete memory model, discharged by case analysis on the three states of a mem_varmem_var cell. (The kernel source keeps a commented-out new_axiomnew_axiom version of all four, which is what the corresponding development would look like if the model were left abstract.)

The first law says every state has a unit it joins with; the second says units are absorbed; the third and fourth give the join relation commutativity and associativity.

As HOL statements:

unit_joinunit_join — proved. Every state joins with some unit.

!n:model. ?u:model. is_unit u /\ join n u n

!n:model. ?u:model. is_unit u /\ join n u n

unit_specunit_spec — proved. Joining a unit changes nothing.

!n:model m:model u:model. is_unit u ==> join n u m ==> n = m

!n:model m:model u:model. is_unit u ==> join n u m ==> n = m

join_commjoin_comm — proved. The join relation is symmetric in its two inputs.

!m1:model m2:model m:model. join m1 m2 m ==> join m2 m1 m

!m1:model m2:model m:model. join m1 m2 m ==> join m2 m1 m

join_assocjoin_assoc — proved. Rebracketing a three-way split is always possible.

!mx:model my:model mz:model mxy:model mxyz:model. join mx my mxy ==> join mxy mz mxyz ==> (?myz. join my mz myz /\ join mx myz mxyz)

!mx:model my:model mz:model mxy:model mxyz:model. join mx my mxy ==> join mxy mz mxyz ==> (?myz. join my mz myz /\ join mx myz mxyz)

|--|-- is a preorder on hprophprop, and antisymmetric up to -|--|-. These five rules are the backbone of every proof: hentail_transhentail_trans chains steps, and hentail_antisymhentail_antisym turns a pair of entailments into a rewritable equality.

hentail_reflhentail_refl — proved. Entailment is reflexive; this is what closes a goal whose two sides have become identical.

!hp. hp |-- hp

!hp. hp |-- hp

hentail_transhentail_trans — proved. Entailment is transitive; chaining is how a proof advances one step at a time.

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp2 |-- hp3) ==> (hp1 |-- hp3)

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp2 |-- hp3) ==> (hp1 |-- hp3)

hentail_antisymhentail_antisym — proved. Mutual entailment is equality of assertions.

!hp1 hp2. (hp1 |-- hp2) ==> (hp2 |-- hp1) ==> (hp1 -|- hp2)

!hp1 hp2. (hp1 |-- hp2) ==> (hp2 |-- hp1) ==> (hp1 -|- hp2)

hentail_sym_lefthentail_sym_left — proved. The converse direction: an equality of assertions can be weakened to an entailment, which is how a rewriting lemma is fed into an entailment goal.

!hp1 hp2. (hp1 -|- hp2) ==> (hp1 |-- hp2)

!hp1 hp2. (hp1 -|- hp2) ==> (hp1 |-- hp2)

heq_symheq_sym — proved. Assertion equality is symmetric, stated as an <=><=> so it can be used to reorient a goal.

!hp1 hp2. (hp1 -|- hp2) <=> (hp2 -|- hp1)

!hp1 hp2. (hp1 -|- hp2) <=> (hp2 -|- hp1)

**** is associative and commutative with empemp as unit — that is, (hprop, **,emp)(hprop, **,emp) is a commutative monoid. The rules below are the ones a proof reaches for when rearranging the spatial part of an assertion.

hsep_assochsep_assoc — proved. **** is associative.

!hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)

!hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)

hsep_commhsep_comm — proved. **** is commutative. Separating conjunction imposes no order on the two heap fragments it joins.

!hp1 hp2. hp1 ** hp2 -|- hp2 ** hp1

!hp1 hp2. hp1 ** hp2 -|- hp2 ** hp1

hsep_hemp_lefthsep_hemp_left — proved. empemp is a left unit.

!hp. emp ** hp -|- hp

!hp. emp ** hp -|- hp

hsep_hemp_righthsep_hemp_right — proved. empemp is a right unit.

!hp. hp ** emp -|- hp

!hp. hp ** emp -|- hp

hsep_comm_left_parthsep_comm_left_part — proved. Pull the middle conjunct of a right-nested chain to the front. This is the workhorse for moving one specific resource to the head of a long **** chain without unfolding the whole chain by hand.

!hp hp1 hp2. hp1 ** hp ** hp2 -|- hp ** hp1 ** hp2

!hp hp1 hp2. hp1 ** hp ** hp2 -|- hp ** hp1 ** hp2

hsep_achsep_ac — proved. The associativity-commutativity bundle: the three rewrites above packaged as one theorem, in the shape HOL’s rewriter expects for AC normalization of ****. The &&&& here is boolean conjunction (&&&& is overloaded, and the three components are boolbool), not handhand.

(hp1 ** hp2 -|- hp2 ** hp1) && ((hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)) && (hp1 ** (hp2 ** hp3) -|- hp2 ** (hp1 ** hp3))

(hp1 ** hp2 -|- hp2 ** hp1) && ((hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)) && (hp1 ** (hp2 ** hp3) -|- hp2 ** (hp1 ** hp3))

This is the theorem that normalization consumes: rewriting with hsep_achsep_ac reorders and rebrackets a **** chain into a canonical form, which is why proofs that manipulate long spatial conjunctions rarely need hsep_assochsep_assoc and hsep_commhsep_comm individually.

neutral_hsepneutral_hsep — proved. empemp is the neutral element of ****, in HOL’s sense of neutralneutral.

neutral(**) = emp

neutral(**) = emp

monoidal_hsepmonoidal_hsep — proved. **** is a monoidal operation, which is the precondition of HOL’s generic iterateiterate machinery. This theorem is what allows the iterated separating conjunction hitersephitersep to inherit the whole ITERATE_*ITERATE_* library (insert, union, difference, delete) for free.

monoidal(**)

monoidal(**)

Framing is the reason separation logic scales: a proof about a few heap cells stays valid when the rest of the heap is carried along untouched. In C* that principle is not a metatheorem about triples but an ordinary theorem about assertions.

hsep_cancel_lefthsep_cancel_left — proved. Strengthen one side of a **** while carrying an arbitrary frame hp3hp3 on the left.

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp3 ** hp1 |-- hp3 ** hp2)

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp3 ** hp1 |-- hp3 ** hp2)

hsep_cancel_righthsep_cancel_right — proved. The mirror image, framing on the right.

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 ** hp3 |-- hp2 ** hp3)

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 ** hp3 |-- hp2 ** hp3)

hsep_cancel_left_eqhsep_cancel_left_eq — proved. The equality-valued version: rewriting inside the right operand of a **** preserves the whole assertion.

!hp1 hp2 hp2'. (hp2 -|- hp2') ==> (hp1 ** hp2 -|- hp1 ** hp2')

!hp1 hp2 hp2'. (hp2 -|- hp2') ==> (hp1 ** hp2 -|- hp1 ** hp2')

hsep_monotonehsep_monotone — proved. **** is monotone in both arguments simultaneously; both cancellation rules are instances of it, taking one entailment to be reflexivity.

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')

The tactic-level counterparts of these rules, and the way a proof cancels matching resources on the two sides of a goal, are covered in Backward Proof for Separation Logic the forward-style frame_right_slruleframe_right_slrule used by local_applylocal_apply is hsep_cancel_righthsep_cancel_right in the same sense.

Two connectives are characterized by adjunctions rather than by introduction and elimination rules: the separating implication -*-* is right adjoint to ****, and the ordinary implication -->--> is right adjoint to &&&&. Both are stated as <=><=>, so each can be read in whichever direction the goal needs.

hwand_hsep_adjointhwand_hsep_adjoint — proved. The wand adjunction.

!hp1 hp2 hp3. (hp1 ** hp2 |-- hp3) <=> (hp1 |-- hp2 -* hp3)

!hp1 hp2 hp3. (hp1 ** hp2 |-- hp3) <=> (hp1 |-- hp2 -* hp3)

himpl_hand_adjointhimpl_hand_adjoint — proved. The implication adjunction.

!hp1 hp2 hp3. (hp1 && hp2 |-- hp3) <=> (hp1 |-- hp2 --> hp3)

!hp1 hp2 hp3. (hp1 && hp2 |-- hp3) <=> (hp1 |-- hp2 --> hp3)

In practice the wand’s definition — quantification over all extensions of the current state — is almost never unfolded. hwand_hsep_adjointhwand_hsep_adjoint is how -*-* is used: a goal hp1 |-- hp2 -* hp3hp1 |-- hp2 -* hp3 becomes the ****-goal hp1 ** hp2 |-- hp3hp1 ** hp2 |-- hp3, which the ordinary spatial machinery can attack, and conversely a hypothesis about a wand is consumed by turning it back into a separating conjunction.

The non-spatial connectives behave as in ordinary intuitionistic logic, lifted pointwise to hprophprop. What is worth attention is how truetrue and falsefalse interact with ****: fact(T)fact(T) is empemp and disappears, while fact(F)fact(F) absorbs everything next to it.

htrue_defhtrue_def — proved. truetrue at type hprophprop is pure(T)pure(T): satisfied by every state, including non-empty ones.

true -|- pure(T)

true -|- pure(T)

hfalse_defhfalse_def — proved. falsefalse is pure(F)pure(F), satisfied by no state.

false -|- pure(F)

false -|- pure(F)

htrue_introhtrue_intro — proved. Anything entails truetrue; this discards an entire assertion.

!hp. hp |-- true

!hp. hp |-- true

htrue_hemphtrue_hemp — proved. The trivial fact is the empty heap. Note the contrast with htrue_defhtrue_def: fact(T)fact(T) carries the additional claim that the heap is empty, whereas truetrue does not.

fact(T) -|- emp

fact(T) -|- emp

hfalse_elimhfalse_elim — proved. Ex falso at the assertion level.

!hp. false |-- hp

!hp. false |-- hp

hsep_hfalse_lefthsep_hfalse_left — proved. falsefalse annihilates a separating conjunction.

!hp. false ** hp |-- false

!hp. false ** hp |-- false

htrue_elim_lefthtrue_elim_left — proved. A trivial fact on the left of **** vanishes.

!hp. fact(T) ** hp -|- hp

!hp. fact(T) ** hp -|- hp

htrue_elim_righthtrue_elim_right — proved. Likewise on the right.

!hp. hp ** fact(T) -|- hp

!hp. hp ** fact(T) -|- hp

hfalse_absorb_lefthfalse_absorb_left — proved. A false fact absorbs whatever it is joined with.

!hp. fact(F) ** hp -|- fact(F)

!hp. fact(F) ** hp -|- fact(F)

hfalse_absorb_righthfalse_absorb_right — proved. Likewise on the right.

!hp. hp ** fact(F) -|- fact(F)

!hp. hp ** fact(F) -|- fact(F)

hand_introhand_intro — proved. To prove a conjunction, prove both conjuncts from the same assertion. Unlike ****, &&&& does not split the heap: both sides describe the same state.

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 |-- hp3) ==> (hp1 |-- hp2 && hp3)

!hp1 hp2 hp3. (hp1 |-- hp2) ==> (hp1 |-- hp3) ==> (hp1 |-- hp2 && hp3)

hand_elim1hand_elim1 — proved. Project out the left conjunct.

!hp1 hp2. (hp1 && hp2 |-- hp1)

!hp1 hp2. (hp1 && hp2 |-- hp1)

hand_elim2hand_elim2 — proved. Project out the right conjunct.

!hp1 hp2. (hp1 && hp2 |-- hp2)

!hp1 hp2. (hp1 && hp2 |-- hp2)

hand_assochand_assoc — proved. &&&& is associative.

!hp1 hp2 hp3. (hp1 && hp2) && hp3 -|- hp1 && (hp2 && hp3)

!hp1 hp2 hp3. (hp1 && hp2) && hp3 -|- hp1 && (hp2 && hp3)

hand_commhand_comm — proved. &&&& is commutative.

!hp1 hp2. hp1 && hp2 -|- hp2 && hp1

!hp1 hp2. hp1 && hp2 -|- hp2 && hp1

hand_monotonehand_monotone — proved. &&&& is monotone in both arguments.

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 && hp2 |-- hp1' && hp2')

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 && hp2 |-- hp1' && hp2')

hor_intro1hor_intro1 — proved. Choose the left disjunct.

!hp1 hp2. (hp1 |-- hp1 || hp2)

!hp1 hp2. (hp1 |-- hp1 || hp2)

hor_intro2hor_intro2 — proved. Choose the right disjunct.

!hp1 hp2. (hp2 |-- hp1 || hp2)

!hp1 hp2. (hp2 |-- hp1 || hp2)

hor_elimhor_elim — proved. Case analysis: to use a disjunction, handle both cases.

!hp1 hp2 hp3. (hp1 |-- hp3) ==> (hp2 |-- hp3) ==> (hp1 || hp2 |-- hp3)

!hp1 hp2 hp3. (hp1 |-- hp3) ==> (hp2 |-- hp3) ==> (hp1 || hp2 |-- hp3)

hor_monotonehor_monotone — proved. |||| is monotone in both arguments.

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 || hp2 |-- hp1' || hp2')

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 || hp2 |-- hp1' || hp2')

C* keeps two ways of embedding a boolbool into an hprophprop, and the distinction governs almost every routine proof step.

pure(p)pure(p) asserts pp and says nothing about the heap: it is satisfied by every state whenever pp holds. fact(p)fact(p) asserts pp and that the heap is empty — by definition fact(p) -|- pure(p) && empfact(p) -|- pure(p) && emp. Because fact(p)fact(p) claims emptiness, it can sit inside a **** chain without consuming any resource, which is why specifications are written with factfact and why fact(T)fact(T) simply disappears.

The rules below move pure information across **** and &&&&, in and out of assertions. The two hsep_hpure_*hsep_hpure_* rules pull a purepure conjunct out of a separating conjunction; the hsep_hfact_*hsep_hfact_* rules do the same for factfact; and hfact_hpurehfact_hpure is the bridge between the two forms.

hpure_introhpure_intro — proved. Attach a proved proposition to the right-hand side.

!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- pure(p) && hp2)

!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- pure(p) && hp2)

hpure_elimhpure_elim — proved. Consume a purepure conjunct on the left by assuming pp.

!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (pure(p) && hp1 |-- hp2)

!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (pure(p) && hp1 |-- hp2)

hsep_hpure_lefthsep_hpure_left — proved. purepure floats out of the left operand of ****.

!p hp1 hp2. (pure(p) && hp1) ** hp2 -|- pure(p) && (hp1 ** hp2)

!p hp1 hp2. (pure(p) && hp1) ** hp2 -|- pure(p) && (hp1 ** hp2)

hsep_hpure_righthsep_hpure_right — proved. purepure floats out of the right operand of ****. These two are what the pure-pulling normalization step rewrites with.

!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)

!p hp1 hp2. hp1 ** (pure(p) && hp2) -|- pure(p) && (hp1 ** hp2)

hfact_defhfact_def — proved. The defining equation of factfact.

!p hp. fact(p) -|- (pure(p) && emp)

!p hp. fact(p) -|- (pure(p) && emp)

hfact_hpurehfact_hpure — proved. A factfact in front of a **** chain is the same as a purepure conjoined with &&&&. This equation is the pivot between the two embeddings and is used in both directions constantly.

!p hp. fact(p) ** hp -|- pure(p) && hp

!p hp. fact(p) ** hp -|- pure(p) && hp

hfact_hpure_righthfact_hpure_right — proved. The same with the operands on the other side.

!p hp. hp && pure(p) -|- fact(p) ** hp

!p hp. hp && pure(p) -|- fact(p) ** hp

hfact_introhfact_intro — proved. Introduce a proved fact into the right-hand side of an entailment.

!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- fact(p) ** hp2)

!p hp1 hp2. p ==> (hp1 |-- hp2) ==> (hp1 |-- fact(p) ** hp2)

hfact_elimhfact_elim — proved. Move a fact from the left-hand side into the ambient proof context, where ordinary HOL reasoning can use it.

!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- hp2)

!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- hp2)

hfact_elim_duphfact_elim_dup — proved. The same, but keeping the fact on the right as well — the usual shape when a fact must be used and preserved.

!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- fact(p) ** hp2)

!p hp1 hp2. (p ==> (hp1 |-- hp2)) ==> (fact(p) ** hp1 |-- fact(p) ** hp2)

hfact_duphfact_dup — proved. Facts are duplicable: unlike heap resources, fact(p)fact(p) may be split into two copies, because it owns nothing.

!p. fact(p) |-- fact(p) ** fact(p)

!p. fact(p) |-- fact(p) ** fact(p)

hsep_hfact_lefthsep_hfact_left — proved. Reassociate a leading fact out of a nested ****.

!p hp1 hp2. (fact(p) ** hp1) ** hp2 -|- fact(p) ** (hp1 ** hp2)

!p hp1 hp2. (fact(p) ** hp1) ** hp2 -|- fact(p) ** (hp1 ** hp2)

hsep_hfact_righthsep_hfact_right — proved. Float a fact out of the right operand.

!p hp1 hp2. hp1 ** (fact(p) ** hp2) -|- fact(p) ** (hp1 ** hp2)

!p hp1 hp2. hp1 ** (fact(p) ** hp2) -|- fact(p) ** (hp1 ** hp2)

hsep_hfact_commhsep_hfact_comm — proved. Facts commute past a resource; an instance of hsep_commhsep_comm specialized to the shape the normalizer meets.

!hp p. hp ** fact(p) -|- fact(p) ** hp

!hp p. hp ** fact(p) -|- fact(p) ** hp

hpure_add_hfacthpure_add_hfact — proved. If an assertion already implies pp, that information can be materialized as a factfact conjunct without losing anything. This is how a derived range or non-nullity condition is added to a symbolic state.

!p hp. (hp |-- pure(p)) ==> (hp |-- fact(p) ** hp)

!p hp. (hp |-- pure(p)) ==> (hp |-- fact(p) ** hp)

hfact_false_elimhfact_false_elim — proved. A false fact is inconsistent and entails anything, so a branch that establishes fact(F)fact(F) is discharged immediately.

!hp. fact(F) |-- hp

!hp. fact(F) |-- hp

existsexists and forallforall at type hprophprop are the overloaded names for hexistshexists and hforallhforall; they bind a HOL variable of an arbitrary type AA and are satisfied pointwise. The introduction and elimination rules are the expected ones, and the interesting content is in how the quantifiers commute with **** and &&&&.

hexists_introhexists_intro — proved. Supply a witness.

!(x : A) hp hpA. (hp |-- hpA x) ==> (hp |-- (exists x : A. hpA x))

!(x : A) hp hpA. (hp |-- hpA x) ==> (hp |-- (exists x : A. hpA x))

hexists_elimhexists_elim — proved. Consume an existential by proving the goal for an arbitrary witness.

!hp hpA. (!x : A. hpA x |-- hp) ==> ((exists y : A. hpA y) |-- hp)

!hp hpA. (!x : A. hpA x |-- hp) ==> ((exists y : A. hpA y) |-- hp)

hexists_monotonehexists_monotone — proved. A pointwise entailment lifts through existsexists.

!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((exists x:A. hpA x) |-- (exists x:A. hpA' x))

!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((exists x:A. hpA x) |-- (exists x:A. hpA' x))

hforall_introhforall_intro — proved. Prove a universal by proving every instance.

!hp hpA. (!x : A. hp |-- hpA x) ==> (hp |-- (forall x : A. hpA x))

!hp hpA. (!x : A. hp |-- hpA x) ==> (hp |-- (forall x : A. hpA x))

hforall_elimhforall_elim — proved. Instantiate a universal at a chosen xx.

!hp hpA (x : A). (hpA x |-- hp) ==> ((forall x : A. hpA x) |-- hp)

!hp hpA (x : A). (hpA x |-- hp) ==> ((forall x : A. hpA x) |-- hp)

hforall_monotonehforall_monotone — proved. A pointwise entailment lifts through forallforall.

!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((forall x:A. hpA x) |-- (forall x:A. hpA' x))

!hpA hpA'. (!x:A. hpA x |-- hpA' x) ==> ((forall x:A. hpA x) |-- (forall x:A. hpA' x))

Existentials commute with **** in both directions — the equations below are -|--|-, so a proof may push an existential outward to expose the witness, or pull it inward to keep a chain in canonical form.

hsep_hexists_lefthsep_hexists_left — proved. Float an existential out of the left operand.

!hpA hp. (exists x : A. hpA x) ** hp -|- exists x : A. (hpA x ** hp)

!hpA hp. (exists x : A. hpA x) ** hp -|- exists x : A. (hpA x ** hp)

hsep_hexists_righthsep_hexists_right — proved. Float an existential out of the right operand.

!hp hpA. hp ** (exists x : A. hpA x) -|- exists x : A. (hp ** hpA x)

!hp hpA. hp ** (exists x : A. hpA x) -|- exists x : A. (hp ** hpA x)

Universals are different. The corresponding rules are stated with |--|--, not -|--|-, and only one direction holds.

hsep_hforall_lefthsep_hforall_left — proved. One-way only: distributing **** into a universal is sound, but the converse is not derivable — the reverse direction would let a single heap fragment hphp be shared by every instance xx, which **** forbids.

!hpA hp. (forall x : A. hpA x) ** hp |-- forall x : A. (hpA x ** hp)

!hpA hp. (forall x : A. hpA x) ** hp |-- forall x : A. (hpA x ** hp)

hsep_hforall_righthsep_hforall_right — proved. The mirror image, likewise one-way.

!hp hpA. hp ** (forall x : A. hpA x) |-- forall x : A. (hp ** hpA x)

!hp hpA. hp ** (forall x : A. hpA x) |-- forall x : A. (hp ** hpA x)

With &&&& in place of **** the asymmetry persists, but for the ordinary logical reason rather than a resource one: &&&& duplicates the state, so existentials still commute in both directions while universals do not.

hand_hexists_lefthand_hexists_left — proved. Existentials commute with &&&& on the left.

!hpA hp. (exists x : A. hpA x) && hp -|- exists x : A. (hpA x && hp)

!hpA hp. (exists x : A. hpA x) && hp -|- exists x : A. (hpA x && hp)

hand_hexists_righthand_hexists_right — proved. And on the right.

!hp hpA. hp && (exists x : A. hpA x) -|- exists x : A. (hp && hpA x)

!hp hpA. hp && (exists x : A. hpA x) -|- exists x : A. (hp && hpA x)

hand_hforall_lefthand_hforall_left — proved. One direction only, as with ****.

!hpA hp. (forall x : A. hpA x) && hp |-- forall x : A. (hpA x && hp)

!hpA hp. (forall x : A. hpA x) && hp |-- forall x : A. (hpA x && hp)

hand_hforall_righthand_hforall_right — proved. The mirror image.

!hp hpA. hp && (forall x : A. hpA x) |-- forall x : A. (hp && hpA x)

!hp hpA. hp && (forall x : A. hpA x) |-- forall x : A. (hp && hpA x)

Inside a proof block, every rule on this page is a thmthm-valued call. The accessor is the rule’s registered name prefixed with get_get_:

[[cst::proof]] {
  thm assoc = get_hsep_assoc();  // |- !hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)
  cst_set_symbolic_state(rewrite_rule(THM_LIST(assoc), cst_get_symbolic_state()));
}

[[cst::proof]] {
  thm assoc = get_hsep_assoc();  // |- !hp1 hp2 hp3. (hp1 ** hp2) ** hp3 -|- hp1 ** (hp2 ** hp3)
  cst_set_symbolic_state(rewrite_rule(THM_LIST(assoc), cst_get_symbolic_state()));
}

The theorem comes back fully quantified; spec_rulespec_rule instantiates it, and match_mp_rulematch_mp_rule discharges an implicational rule such as hentail_transhentail_trans against a theorem you already hold.

The complete accessor index — every get_*get_* declaration in proof_kernel.hproof_kernel.h, in header order, with its exact HOL statement — is in Kernel Objects and Theorems. An accessor marked @derived@derived there corresponds to a lemma that the kernel derives from the rules above rather than one of the core set: hsep_hfalse_lefthsep_hfalse_left, hsep_hfact_commhsep_hfact_comm, hfact_hpure_righthfact_hpure_right, hsep_comm_left_parthsep_comm_left_part, hentail_sym_lefthentail_sym_left, hsep_cancel_left_eqhsep_cancel_left_eq, hfact_elim_duphfact_elim_dup, hpure_add_hfacthpure_add_hfact, hsep_achsep_ac, and heq_symheq_sym. The marker is about layering within the kernel’s own development, not about trust: derived and non-derived accessors alike are proved theorems.

A rule that has no get_*get_* accessor is still reachable by name:

thm mono = get_theorem_by_name("monoidal_hsep");

thm mono = get_theorem_by_name("monoidal_hsep");

• Every rule on this page is proved: the four separation-algebra laws are theorems about mem_joinmem_join, and everything else follows from them and from the definitions of the connectives. C*‘s axioms live in the typed-memory layer, not here.
• unit_joinunit_join, unit_specunit_spec, join_commjoin_comm, and join_assocjoin_assoc are the entire foundation. Commutativity of ****, the neutrality of empemp, and the wand adjunction are consequences, not assumptions.
• |--|-- is a preorder, antisymmetric up to -|--|-, and -|--|- is genuine HOL equality on hprophprop, so every -|--|- rule doubles as a rewrite.
• (hprop, **, emp)(hprop, **, emp) is a commutative monoid; hsep_achsep_ac packages that fact in the form rewriting consumes, and monoidal_hsepmonoidal_hsep is what gives hitersephitersep its library.
• hsep_cancel_lefthsep_cancel_left is the frame rule at the assertion level; hsep_monotonehsep_monotone generalizes it to both operands at once.
• -*-* and -->--> are used through their adjunctions rather than their definitions.
• pure(p)pure(p) constrains only the proposition; fact(p)fact(p) also claims an empty heap, is duplicable, and is what specifications are written with.
• Existentials commute with **** and &&&& as equalities; universals only distribute one way.