tactics API 参考

tactics 包（Luna-Flow/QED/tactics）以反向方式运行证明。ProofState 持有一个根目标和一组待处理子目标；每个 TacticStep 变换第一个待处理目标，最后一个目标关闭时，该包通过 logic 和内核规则正向重放所记录的步骤来构造定理。只有当定理恰好证明根目标时，ps_qed 才返回它。该包依赖 kernel 和 logic。

步骤与内核规则之间的关系在 tactics 设计说明中解释；tactics 教程逐步证明目标。编写证明脚本的用户通过 prover 使用本包。

目标

`Goal`

Goal 是待证明的相继式：假设和结论，全部为命题。

pub struct Goal {
  hyps : Array[@kernel.Term]
  concl : @kernel.Term
}

目标中的联结词是 logic 构建器的基础项，由解析器（parser）产生。

`mk_goal`、`goal_hyps`、`goal_concl` 和 `goal_hyp_count`

这些函数构建并读取目标；goal_hyps 返回副本。

pub fn mk_goal(Array[@kernel.Term], @kernel.Term) -> Goal
pub fn goal_hyps(Goal) -> Array[@kernel.Term]
pub fn goal_concl(Goal) -> @kernel.Term
pub fn goal_hyp_count(Goal) -> Int

步骤

`TacticStep`

TacticStep 是一个反向证明步骤。

pub enum TacticStep {
  Intro(String)
  Exact(String)
  Apply(String)
  Assumption
  Split
  Left
  Right
}

步骤	当前目标	新目标	关闭依据
`Intro(h)`	$\Gamma \vdash a \Rightarrow b$	带局部假设 `h : a` 的 $\Gamma, a \vdash b$	蕴含引入
`Intro(x)`	$\Gamma \vdash (\lambda y.\,P) = (\lambda y.\,\top)$	$\Gamma \vdash P[x/y]$ ，其中 `x` 为新变量	DEDUCT_ANTISYM_RULE 和 ABS
`Exact(n)`	$\Gamma \vdash c$	无	局部假设 `n`，或 `exact` 模式下的目录定理 `n`
`Apply(n)`	$\Gamma \vdash b$	$\Gamma \vdash a$	用 `n : a ⇒ b` 做蕴含消除
`Assumption`	$\Gamma \vdash c$ ，其中 $c \in \Gamma$	无	该假设
`Split`	$\Gamma \vdash a \wedge b$	$\Gamma \vdash a$ ，然后 $\Gamma \vdash b$	合取引入
`Left`	$\Gamma \vdash a \vee b$	$\Gamma \vdash a$	析取引入
`Right`	$\Gamma \vdash a \vee b$	$\Gamma \vdash b$	析取引入

Apply(n) 按以下顺序解析 n：结论为目标的局部蕴含；规则名 imp_elim（在假设和局部假设中找到这样的蕴含）、imp_intro（类似带隐藏局部假设的 Intro）和 and_intro（类似 Split）；然后是 apply 模式下的目录名称。规则名是 tactics 层面的便利设施；用户手册列出了证明脚本文档中约定使用的定理名称。没有 hole 步骤：hole 由 prover 处理。

`step_intro`、`step_exact`、`step_apply`、`step_assumption`、`step_split`、`step_left` 和 `step_right`

这些函数构建相应的 TacticStep 值。

pub fn step_intro(String) -> TacticStep
pub fn step_exact(String) -> TacticStep
pub fn step_apply(String) -> TacticStep
pub fn step_assumption() -> TacticStep
pub fn step_split() -> TacticStep
pub fn step_left() -> TacticStep
pub fn step_right() -> TacticStep

证明状态

`ProofState`

ProofState 是反向证明的抽象状态：根目标、有序的待处理目标（附带重放它们所需的数据），以及证明完成后的最终定理。

type ProofState

状态是不可变的；每个操作都返回一个新状态。

`ps_init` 和 `ps_enter_frame`

ps_init(goal) 以一个待处理目标开始对 goal 的证明。ps_enter_frame 是同一操作，名称是 prover 打开分支帧时使用的。

pub fn ps_init(Goal) -> ProofState
pub fn ps_enter_frame(Goal) -> ProofState

`ps_apply` 和 `ps_apply_script`

ps_apply(state, prelude, ps, step) 对第一个待处理目标运行一个步骤。ps_apply_script 运行一列步骤，并在第一个错误处停止。

pub fn ps_apply(@kernel.KernelState, @logic.PropPrelude, ProofState, TacticStep) -> Result[ProofState, TacticExecError]
pub fn ps_apply_script(@kernel.KernelState, @logic.PropPrelude, ProofState, Array[TacticStep]) -> Result[ProofState, TacticExecError]

新目标被放在其余目标之前，因此 Split 的第一个子目标会接着被处理。关闭目标的步骤会立即通过内核重放其证据；若重放失败，该步骤即失败。

