C*：开发与证明一体化

证明规则

EN | 中文

证明规则

本页列出 C* 证明内核提供的分离逻辑规则。每个条目给出规则的注册名及其在内核中的确切表述。注册名就是传给 get_theorem_by_nameget_theorem_by_name 的名字，也用于 proof_kernel.hproof_kernel.h 中相应的 get_*get_* 访问器。

下文使用的术语和记号——hprophprop、****、-*-*、&&&&、||||、-->-->、empemp、purepure、factfact、 |--|--、-|--|-，以及量词 existsexists 与 forallforall——在内存模型与断言中定义。下文的每条表述都涉及以下两点，因此在此重申：|--|-- 是蕴含（hentailhentail，类型为 boolbool），而 -|--|- 是断言之间的 HOL 等式（-|--|- 就是 hprophprop 类型上的 ==），并非另设的等价关系。内核证明了 heqheq，即 !hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)!hp1 hp2. (hp1 -||- hp2) <=> (hp1 -|- hp2)，由此可以将互相蕴含与等式互换使用。由于 -|--|- 就是等式，下文的每条 -|--|- 规则都可以用于双向重写。

这些连接词都定义在内存模型之上，并非原始概念：**** 对状态的各种拆分作量化，-*-* 对状态的各种扩张作量化，empemp 表示内存为空。因此 **** 的结合律与交换律、empemp 的单位元性质以及魔术棒的伴随，都是模型的推论，并非假设。

蕴含

|--|-- 是 hprophprop 上的预序，并且以 -|--|- 为等式满足反对称性。下面五条规则是各项证明的基础：hentail_transhentail_trans 串联各步，hentail_antisymhentail_antisym 把一对蕴含转换为可用于重写的等式。

hentail_reflhentail_refl——蕴含具有自反性；当目标两侧完全相同时，这条规则就能解决目标。

!hp. hp |-- hp
!hp. hp |-- hp

hentail_transhentail_trans——蕴含具有传递性，可以串联各步推理，逐步推进证明。

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

hentail_antisymhentail_antisym——互相蕴含即断言的等式。

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

hentail_sym_lefthentail_sym_left——反过来，断言的等式可以弱化为蕴含，从而将重写引理用于蕴含目标。

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

heq_symheq_sym——断言等式具有对称性。此处用 <=><=> 表述，因此可以用来调整目标的方向。

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

分离合取

**** 满足结合律与交换律，并以 empemp 为单位元，也就是说，(hprop, **, emp)(hprop, **, emp) 构成交换幺半群。重排断言的空间部分时，可以使用以下规则。

hsep_assochsep_assoc——**** 满足结合律。

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

hsep_commhsep_comm——**** 满足交换律。分离合取不限定它所连接的两块堆片段的顺序。

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

hsep_hemp_lefthsep_hemp_left——empemp 是左单位元。

!hp. emp ** hp -|- hp
!hp. emp ** hp -|- hp

hsep_hemp_righthsep_hemp_right——empemp 是右单位元。

!hp. hp ** emp -|- hp
!hp. hp ** emp -|- hp

hsep_comm_left_parthsep_comm_left_part——把右嵌套链中间的合取项移到最前面。这条规则主要用于将某个特定资源移到长 **** 链的头部，无须手工展开整条链。

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

hsep_achsep_ac——将结合律与交换律合并为一条定理：上面三条重写以 HOL 重写器要求的形式组合，用于对 **** 作 AC 规范化。这里的 &&&& 是布尔合取（&&&& 是重载的，三个分量都是 boolbool），并非 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))

规范化使用的就是这条定理。用 hsep_achsep_ac 重写，可以调整 **** 链的顺序和括号，将其化为规范形式。因此，处理长空间合取时，很少需要单独使用 hsep_assochsep_assoc 与 hsep_commhsep_comm。

neutral_hsepneutral_hsep——在 HOL 的 neutralneutral 意义下，empemp 就是 **** 的单位元。

neutral(**) = emp
neutral(**) = emp

