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)，正是它允许把 互相蕴含与等式互换使用；由于 -|--|- 确实就是等式，下文每一条 -|--|- 规则都可以在两个 方向上用作重写。

分离代数

其余一切都建立在关于内存合并关系的四条定理之上。它们表述在抽象签名 join : model->model->model->booljoin : model->model->model->bool 与 is_unit : model->boolis_unit : model->bool 之上，内核把它们实例化为 mem_joinmem_join 与 mem_emptymem_empty。C* 的开发并未把它们假设为公理：每一条都是针对具体内存 模型的一次 proveprove，经由对 mem_varmem_var 单元三种状态的分类讨论卸除。（内核源码中以注释 形式保留了这四条的 new_axiomnew_axiom 版本；若模型保持抽象，相应的开发就会是那种形态。）

第一条定律说每个状态都存在与之合并的单位元；第二条说单位元会被吸收；第三、四条分别 赋予合并关系交换律与结合律。

以 HOL 表述如下：

unit_joinunit_join——已证明。每个状态都能与某个单位元合并。

!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——已证明。与单位元合并不改变任何东西。

!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——已证明。合并关系对两个输入是对称的。

!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——已证明。三路拆分总可以重新加括号。

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

蕴含

|--|-- 是 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_* 库（insert、union、 difference、delete）。

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——已证明。平凡的 fact 就是空堆。注意与 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——已证明。逐点的蕴含可以穿过 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——已证明。通过证明每个实例来证明全称断言。

!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——已证明。逐点的蕴含可以穿过 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))

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

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——已证明。只有单向成立：把 **** 分配进全称量词是健全的，但逆向 无法推导——反方向会让同一块堆片段 hphp 被每个实例 xx 共享，而这是 **** 所禁止的。

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

小结

  • 本页每一条规则都是已证明的：分离代数的四条定律是关于 mem_joinmem_join 的定理，其余一切 都由它们与联结词的定义推出。C* 的公理位于带类型的内存层，而不在本页。
  • unit_joinunit_join、unit_specunit_spec、join_commjoin_comm 与 join_assocjoin_assoc 就是全部的基础。**** 的交换律、 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) 还声称堆为空，可以复制，也是书写规约时所用的形式。
  • 存在量词与 ****、&&&& 以等式形式交换；全称量词只能单向分配。