`ps_qed` 和 `ps_close_frame`

ps_qed 返回已完成证明的定理。ps_close_frame 是用于分支帧的同一操作。

pub fn ps_qed(ProofState) -> Result[@kernel.Thm, TacticExecError]
pub fn ps_close_frame(ProofState) -> Result[@kernel.Thm, TacticExecError]

仍有待处理目标时以 UnsolvedGoals 失败。定理在最后一个目标关闭时已被检查：经 β 归约后，其假设必须与根目标的假设一一对应，其结论在 α 等价意义下必须等于根结论；否则关闭步骤已以 ProofSynthesisUnavailable 失败。

`ps_close_current_with_th`

ps_close_current_with_th(state, prelude, ps, th) 用你提供的定理关闭第一个待处理目标，前提是检查该定理能从不超过该目标的假设证明该目标的结论。

pub fn ps_close_current_with_th(@kernel.KernelState, @logic.PropPrelude, ProofState, @kernel.Thm) -> Result[ProofState, TacticExecError]

定理不适合时以 GoalShapeMismatch 失败，没有待处理目标时以 NoGoals 失败。

`ps_isolate_pending_at`

ps_isolate_pending_at(ps, i) 返回一个新的证明状态，其根目标是待处理目标 i，不带原状态的重放上下文；若 i 越界则返回 None。

pub fn ps_isolate_pending_at(ProofState, Int) -> ProofState?

prover 用它在独立的帧中运行分支块，并防止分支内的失败影响其兄弟分支。

test "proof state" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let env = @parser.parse_env_push_local(env, "q", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "⊢ p ∧ q -> q ∧ p").unwrap()
  let ps = @tactics.ps_init(@tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g)))
  let ps = @tactics.ps_apply_script(st, pre, ps, [
    @tactics.step_intro("h"),
    @tactics.step_split(),
  ]).unwrap()
  inspect(@tactics.ps_goal_count(ps), content="2")
  inspect(@tactics.ps_qed(ps) is Err(@tactics.UnsolvedGoals), content="true")
  let ps = @tactics.ps_apply_script(st, pre, ps, [
    @tactics.step_exact("and_elim_r"),
    @tactics.step_exact("and_elim_l"),
  ]).unwrap()
  let th = @tactics.ps_qed(ps).unwrap()
  inspect(@kernel.thm_hyp_count(th), content="0")
  // nothing is left to do
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_split()) is Err(@tactics.NoGoals), content="true")
}

观察证明

`ps_goal_count`、`ps_current_goal` 和 `ps_pending_goal_at`

ps_goal_count 是待处理目标的数量。ps_current_goal 返回第一个目标，ps_pending_goal_at 返回指定下标处的目标。

pub fn ps_goal_count(ProofState) -> Int
pub fn ps_current_goal(ProofState) -> Goal?
pub fn ps_pending_goal_at(ProofState, Int) -> Goal?

`ps_root_goal`

ps_root_goal 返回证明起始的目标。

pub fn ps_root_goal(ProofState) -> Goal

`LocalHyp`、`local_hyp_name` 和 `local_hyp_term`

LocalHyp 是由 Intro 引入的具名假设，即用户所见的形式。

type LocalHyp

pub fn local_hyp_name(LocalHyp) -> String
pub fn local_hyp_term(LocalHyp) -> @kernel.Term

`ps_current_local_hyps` 和 `ps_current_branch_path`

这些函数返回第一个待处理目标的局部假设和分支路径。分支路径从根开始列出在每个 Split 处取了哪个子目标（1 或 2），以及 Left 或 Right（始终为 1）。

pub fn ps_current_local_hyps(ProofState) -> Array[LocalHyp]
pub fn ps_current_branch_path(ProofState) -> Array[Int]

`ProofGoalView`、`ps_current_focus` 和 `ps_pending_focus_at`

ProofGoalView 把一个待处理目标与其局部假设和分支路径捆绑在一起。这两个函数返回第一个待处理目标或指定下标处目标的视图。

type ProofGoalView

pub fn ps_current_focus(ProofState) -> ProofGoalView?
pub fn ps_pending_focus_at(ProofState, Int) -> ProofGoalView?
pub fn proof_goal_view_goal(ProofGoalView) -> Goal
pub fn proof_goal_view_locals(ProofGoalView) -> Array[LocalHyp]
pub fn proof_goal_view_branch_path(ProofGoalView) -> Array[Int]

`ProofStateSnapshot` 和 `ps_snapshot`

ps_snapshot 把根目标、待处理目标数量和当前焦点捕获到一个值中，用于诊断。

type ProofStateSnapshot

pub fn ps_snapshot(ProofState) -> ProofStateSnapshot
pub fn proof_state_snapshot_root_goal(ProofStateSnapshot) -> Goal
pub fn proof_state_snapshot_pending_goal_count(ProofStateSnapshot) -> Int
pub fn proof_state_snapshot_current(ProofStateSnapshot) -> ProofGoalView?

