Proof Rules

This page lists the separation-logic rules available in C*‘s proof kernel. Each entry gives the rule’s registered name, which you pass to get_theorem_by_nameget_theorem_by_name, together with the exact statement of the theorem in the kernel. Where a corresponding get_*get_* accessor is declared in proof_kernel.hproof_kernel.h, its name uses the same registered name.

The vocabulary used below — hprophprop, ****, -*-*, &&&&, ||||, -->-->, empemp, purepure, factfact, |--|--, -|--|-, and the quantifiers existsexists and forallforall — is defined in Memory Model and Assertions. Two distinctions apply throughout this page: |--|-- 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 allows mutual entailment and equality to be used interchangeably. Because -|--|- is equality, every -|--|- rule below can be used as a rewrite in either direction.

The connectives are definitions over the memory model, not primitives: **** quantifies over splittings of the state, -*-* over extensions of it, and empemp is satisfied by an empty memory. Thus the associativity and commutativity of ****, the neutrality of empemp and the wand adjunction are consequences of the model, not assumptions.

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

hentail_reflhentail_refl — Entailment is reflexive; this closes a goal whose two sides are identical.

!hp. hp |-- hp

!hp. hp |-- hp

hentail_transhentail_trans — Entailment is transitive, allowing successive proof steps to be chained.

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

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

hentail_antisymhentail_antisym — 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 — The converse direction: an equality of assertions can be weakened to an entailment, allowing a rewriting lemma to be used in an entailment goal.

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

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

heq_symheq_sym — 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 following rules rearrange the spatial part of an assertion.

hsep_assochsep_assoc — **** is associative.

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

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

hsep_commhsep_comm — **** 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 — empemp is a left unit.

!hp. emp ** hp -|- hp

!hp. emp ** hp -|- hp

hsep_hemp_righthsep_hemp_right — empemp is a right unit.

!hp. hp ** emp -|- hp

!hp. hp ** emp -|- hp

hsep_comm_left_parthsep_comm_left_part — Pull the middle conjunct of a right-nested chain to the front. This moves a specific resource to the head of a long **** chain without manually unfolding the whole chain.

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

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

hsep_achsep_ac — The associativity-commutativity bundle: the three rewrites above combined in the form 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))

Rewriting with hsep_achsep_ac reorders and rebrackets a **** chain into a canonical form. Proofs that manipulate long spatial conjunctions therefore rarely need hsep_assochsep_assoc and hsep_commhsep_comm individually.

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

neutral(**) = emp

neutral(**) = emp

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

monoidal(**)

monoidal(**)

Framing allows a proof about a few heap cells to remain valid when the rest of the heap is preserved unchanged. In C* this principle is not a metatheorem about triples but an ordinary theorem about assertions.

hsep_cancel_lefthsep_cancel_left — Apply an entailment to one operand of **** under 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 — The corresponding rule for a frame 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 — 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 — **** is monotone in both arguments simultaneously; both cancellation rules are instances obtained by taking one entailment to be reflexive.

!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 used in either direction as the goal requires.

hwand_hsep_adjointhwand_hsep_adjoint — 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 — 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. Instead, hwand_hsep_adjointhwand_hsep_adjoint is used to reason about -*-*: a goal hp1 |-- hp2 -* hp3hp1 |-- hp2 -* hp3 becomes the ****-goal hp1 ** hp2 |-- hp3hp1 ** hp2 |-- hp3, which can be handled by the usual spatial reasoning rules. 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. The rules also describe how truetrue and falsefalse interact with ****: fact(T)fact(T) is empemp and can be eliminated, while fact(F)fact(F) absorbs any assertion joined with it.

htrue_defhtrue_def — 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 — falsefalse is pure(F)pure(F), satisfied by no state.

false -|- pure(F)

false -|- pure(F)

htrue_introhtrue_intro — Every assertion entails truetrue; this discards an entire assertion.

!hp. hp |-- true

!hp. hp |-- true

htrue_hemphtrue_hemp — 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 — Ex falso at the assertion level.

!hp. false |-- hp

!hp. false |-- hp

hsep_hfalse_lefthsep_hfalse_left — falsefalse annihilates a separating conjunction.

!hp. false ** hp |-- false

!hp. false ** hp |-- false

htrue_elim_lefthtrue_elim_left — Eliminate a trivial fact on the left of ****.

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

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

htrue_elim_righthtrue_elim_right — Likewise on the right.

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

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

