分离逻辑的后向证明

EN | 中文

前一节中目标统一写为 [Gamma ?- p][Gamma ?- p]，策略通过目标树将一个普通的布尔命题分解为子目标。但 C* 的验证条件通常是分离逻辑蕴含：证明器不仅要处理命题，还必须拆分、选择和重组线性堆资源。本节介绍专门用于此目的的目标表示与策略族，它们建立于前一节的通用目标树之上（同时回引 sllsll 谓词）。

我们以一个取自链表逆置例子的引理作为讨论的核心。这正是前向证明一节中复用为现成定理的那个 sll_unfoldsll_unfold 引理；这里我们终于来证明它。

回顾单向链表谓词 sll pt lsll pt l，它描述一个起始地址为 ptpt、逻辑内容为整数列表 ll 的链表：


thm sll_def = cst_new_rec_definition(
  "sll", get_theorem_by_name("list_RECURSION"),
  `(sll pt [] -|- fact(pt == 0i)) &&
   (sll pt (h :: t) -|- fact(~(pt == 0i)) ** exists q.
      data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr q ** sll q t)`,
  `:addr->(int)list->hprop`);


thm sll_def = cst_new_rec_definition(
  "sll", get_theorem_by_name("list_RECURSION"),
  `(sll pt [] -|- fact(pt == 0i)) &&
   (sll pt (h :: t) -|- fact(~(pt == 0i)) ** exists q.
      data_at (field_addr pt Tlist Fhead) Tint h **
      data_at (field_addr pt Tlist Ftail) Tptr q ** sll q t)`,
  `:addr->(int)list->hprop`);

空链表是空指针；非空链表的头结点拥有 headhead 和 tailtail 字段，且尾指针 qq 指向剩余部分 tt 的链表。

引理 1（unfold_sll_not_nullunfold_sll_not_null）。如果 ptpt 非空且 sll pt lsll pt l 成立，那么 ll 必定为某个 h :: th :: t，并且头结点展开后是两个字段资源加一个后继链表：
forall l pt. ~(pt == 0i) ==> (sll pt l |-- exists h t q. fact(l == h :: t) ** data_at (field_addr pt Tlist Fhead) Tint h ** data_at (field_addr pt Tlist Ftail) Tptr q ** sll q t)
forall l pt. ~(pt == 0i) ==> (sll pt l |-- exists h t q. fact(l == h :: t) ** data_at (field_addr pt Tlist Fhead) Tint h ** data_at (field_addr pt Tlist Ftail) Tptr q ** sll q t)

虽然这看起来就只是“展开定义一次”，但引理实际上包裹了若干互不相同的证明动作：引入全称量词和纯前件 ~(pt == 0i)~(pt == 0i)；将 sll pt l |-- ...sll pt l |-- ... 转变为适合操作资源的目标形态；对 ll 进行分类讨论，在空表分支中利用矛盾消去；在非空分支中展开 sllsll，分解出存在量词和分离合取，为堆结论提供 hh、tt、qq 三个例证，同时简化纯事实并对两侧共有的空间资源施加框架消除。

本节将逐步完成这些步骤。首先：用普通目标能不能表达这种资源结构？

理解分离逻辑目标

普通目标将蕴含看作一个黑盒子。 前一节中的普通目标是 [Gamma ?- p][Gamma ?- p]。引入 unfold_sll_not_nullunfold_sll_not_null 的外层全称量词和蕴含后，得到：

作为普通目标


P_pt: ~(pt == 0i)
--------------------------------
sll pt l |--
  exists h t q.
    fact(l == h :: t) **
    data_at (field_addr pt Tlist Fhead) Tint h **
    data_at (field_addr pt Tlist Ftail) Tptr q **
    sll q t


P_pt: ~(pt == 0i)
--------------------------------
sll pt l |--
  exists h t q.
    fact(l == h :: t) **
    data_at (field_addr pt Tlist Fhead) Tint h **
    data_at (field_addr pt Tlist Ftail) Tptr q **
    sll q t

这是一个普通目标：整条蕴含 sll pt l |-- ...sll pt l |-- ... 被当作一个 boolbool 结论来处理。目标树只知道它是一个需要证明的命题，但对蕴含的内部结构一无所知。证明器无法按标签操作堆资源，就像操作普通假设那样；对目标的任何变换都有破坏蕴含形态的风险。