test "observe" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "⊢ p -> p ∧ p").unwrap()
  let ps = @tactics.ps_init(@tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g)))
  let ps = @tactics.ps_apply_script(st, pre, ps, [@tactics.step_intro("h"), @tactics.step_split()]).unwrap()
  assert_eq(@tactics.ps_current_local_hyps(ps).map(@tactics.local_hyp_name), ["h"])
  assert_eq(@tactics.ps_current_branch_path(ps), [1])
  let second = @tactics.ps_pending_focus_at(ps, 1).unwrap()
  assert_eq(@tactics.proof_goal_view_branch_path(second), [2])
  let snap = @tactics.ps_snapshot(ps)
  inspect(@tactics.proof_state_snapshot_pending_goal_count(snap), content="2")
}

重放上下文

这些枚举描述待处理目标在关闭时将如何被重放。它们出现在接口中是因为待处理目标携带它们；调用者不应自行构造。

`PendingRefine`

PendingRefine 记录一个需要正向撤销的反向步骤：对局部蕴含项（ImpBackwardTerm）或蕴含定理（ImpBackwardTheorem）的 apply，或对量化目标的 intro，其中包含用户的绑定子和一个新的重放绑定子（AbsBackwardTerm）。

pub enum PendingRefine {
  ImpBackwardTerm(@kernel.Term)
  ImpBackwardTheorem(@kernel.Thm)
  AbsBackwardTerm(@kernel.Term, @kernel.Term)
}

`SplitRole`

SplitRole 把一个目标标记为 Split 的左半或右半；右半在关闭时接收左半的定理。

pub enum SplitRole {
  SplitNone
  SplitLeft(@kernel.Term)
  SplitRight(@kernel.Term, @kernel.Thm?)
}

`OrContext`

OrContext 标记由 Left 或 Right 产生的目标，附带完整的析取式和另一分支。

pub enum OrContext {
  OrNone
  OrPendingLeft(@kernel.Term, @kernel.Term)
  OrPendingRight(@kernel.Term, @kernel.Term)
}

错误

`TacticExecError`

TacticExecError 是某个步骤或 ps_qed 的失败。

pub enum TacticExecError {
  UnknownName(String)
  GoalShapeMismatch(String)
  ApplyMismatch(String)
  NoGoals
  UnsolvedGoals
  ProofSynthesisUnavailable(String)
  Logic(@kernel.LogicError)
}

构造子	含义
`UnknownName(n)`	`n` 既不是局部假设也不是目录名称。
`GoalShapeMismatch(msg)`	目标不具有该步骤所需的形状，或 `exact` 给出的见证不能关闭它。
`ApplyMismatch(msg)`	`apply` 得到的不是以该目标为结论的蕴含。
`NoGoals`	对已完成的证明应用了一个步骤。
`UnsolvedGoals`	仍有待处理目标时调用了 `ps_qed`。
`ProofSynthesisUnavailable(msg)`	重放无法为根目标构造定理。
`Logic(e)`	重放期间某条内核或 logic 规则失败。

`tactic_goal_shape_mismatch` 和 `tactic_no_goals`

这些函数构建包外调用者自行抛出的两种错误：当分支块与其目标不匹配时，prover 会使用它们。

pub fn tactic_goal_shape_mismatch(String) -> TacticExecError
pub fn tactic_no_goals() -> TacticExecError

test "errors" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "⊢ p -> p").unwrap()
  let ps = @tactics.ps_init(@tactics.mk_goal(@parser.parsed_goal_hyps(g), @parser.parsed_goal_concl(g)))
  let ps = @tactics.ps_apply(st, pre, ps, @tactics.step_intro("h")).unwrap()
  // `truth` is a catalog name, but not an implication
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_apply("truth")) is Err(@tactics.ApplyMismatch(_)), content="true")
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_exact("nope")) is Err(@tactics.UnknownName("nope")), content="true")
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_split()) is Err(@tactics.GoalShapeMismatch(_)), content="true")
  inspect(@tactics.ps_apply(st, pre, ps, @tactics.step_assumption()) is Ok(_), content="true")
}

tactics API 参考

目标

Goal

mk_goal、goal_hyps、goal_concl 和 goal_hyp_count

步骤

TacticStep

step_intro、step_exact、step_apply、step_assumption、step_split、step_left 和 step_right

证明状态

ProofState

ps_init 和 ps_enter_frame

ps_apply 和 ps_apply_script

ps_qed 和 ps_close_frame

ps_close_current_with_th

ps_isolate_pending_at

观察证明

ps_goal_count、ps_current_goal 和 ps_pending_goal_at

ps_root_goal

LocalHyp、local_hyp_name 和 local_hyp_term

ps_current_local_hyps 和 ps_current_branch_path

ProofGoalView、ps_current_focus 和 ps_pending_focus_at

ProofStateSnapshot 和 ps_snapshot