monoidal_hsepmonoidal_hsep——**** 是幺半群运算，这是 HOL 通用 iterateiterate 机制的前提。有了这条定理，迭代分离合取 hitersephitersep 就能直接复用整个 ITERATE_*ITERATE_* 库（插入、并集、差集、删除）。

monoidal(**)
monoidal(**)

框架消除与单调性

框架消除使分离逻辑能够处理更大规模的问题：关于少数几个堆单元的证明，在一并保留其余堆且不作改动时依然成立。在 C* 中，这一原则表述为关于断言的普通定理，而非关于三元组的元定理。

hsep_cancel_lefthsep_cancel_left——在左侧保留任意框架 hp3hp3，同时加强 **** 的另一侧。

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

hsep_cancel_righthsep_cancel_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——以等式表述的版本：在 **** 的右操作数内部重写，整条断言保持不变。

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

hsep_monotonehsep_monotone——**** 对两个参数同时具有单调性；两条消去规则都是它的实例，只需让其中一条蕴含采用自反形式。

!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')
!hp1 hp1' hp2 hp2'. (hp1 |-- hp1') ==> (hp2 |-- hp2') ==> (hp1 ** hp2 |-- hp1' ** hp2')
定理 1（框架规则）。

hsep_cancel_lefthsep_cancel_left 就是框架规则，只不过表述在断言层面而非三元组层面。把 hp3hp3 理解为框架 FF：任何在小足迹上证明的蕴含，在加入一块不相交的剩余部分后依然成立。

这里没有对 FF 作任何假设。前提的证明不涉及它，而 **** 的定义保证框架占据一块不相交的内存，因此结论对任意 FF 都成立。符号执行引擎由此可以将一条小足迹蕴含（只涉及某条语句所访问的单元）应用于完整的符号状态。

这些规则对应哪些策略，以及如何在证明中消去目标两侧相匹配的资源，见分离逻辑的后向证明；local_applylocal_apply 所用的前向式 frame_right_slruleframe_right_slrule，在同样意义下就是 hsep_cancel_righthsep_cancel_right。

伴随

以下两个连接词通过伴随关系刻画，而非引入与消去规则：分离蕴含 -*-* 是 **** 的右伴随，普通蕴含 -->--> 是 &&&& 的右伴随。两条规则都以 <=><=> 表述，因此可以根据目标选择使用方向。

hwand_hsep_adjointhwand_hsep_adjoint——魔术棒的伴随。

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

himpl_hand_adjointhimpl_hand_adjoint——蕴含的伴随。

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

实际证明中几乎不展开魔术棒的定义（对当前状态的所有扩张作量化），而是通过 hwand_hsep_adjointhwand_hsep_adjoint 使用 -*-*：将目标 hp1 |-- hp2 -* hp3hp1 |-- hp2 -* hp3 转换为 **** 形式的目标 hp1 ** hp2 |-- hp3hp1 ** hp2 |-- hp3，即可使用常规的空间推理机制处理。反过来，消耗关于魔术棒的假设时，也是先将其转换为分离合取。

真、假、合取与析取

非空间连接词与普通直觉主义逻辑中的行为相同，只是逐点提升到了 hprophprop。需要注意 truetrue、falsefalse 与 **** 的相互作用：fact(T)fact(T) 就是 empemp，可以从分离合取中消去； fact(F)fact(F) 则会吸收与它相邻的部分。

htrue_defhtrue_def——hprophprop 类型上的 truetrue 就是 pure(T)pure(T)：任何状态都满足它，包括非空状态。

true -|- pure(T)
true -|- pure(T)

hfalse_defhfalse_def——falsefalse 就是 pure(F)pure(F)，没有任何状态满足它。

false -|- pure(F)
false -|- pure(F)

htrue_introhtrue_intro——任何断言都蕴含 truetrue；这会丢弃整条断言。

!hp. hp |-- true
!hp. hp |-- true

htrue_hemphtrue_hemp——平凡的事实就是空堆。注意它与 htrue_defhtrue_def 的区别：fact(T)fact(T) 还要求堆为空，而 truetrue 没有这一要求。

fact(T) -|- emp
fact(T) -|- emp

hfalse_elimhfalse_elim——断言层面的爆炸律（ex falso）。