分离逻辑目标将结构暴露出来。 全文使用如下记号：


p, q               : bool
H, K, P, Q         : hprop
Lambda             : 有序且带标签的普通逻辑前件
Delta              : 有序且带标签的堆前件
ant(Delta)         = Delta 中堆断言之分离合取


p, q               : bool
H, K, P, Q         : hprop
Lambda             : 有序且带标签的普通逻辑前件
Delta              : 有序且带标签的堆前件
ant(Delta)         = Delta 中堆断言之分离合取

打印时呈现为两个前件区域：

分离逻辑目标的打印样式


A_1: p_1
...
A_n: p_n
----------------
L_1: H_1
...
L_m: H_m
================
K


A_1: p_1
...
A_n: p_n
----------------
L_1: H_1
...
L_m: H_m
================
K

对于链表引理，进入此目标模式后得到：

链表例子作为分离逻辑目标


P_pt: ~(pt == 0i)
----------------
H: sll pt l
================
exists h t q.
  fact(l == h :: t) **
  data_at (field_addr pt Tlist Fhead) Tint h **
  data_at (field_addr pt Tlist Ftail) Tptr q **
  sll q t


P_pt: ~(pt == 0i)
----------------
H: sll pt l
================
exists h t q.
  fact(l == h :: t) **
  data_at (field_addr pt Tlist Fhead) Tint h **
  data_at (field_addr pt Tlist Ftail) Tptr q **
  sll q t

现在 P_ptP_pt 是可用于重写和导矛盾的普通逻辑前件，HH 是只能由分离逻辑规则使用的资源，而堆结论整体保留。这一划分直接反映了分离逻辑证明的结构。

进入分离逻辑目标模式

从蕴含进入：SL_MODESL_MODE。

SL_MODESL_MODE


gnode_list SL_MODE(const gnode gn, const char *pattern)


gnode_list SL_MODE(const gnode gn, const char *pattern)

将普通目标 [Lambda ?- (H |-- K)][Lambda ?- (H |-- K)] 转变为分离逻辑目标，同时根据 patternpattern 解构并命名初始堆前件 HH。返回所有结果中的开放叶节点。

最安全的起始形式是将整个前件命名为 "H""H"：


gnode_list gns = SL_MODE(gn, "H");


gnode_list gns = SL_MODE(gn, "H");

如果前件的结构已知，可以在进入时间同时解构。模式语言仅有四种构造：

模式	含义
`HH`	将整个堆前件命名为 `HH`
`H_1 * H_2H_1 * H_2`	拆分外层的分离合取
`H_1 \| H_2H_1 \| H_2`	拆分外层的析取，产生两条分支
`x ? Hx ? H`	消去外层的存在量词，以新变量 `xx` 开启

解析器从括号中读取结构，不设运算符优先级，因此复杂模式必须显式加括号：


SL_MODE(g, "H_1 * ((x ? H_2) | H_3)");


SL_MODE(g, "H_1 * ((x ? H_2) | H_3)");

从堆断言等式进入：EQ_SLTACEQ_SLTAC。 另一种常见目标是两个堆断言相等。此时 SL_MODESL_MODE 不适用，应改用反对称性将等式拆分为两个有向蕴含。

EQ_SLTACEQ_SLTAC


gnode_list EQ_SLTAC(const gnode gn, const char *L_1, const char *L_2)


gnode_list EQ_SLTAC(const gnode gn, const char *L_1, const char *L_2)


     [Lambda; L_1:H_1 ?- H_2]
     [Lambda; L_2:H_2 ?- H_1]
-------------------------------- EQ_SLTAC L_1 L_2
        [Lambda ?- (H_1 = H_2)]


     [Lambda; L_1:H_1 ?- H_2]
     [Lambda; L_2:H_2 ?- H_1]
-------------------------------- EQ_SLTAC L_1 L_2
        [Lambda ?- (H_1 = H_2)]

两条分支各自有独立的标签命名空间，因此 L_1L_1 和 L_2L_2 可以使用同一名称。

分析堆前件

进入分离逻辑目标后，证明器首先面对的是 DeltaDelta 中已有的资源。它们与普通逻辑前件的根本区别在于线性：每个资源恰好使用一次——既不能随意拷贝，也不能随意丢弃。