hfalse_absorb_lefthfalse_absorb_left — A false fact absorbs any assertion joined with it.

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

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

hfalse_absorb_righthfalse_absorb_right — Likewise on the right.

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

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

hand_introhand_intro — 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 — Project out the left conjunct.

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

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

hand_elim2hand_elim2 — Project out the right conjunct.

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

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

hand_assochand_assoc — &&&& is associative.

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

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

hand_commhand_comm — &&&& is commutative.

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

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

hand_monotonehand_monotone — &&&& 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 — Choose the left disjunct.

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

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

hor_intro2hor_intro2 — Choose the right disjunct.

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

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

hor_elimhor_elim — 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 — |||| 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* provides two ways of embedding a boolbool into an hprophprop. Their distinction matters in routine proof steps.

pure(p)pure(p) asserts pp and imposes no condition on the heap: it is satisfied by every state whenever pp holds. fact(p)fact(p) asserts both 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 occur inside a **** chain without consuming any resource. This is why specifications use factfact and why fact(T)fact(T) can be eliminated.

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 converts between the two forms.

hpure_introhpure_intro — 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 — 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 — Move purepure 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 — Move purepure out of the right operand of ****. The pure-pulling normalization step uses these two rewrite rules.

!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 — The defining equation of factfact.

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

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

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

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

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

hfact_hpure_righthfact_hpure_right — The same equation with the operands rearranged.

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

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

hfact_introhfact_intro — 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 — 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 — The same rule with the fact also preserved on the right, for use when a fact must be both 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 — 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 — 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 — Move 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 — Facts commute past a resource; an instance of hsep_commhsep_comm specialized to the form used by the normalizer.

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

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

hpure_add_hfacthpure_add_hfact — If an assertion already implies pp, that information can be added as a factfact conjunct while preserving the assertion. 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 — 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 follow the usual logical rules. The remaining rules describe how the quantifiers commute with **** and &&&&.

hexists_introhexists_intro — 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 — 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 — 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 — 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 — 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 — 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 — Move 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 — Move 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)

For universals, the corresponding rules use |--|-- rather than -|--|-; the converse entailments need not hold.

hsep_hforall_lefthsep_hforall_left — Distributing **** into a universal is sound. The left-hand side uses one fixed heap split, with hphp holding on the frame, for every instance xx. On the right, the split chosen for **** may depend on the instance, so the converse need not hold.

!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 — The corresponding rule for the right operand, also 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 ****, both quantifiers commute with conjunction in these forms: &&&& tests both operands on the same state, and the other operand does not depend on the quantified variable. For universals, the converse also uses the fact that HOL types are non-empty. The registered universal rules below state one direction of this equivalence; they do not imply that the converse fails.

hand_hexists_lefthand_hexists_left — 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 — 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 — Distribute ordinary conjunction into a universal on the left. Unlike the corresponding rule for ****, this entailment has a valid converse.

!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 — The corresponding rule for the right operand.

!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, each rule on this page can be obtained through a thmthm-valued call. For accessors declared in the kernel header, the name is the rule’s registered name prefixed with get_get_; rules without such an accessor are retrieved by name, as shown below:

[[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 returned theorem is fully quantified; spec_rulespec_rule instantiates it, and match_mp_rulematch_mp_rule discharges an implicational rule such as hentail_transhentail_trans against an existing theorem.

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 identifies layers within the kernel’s own development; both derived and non-derived accessors return proved theorems with the same trust status.

A rule without a get_*get_* accessor can still be retrieved by name:

thm mono = get_theorem_by_name("monoidal_hsep");

thm mono = get_theorem_by_name("monoidal_hsep");

• Every rule on this page is a proved theorem, derived from the definitions of the connectives and the memory model, and so is every rule of the typed-memory layer above it.
• Because the connectives are definitions, the associativity and commutativity of ****, the neutrality of empemp, and the wand adjunction are consequences of the model, not assumptions.
• |--|-- is a preorder, antisymmetric up to -|--|-, and -|--|- is HOL equality on hprophprop, so every -|--|- rule can also be used as a rewrite.
• (hprop, **, emp)(hprop, **, emp) is a commutative monoid; hsep_achsep_ac packages that fact in the form required for rewriting, and monoidal_hsepmonoidal_hsep allows hitersephitersep to use the iteration 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 used in specifications.
• Existentials commute with **** and &&&& as equalities. Universals commute with ordinary conjunction in these forms; for separating conjunction, only the displayed direction holds in general.