!hp. false |-- hp
!hp. false |-- hp

hsep_hfalse_lefthsep_hfalse_left——falsefalse 会湮灭整个分离合取。

!hp. false ** hp |-- false
!hp. false ** hp |-- false

htrue_elim_lefthtrue_elim_left——**** 左侧的平凡事实会消失。

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

htrue_elim_righthtrue_elim_right——右侧同理。

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

hfalse_absorb_lefthfalse_absorb_left——假事实会吸收与它合并的任何断言。

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

hfalse_absorb_righthfalse_absorb_right——右侧同理。

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

hand_introhand_intro——要证明一个合取，就从同一条断言出发证明两个合取项。与 **** 不同，&&&& 不会拆分堆：两侧描述的是同一个状态。

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

hand_elim1hand_elim1——投影出左合取项。

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

hand_elim2hand_elim2——投影出右合取项。

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

hand_assochand_assoc——&&&& 满足结合律。

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

hand_commhand_comm——&&&& 满足交换律。

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

hand_monotonehand_monotone——&&&& 对两个参数都具有单调性。

!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——选择左析取支。

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

hor_intro2hor_intro2——选择右析取支。

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

hor_elimhor_elim——分类讨论：使用一个析取时，需要处理两种情况。

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

hor_monotonehor_monotone——|||| 对两个参数都具有单调性。

!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* 提供两种将 boolbool 嵌入 hprophprop 的方式，几乎每个常规证明步骤都涉及两者的区别。

pure(p)pure(p) 断言 pp，对堆不作任何说明：只要 pp 成立，任何状态都满足它。fact(p)fact(p) 既断言 pp，又断言堆为空，按定义 fact(p) -|- pure(p) && empfact(p) -|- pure(p) && emp。由于 fact(p)fact(p) 断言堆为空，它可以出现在 **** 链中而不消耗任何资源。这也解释了为什么规约用 factfact 书写，以及为什么 fact(T)fact(T) 可以直接消去。

下面的规则用于在 **** 与 &&&& 之间转换纯信息，并将其移入或移出断言。两条 hsep_hpure_*hsep_hpure_* 规则把 purepure 合取项从分离合取中提取出来；hsep_hfact_*hsep_hfact_* 规则对 factfact 做同样的事； hfact_hpurehfact_hpure 则用于转换这两种形式。

hpure_introhpure_intro——把一条已证命题附加到右侧。

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

hpure_elimhpure_elim——通过假设 pp 来消耗左侧的 purepure 合取项。

!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——从 **** 的左操作数中提取 purepure。

!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——从 **** 的右操作数中提取 purepure。规范化时，提取纯事实的步骤就使用这两条重写规则。

!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——factfact 的定义方程。

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

hfact_hpurehfact_hpure——**** 链前面的 factfact 等同于用 &&&& 连接的 purepure。这条等式是两种嵌入方式之间的转换依据，两个方向都经常用到。

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

hfact_hpure_righthfact_hpure_right——同样的等式，调整了操作数的位置。

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

hfact_introhfact_intro——把一条已证事实引入蕴含的右侧。

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

hfact_elimhfact_elim——把事实从左侧移入外围的证明上下文，供普通的 HOL 推理使用。

!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——同上，同时在右侧保留该事实；当一条事实既要使用又要保留时，通常采用这种形式。

!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——事实是可复制的：与堆资源不同，fact(p)fact(p) 可以拆分成两份副本，因为它不拥有任何资源。

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

hsep_hfact_lefthsep_hfact_left——通过重新结合，把开头的事实从嵌套的 **** 中提取出来。

!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——从右操作数中提取事实。

!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——事实可以与资源交换位置；这是 hsep_commhsep_comm 针对规范化器所处理形式的特例。

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

hpure_add_hfacthpure_add_hfact——如果一条断言已经蕴含 pp，就可以将这一信息显式表示为一个 factfact 合取项，同时保留原断言。推导出的范围条件或非空条件正是这样加入符号状态的。

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

hfact_false_elimhfact_false_elim——假事实自相矛盾，可以蕴含任何断言，因此一旦在分支中证明 fact(F)fact(F)，就能立即卸除该分支的证明义务。

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