解构外层结构。 对单个带标签的堆前件，最常用的原子策略如下：

前件形态	策略	效果
`L:(P Q)L:(P Q)`	`HANT_SEP_SLTACHANT_SEP_SLTAC`	拆分为两个带标签的资源
`L:(P \|\| Q)L:(P \|\| Q)`	`HANT_DISJ_SLTACHANT_DISJ_SLTAC`	每个析取支产生一个子目标
`L:(exists x. H)L:(exists x. H)`	`HANT_EXISTS_SLTACHANT_EXISTS_SLTAC`	以新变量开启存在量词
`L:HL:H`	`HANT_RENAME_SLTACHANT_RENAME_SLTAC`	仅更改标签，不更改内容

以上均保留堆结论。例如，拆分分离合取的抽象形式为：


     [Lambda; Delta_R,L_1:P,L_2:Q ?- K]
------------------------------------------------
          [Lambda; Delta,L:(P ** Q) ?- K]


     [Lambda; Delta_R,L_1:P,L_2:Q ?- K]
------------------------------------------------
          [Lambda; Delta,L:(P ** Q) ?- K]

分离合取产生一个子目标（两种资源同时存在）；析取产生两个子目标（状态可能满足任一侧）；开启存在量词时必须选取一个不与目标自由变量捕获的名称。

递归解构整个前件：


gnode_list HANT_DESTRUCT_SLTAC(
  const gnode gn, const char *L, const char *pattern);
gnode_list AUTO_HANT_DESTRUCT_SLTAC(const gnode gn);


gnode_list HANT_DESTRUCT_SLTAC(
  const gnode gn, const char *L, const char *pattern);
gnode_list AUTO_HANT_DESTRUCT_SLTAC(const gnode gn);

前者遵循给定模式；后者按顺序遍历上下文，对每个可见的 ****、|||| 和 existsexists 递归拆分，在每个新的析取分支上继续，直至没有任何此类外层结构存在。

将纯事实移到普通逻辑区域。 为了能让 fact(p)fact(p) 参与普通逻辑重写、算术或导矛盾，将它从堆区域移入 LambdaLambda：


gnode INTRO_FACT_SLTAC(
  const gnode gn, const const_cstr_list lbs);
gnode AUTO_INTRO_FACT_SLTAC(const gnode gn);


gnode INTRO_FACT_SLTAC(
  const gnode gn, const const_cstr_list lbs);
gnode AUTO_INTRO_FACT_SLTAC(const gnode gn);

INTRO_FACT_SLTACINTRO_FACT_SLTAC 选取指定标签；自动版选取当前堆前件中每个顶层的 fact(p)fact(p)。一旦移入，这些命题的行为与前一节中的普通假设无异。

重写、魔术棒以及关闭矛盾分支。 三种更常见的动作：

HANT_CONV_SLTACHANT_CONV_SLTAC：以变换重写指定堆前件；
WAND_MP_SLTACWAND_MP_SLTAC：从 (P -* Q)(P -* Q) 和资源 PP 产生资源 QQ；
CONTR_SLTACCONTR_SLTAC：当某堆前件规范化为 fact(false)fact(false) 时关闭分支。

例如，在链表例子的空链表分支中，展开 sll pt []sll pt [] 得到 fact(pt == 0i)fact(pt == 0i)。用普通逻辑前件 ~(pt == 0i)~(pt == 0i) 重写后得到一个矛盾性资源，CONTR_SLTACCONTR_SLTAC 随即关闭该分支。

构造堆结论

分析堆前件回答的是“我有什么”；操作堆结论回答的是“我还必须构造出什么”。结论 KK 整体保留，策略由它的最外层结构选择。

分离合取划分资源。 如果目标是 K_1 ** K_2K_1 ** K_2，两侧并不能像普通逻辑合取那样全部继承资源。证明器必须指明哪些前件资源归属到左侧子目标，其余归到右侧：

SEP_SLTACSEP_SLTAC


gnode_list SEP_SLTAC(
  const gnode gn, const const_cstr_list labels_for_left)


gnode_list SEP_SLTAC(
  const gnode gn, const const_cstr_list labels_for_left)


     [Lambda; Delta_L ?- K_1]
     [Lambda; Delta_R ?- K_2]
-------------------------------- SEP_SLTAC labels_for_left
     [Lambda; Delta ?- K_1 ** K_2]


     [Lambda; Delta_L ?- K_1]
     [Lambda; Delta_R ?- K_2]
-------------------------------- SEP_SLTAC labels_for_left
     [Lambda; Delta ?- K_1 ** K_2]

析取、存在量词与纯事实。 其余结论侧的策略按结构分组：

结论形态	策略	证明器的选择
`K_1 \|\| K_2K_1 \|\| K_2`	`DISJ1_SLTACDISJ1_SLTAC` / `DISJ2_SLTACDISJ2_SLTAC`	选择左或右的析取支
`exists x. Hexists x. H`	`EXISTS_SLTACEXISTS_SLTAC`	提供例证
多个外层 `existsexists`	`LIST_EXISTS_SLTACLIST_EXISTS_SLTAC`	按顺序提供例证列表
`P (exists x. Q)P (exists x. Q)`	`EXISTS_PULL_SLTACEXISTS_PULL_SLTAC`	先将存在量词提至最外层
若干 `fact(p)fact(p)`	`PURE_SLTACPURE_SLTAC`	将纯事实分离出一个普通目标，保留其余
`KK`	`HCON_CONV_SLTACHCON_CONV_SLTAC`	以变换重写整个堆结论

例如：


     [Lambda; Delta ?- H[w/x]]
-------------------------------- EXISTS_SLTAC w
 [Lambda; Delta ?- exists x. H]


     [Lambda; Delta ?- H[w/x]]
-------------------------------- EXISTS_SLTAC w
 [Lambda; Delta ?- exists x. H]

其中例证的类型必须与存在量词变量的类型一致。

规范化、清理与框架消除

许多分离逻辑目标在语义上已经成立；只是两侧在语法上有差异——一侧展开了定义、纯事实未简化，或者 **** 的结合与排列方式不同。这类目标需要先规范化，再消去共同资源。

变换与清理。


gnode CONV_SLTAC(const gnode gn, const conv cv);
gnode CONV_WITH_ASMP_SLTAC(
  const gnode gn,
  conv (*cvf)(thm_list),
  const thm_list ths);
gnode CLEAN_SLTAC(const gnode gn);
void EMP_SLTAC(const gnode gn);


gnode CONV_SLTAC(const gnode gn, const conv cv);
gnode CONV_WITH_ASMP_SLTAC(
  const gnode gn,
  conv (*cvf)(thm_list),
  const thm_list ths);
gnode CLEAN_SLTAC(const gnode gn);
void EMP_SLTAC(const gnode gn);

CONV_SLTACCONV_SLTAC 依次重写堆结论和每个堆前件。CONV_WITH_ASMP_SLTACCONV_WITH_ASMP_SLTAC 额外将 LambdaLambda 中的普通逻辑前件作为假设定理传递给变换函数，适合“按定义展开再根据当前分支事实简化”的场景。CLEAN_SLTACCLEAN_SLTAC 删除 empemp、fact(true)fact(true) 等单位元并规范化其余部分。如果规范化后堆结论为 empemp 且每个堆前件都是 empemp 或平凡为真的事实，EMP_SLTACEMP_SLTAC 关闭该目标。

框架消除。 除 EMP_SLTACEMP_SLTAC 外，最常见的收尾方式是消去两侧的共同资源：


gnode FRAME_SLTAC(
  const gnode gn, const const_cstr_list labels);
gnode AUTO_FRAME_SLTAC(const gnode gn);


gnode FRAME_SLTAC(
  const gnode gn, const const_cstr_list labels);
gnode AUTO_FRAME_SLTAC(const gnode gn);

FRAME_SLTACFRAME_SLTAC 按标签选择堆前件，在堆结论的顶层多重集中找到与其相等的出现，将两者同时消去（不关闭目标）；AUTO_FRAME_SLTACAUTO_FRAME_SLTAC 按前件顺序贪心地消去所有可匹配的资源，然后清理单位元，并在目标已变得平凡时关闭。

框架匹配按出现次数进行。如果前件中某个资源有两个副本而结论中只有一个，同一结论资源不能被匹配两次。这一资源多重集正是与普通逻辑假设集合的关键区别。

自动初始化：`AUTO_INIT_SLTACAUTO_INIT_SLTAC`