量词

hprophprop 类型上的 existsexists 与 forallforall 是 hexistshexists 与 hforallhforall 的重载名；它们绑定一个任意类型 AA 的 HOL 变量，满足关系按逐点方式定义。引入与消去规则与通常的规则一致，这里着重说明量词如何与 **** 和 &&&& 交换。

hexists_introhexists_intro——提供一个例证。

!(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——通过对任意例证证明目标，来消耗一个存在量词。

!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——将逐点蕴含提升为存在量化断言之间的蕴含。

!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——通过证明每个实例来证明全称断言。

!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——把全称断言实例化到选定的 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——将逐点蕴含提升为全称量化断言之间的蕴含。

!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))

存在量词与 **** 在两个方向上都可交换。下面的等式都是 -|--|-，因此证明既可以把存在量词向外移，使例证显式出现，也可以将其向内移，使链保持规范形式。

hsep_hexists_lefthsep_hexists_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)

hsep_hexists_righthsep_hexists_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)

全称量词则不同。对应的规则以 |--|-- 而非 -|--|- 表述，并且只有一个方向成立。

hsep_hforall_lefthsep_hforall_left——只在一个方向上成立：将 **** 分配到全称量词内部是健全的，但逆向无法推导，因为反方向会允许每个实例 xx 共享同一块堆片段 hphp，而 **** 不允许这样做。

!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——镜像版本，同样只有单向成立。

!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)

把 **** 换成 &&&& 后，这种不对称依然存在，但原因来自普通逻辑而非资源：&&&& 会复制状态，所以存在量词仍在两个方向上可交换，全称量词则不然。

hand_hexists_lefthand_hexists_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——右侧亦然。

!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——与 **** 一样，只有一个方向成立。

!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——镜像版本。

!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)

在 C* 中取用规则

在证明块内部，可以通过返回 thmthm 的函数调用获取本页的规则。访问器名称由规则的注册名加上前缀 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()));
}

返回的定理经过完全量化；spec_rulespec_rule 可以将其实例化，match_mp_rulematch_mp_rule 则利用已有定理卸除 hentail_transhentail_trans 这类蕴含式规则的前提。

完整的访问器索引见内核对象与定理，其中按头文件顺序列出 proof_kernel.hproof_kernel.h 中的每条 get_*get_* 声明，并附其确切的 HOL 表述。其中标记为 @derived@derived 的访问器，对应的是内核由上述规则推导出的引理，而非核心规则集中的成员： 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 与 heq_symheq_sym。这一标记表示内核开发中的分层，与信任无关：无论是否标记为派生，访问器返回的都是已证明的定理。

没有 get_*get_* 访问器的规则，仍可按名字取得：

thm mono = get_theorem_by_name("monoidal_hsep");
thm mono = get_theorem_by_name("monoidal_hsep");

小结

  • 本页每一条规则都是已证明的定理，由连接词的定义与内存模型推导而来；其上的带类型内存层的每一条规则也是如此。
  • 由于连接词都是定义，**** 的结合律与交换律、empemp 的单位元性质以及魔术棒的伴随都是模型的推论，并非假设。
  • |--|-- 是预序，以 -|--|- 为等式满足反对称性；-|--|- 是 hprophprop 上真正的 HOL 等式，因此每条 -|--|- 规则同时也可以当作一条重写规则。
  • (hprop, **, emp)(hprop, **, emp) 构成交换幺半群；hsep_achsep_ac 将这一事实组合为重写所需的形式， monoidal_hsepmonoidal_hsep 则让 hitersephitersep 可以复用整套库。
  • hsep_cancel_lefthsep_cancel_left 是断言层面的框架规则；hsep_monotonehsep_monotone 把它一次性推广到两个操作数。
  • -*-* 与 -->--> 通过各自的伴随来使用，而非通过定义来使用。
  • pure(p)pure(p) 只约束命题；fact(p)fact(p) 还断言堆为空，可以复制，也是书写规约时所用的形式。
  • 存在量词与 ****、&&&& 以等式形式交换；全称量词只能单向分配。