进入分离逻辑目标模式、解构堆前件、清理单位元、引入纯事实、尝试框架消除——这些都是机械性步骤，并且常常以相同顺序打开一个证明。因此库将它们打包为一个组合策略。

定义 3（组合策略）。 组合策略依次调用已有策略，将每一步的未完成叶节点喂给下一步。它不引入新的推理规则；健全性来自它所组合的原子策略。

AUTO_INIT_SLTACAUTO_INIT_SLTAC


gnode_list AUTO_INIT_SLTAC(const gnode gn)


gnode_list AUTO_INIT_SLTAC(const gnode gn)

以如下固定顺序处理目标：


AUTO_INTROS_TAC
SL_MODE "H"
AUTO_HANT_DESTRUCT_SLTAC
CLEAN_SLTAC
AUTO_INTRO_FACT_SLTAC
AUTO_FRAME_SLTAC


AUTO_INTROS_TAC
SL_MODE "H"
AUTO_HANT_DESTRUCT_SLTAC
CLEAN_SLTAC
AUTO_INTRO_FACT_SLTAC
AUTO_FRAME_SLTAC

这条流水线首先引入普通逻辑量词和前件，然后进入分离逻辑目标模式；接着解构可见的堆前件、清理平凡资源、将顶层的纯事实移到普通逻辑区域，最后尝试消去可直接匹配的框架资源。由于拆分析取可能产生分支，它返回所有当前的未完成叶节点，而非单个 gnodegnode。

完整的链表证明

现在我们掌握了证明所需的全部原子策略，也知道了 AUTO_INIT_SLTACAUTO_INIT_SLTAC 在开头组合了哪些步骤。回到开篇的链表引理，将这些工具串联起来：


thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode gn = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(gn, `l:(int)list`, "P_l");
  gn = gns[0];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(gn, "H");
  gn = gns[1];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  gn = AUTO_HANT_DESTRUCT_SLTAC(gn)[0];
  gn = LIST_EXISTS_SLTAC(
    gn, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  gn = CONV_SLTAC(gn, simp_conv(thm_list_n(0)));
  gn = AUTO_FRAME_SLTAC(gn);
  return gnode_prove(root);
}


thm unfold_sll_not_null_proof(const term goal_tm) {
  gnode root = gnode_new_with_ccl(goal_tm);
  gnode gn = AUTO_INIT_SLTAC(root)[0];
  gnode_list gns = CASES_TAC(gn, `l:(int)list`, "P_l");
  gn = gns[0];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  CONTR_SLTAC(gn, "H");
  gn = gns[1];
  gn = CONV_WITH_ASMP_SLTAC(
    gn, rewrite_conv, THM_LIST(sll_def));
  gn = AUTO_HANT_DESTRUCT_SLTAC(gn)[0];
  gn = LIST_EXISTS_SLTAC(
    gn, TERM_LIST(`a0:int`, `a1:(int)list`, `q:addr`));
  gn = CONV_SLTAC(gn, simp_conv(thm_list_n(0)));
  gn = AUTO_FRAME_SLTAC(gn);
  return gnode_prove(root);
}

初始化：从普通目标到资源化目标。 AUTO_INIT_SLTACAUTO_INIT_SLTAC 完成外层引入并设置资源化目标；运行后仅剩一个未完成的叶节点，因此示例取返回列表的第一个元素。

对逻辑列表进行分类讨论。 CASES_TAC(gn, CASES_TAC(gn, l:(int)list, "P_l"), "P_l") 只改变普通逻辑前件，因此两个子目标均停留在分离逻辑目标模式中。空链表分支获得 l = []l = []；非空分支获得 l = a0 :: a1l = a0 :: a1。

空链表分支：展开至矛盾。 用 sll_defsll_def 展开 sll pt []sll pt []，再以分支的逻辑前件化简；此时资源 HH 变为矛盾性，CONTR_SLTACCONTR_SLTAC 关闭该分支。

非空分支：展开、提供例证、框架消除。 展开定义后，非空事实、头/尾字段以及后继 sllsll 暴露出来。AUTO_HANT_DESTRUCT_SLTACAUTO_HANT_DESTRUCT_SLTAC 将外层的 **** 和 existsexists 转化为独立带标签的资源。分类讨论和展开已经确定了三个例证，LIST_EXISTS_SLTACLIST_EXISTS_SLTAC 将它们一并提供；CONV_SLTACCONV_SLTAC 简化纯事实 l == a0 :: a1l == a0 :: a1；两侧剩余的空间资源逐项匹配，AUTO_FRAME_SLTACAUTO_FRAME_SLTAC 一一消去并关闭目标。

最后，gnode_prove(root)gnode_prove(root)——树中每个叶节点都已关闭，因此可以自底向上重建，返回原始引理的定理。

用户自定义组合策略

AUTO_INIT_SLTACAUTO_INIT_SLTAC 展示了库如何封装一套稳定的机械性流程。用户也可以用同样的方式组合已有策略，为自己的证明构建范围更小、更针对性的自动步骤。

如果每一步都产生单个子目标，可以直接串联：


gnode MY_CLEAN_FRAME_SLTAC(const gnode gn) {
  gnode next_gn = CLEAN_SLTAC(gn);
  next_gn = AUTO_INTRO_FACT_SLTAC(next_gn);
  next_gn = AUTO_FRAME_SLTAC(next_gn);
  return next_gn;
}


gnode MY_CLEAN_FRAME_SLTAC(const gnode gn) {
  gnode next_gn = CLEAN_SLTAC(gn);
  next_gn = AUTO_INTRO_FACT_SLTAC(next_gn);
  next_gn = AUTO_FRAME_SLTAC(next_gn);
  return next_gn;
}

但像析取或分离合取结论这样的策略可能产生分支。此时下一步策略必须施加到所有当前叶节点上：


gnode_list gns = AUTO_HANT_DESTRUCT_SLTAC(gn);
APPLY_ALL_TAC(CLEAN_SLTAC, gns);
gns = gnode_leaves(gn);


gnode_list gns = AUTO_HANT_DESTRUCT_SLTAC(gn);
APPLY_ALL_TAC(CLEAN_SLTAC, gns);
gns = gnode_leaves(gn);

重新获取 gnode_leavesgnode_leaves 是必要的：上一步可能关闭了某些目标或产生了新分支，旧的列表未必还代表子树的未完成工作。

分离逻辑策略何以健全

前一节已经覆盖了通用的健全性机制：当策略展开一个目标时，它必须记录一个验证函数；子目标有了定理后，验证函数重建上层定理，gnode_provegnode_prove 将整棵树归约到根定理。分离逻辑策略复用同一机制。

需要额外保证的是资源线性：普通逻辑前件按集合检查，堆前件则按出现次数的多重集检查。同一资源不能被消耗两次。当标签、资源计数、变量新鲜性或类型不满足策略要求时，策略直接失败；它绝不会把缺失的条件当作事实处理。

小结

普通目标将 H |-- KH |-- K 整体当作一个命题；分离逻辑目标则将普通逻辑前件、带标签的堆前件和堆结论分开保存，直接反映资源结构。
SL_MODESL_MODE 处理分离逻辑蕴含；EQ_SLTACEQ_SLTAC 通过两条有向蕴含处理堆断言等式。
HANT_*_SLTACHANT_*_SLTAC 分析已有资源；INTRO_FACT_SLTACINTRO_FACT_SLTAC 将纯事实移入普通逻辑区域；SEP_SLTACSEP_SLTAC 及析取/存在量词策略构造堆结论。
变换与清理是统一的；FRAME_SLTACFRAME_SLTAC 和 AUTO_FRAME_SLTACAUTO_FRAME_SLTAC 按出现次数消去共同资源。
组合策略如 AUTO_INIT_SLTACAUTO_INIT_SLTAC 适用于机械性步骤；分支、例证和资源划分通常需要证明者显式输入。
分离逻辑策略仍通过目标树验证函数重建定理，最终由 HOL 内核检查。

链表例子的典型节奏：初始化目标，对纯数据进行分类讨论，展开空间谓词，提供例证，规范化两侧，框架消除共同资源。之后更丰富的数据结构上的证明都沿用了这条主线。

分离逻辑的后向证明

理解分离逻辑目标

进入分离逻辑目标模式

分析堆前件

构造堆结论

规范化、清理与框架消除

自动初始化：AUTO_INIT_SLTACAUTO_INIT_SLTAC

完整的链表证明

用户自定义组合策略

分离逻辑策略何以健全

小结

自动初始化：`AUTO_INIT_SLTACAUTO_INIT_SLTAC`