research_rewrite API

research_rewrite 包（Luna-Flow/QED/research_rewrite）是用于重写和化简证明目标的研究原型。它在选定位置重写目标的结论，记录每一步如何用内核规则重放，并能再次检查这样的记录。它只依赖 kernel 和 logic。

research_rewrite 设计说明解释了重放模型，research_rewrite 教程演示了一次重写。

请求

`RewriteWitness`、`ConnectorKind` 及其构造函数

RewriteWitness 表示用哪个等式来证成一次重写：按名称引用目标的局部假设、一个显式给出的定理、某个联结词的定义，或 β 归约。

pub enum RewriteWitness {
  LocalEquality(String)
  ExplicitTheorem(@kernel.Thm)
  CanonicalUnfold(ConnectorKind)
  BetaNormalization
}

pub enum ConnectorKind {
  Not
  Imp
  And
  Or
}

pub fn research_local_equality(String) -> RewriteWitness
pub fn research_explicit_theorem(@kernel.Thm) -> RewriteWitness
pub fn research_canonical_unfold_not() -> RewriteWitness
pub fn research_canonical_unfold_imp() -> RewriteWitness
pub fn research_canonical_unfold_and() -> RewriteWitness
pub fn research_canonical_unfold_or() -> RewriteWitness
pub fn research_beta_normalization() -> RewriteWitness

局部或显式见证必须得出等式 $l = r$ 。联结词展开会把prelude 常量的应用重写为其经 β 归约的定义。

`RewriteDirection`、`research_left_to_right` 和 `research_right_to_left`

RewriteDirection 表示是把 $l$ 替换为 $r$ ，还是把 $r$ 替换为 $l$ 。

pub enum RewriteDirection {
  LeftToRight
  RightToLeft
}

pub fn research_left_to_right() -> RewriteDirection
pub fn research_right_to_left() -> RewriteDirection

从右到左只支持局部和显式见证；折叠定义或 β 展开会诚实失败。

`RewriteSiteStep` 及其构造函数

位置（site）是从结论的根到待重写子项的一条路径：进入应用的函数部分或参数部分，或进入抽象的主体。

pub enum RewriteSiteStep {
  CombFun
  CombArg
  AbsBody
}

pub fn research_site_comb_fun() -> RewriteSiteStep
pub fn research_site_comb_arg() -> RewriteSiteStep
pub fn research_site_abs_body() -> RewriteSiteStep

空路径表示整个结论。在抽象之下重写（AbsBody）不受支持，会诚实失败。

`RewriteRequest` 和 `research_rewrite_request`

请求由见证、方向和位置组合而成。

pub struct RewriteRequest {
  witness : RewriteWitness
  direction : RewriteDirection
  site : Array[RewriteSiteStep]
}

pub fn research_rewrite_request(RewriteWitness, RewriteDirection, Array[RewriteSiteStep]) -> RewriteRequest

重写

`research_rewrite_term_concl`

research_rewrite_term_concl(state, prelude, locals, concl, request) 对命题 concl 执行一次重写。locals 是 LocalEquality 可以引用的具名假设。

pub fn research_rewrite_term_concl(@kernel.KernelState, @logic.PropPrelude, Array[(String, @kernel.Term)], @kernel.Term, RewriteRequest) -> RewriteResult

它返回重写后的结论以及一段仅含一个片段的重放义务，或者诚实失败：结论不是命题、位置不存在、见证未知或与该位置的子项不匹配，或某个内核步骤失败。

`research_simplify_term_concl` 和 `SimplifyConfig`

research_simplify_term_concl 反复重写直到不再变化：每一轮中，若 allow_unfold 则展开联结词，若 allow_beta 则做 β 归约，并应用 rewrite_requests 中每个匹配的请求。step_limit 限制片段数量。

pub struct SimplifyConfig {
  step_limit : Int
  allow_unfold : Bool
  allow_beta : Bool
  rewrite_requests : Array[RewriteRequest]
}

pub fn research_simplify_config(Int, Bool, Bool, Array[RewriteRequest]) -> SimplifyConfig
pub fn research_simplify_term_concl(@kernel.KernelState, @logic.PropPrelude, Array[(String, @kernel.Term)], @kernel.Term, SimplifyConfig) -> RewriteResult

没有可应用的步骤时返回 NoChange；当需要超过 step_limit 个片段时，诚实失败并报告 “step limit exceeded”；step_limit 为负时报告 “step limit must be non-negative”。

`RewriteResult`

RewriteResult 是一次重写或化简的结果。

pub enum RewriteResult {
  Rewritten(@kernel.Term, ReplayObligation)
  NoChange
  HonestFailure(String)
}

结果是一个项和一条记录，而不是定理：这里没有任何东西证明了重写后的目标。

重放义务

`ReplayStepKind` 和 `research_step_name`

ReplayStepKind 命名一个片段所需的内核级步骤：解析见证、对称性、同余（每个位置步骤一次）、展开定义、β 归约。research_step_name 以字符串形式返回构造子名称。

pub enum ReplayStepKind {
  ResolveWitness
  Symmetry
  Congruence
  Unfold
  BetaNormalize
}

pub fn research_step_name(ReplayStepKind) -> String

`ReplaySegment`、`ReplayObligation` 及其构造函数

片段记录一次重写：请求、重写前后的结论及其步骤。义务把若干片段从第一个结论链接到最后一个结论。

pub struct ReplaySegment {
  request : RewriteRequest
  before_concl : @kernel.Term
  after_concl : @kernel.Term
  steps : Array[ReplayStepKind]
}

pub struct ReplayObligation {
  before_concl : @kernel.Term
  after_concl : @kernel.Term
  segments : Array[ReplaySegment]
}

pub fn research_replay_segment(RewriteRequest, @kernel.Term, @kernel.Term, Array[ReplayStepKind]) -> ReplaySegment
pub fn research_replay_obligation(@kernel.Term, @kernel.Term, Array[ReplaySegment]) -> ReplayObligation

`research_validate_replay_obligation`

research_validate_replay_obligation(state, prelude, locals, obligation) 检查一条义务：用内核规则从每个片段的请求重新构建该片段，并把结果、步骤和链接情况与义务中的记录比较。

pub fn research_validate_replay_obligation(@kernel.KernelState, @logic.PropPrelude, Array[(String, @kernel.Term)], ReplayObligation) -> Result[Unit, @kernel.LogicError]

手工构造或已过期的义务会以 LogicError 失败。

test "rewrite" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  let f = @kernel.mk_var("f", @kernel.fun_ty(bool, bool))
  let locals = [("h", @kernel.mk_eq(p, q).unwrap())]
  // rewrite the argument of f p with h : p = q
  let req = @research_rewrite.research_rewrite_request(
    @research_rewrite.research_local_equality("h"),
    @research_rewrite.research_left_to_right(),
    [@research_rewrite.research_site_comb_arg()],
  )
  guard @research_rewrite.research_rewrite_term_concl(st, pre, locals, @kernel.mk_comb(f, p), req)
    is Rewritten(after, obligation) else {
    fail("expected a rewrite")
  }
  inspect(@kernel.term_to_string(after), content="Comb(Var(f : fun(bool, bool)), Var(q : bool))")
  let steps = obligation.segments[0].steps.map(@research_rewrite.research_step_name)
  inspect(steps.join(", "), content="ResolveWitness, Congruence")
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, locals, obligation) is Ok(_), content="true")
  // without the hypothesis h the obligation does not replay
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, [], obligation) is Err(_), content="true")
}

research_rewrite API

请求

RewriteWitness、ConnectorKind 及其构造函数

RewriteDirection、research_left_to_right 和 research_right_to_left

RewriteSiteStep 及其构造函数

RewriteRequest 和 research_rewrite_request

重写

research_rewrite_term_concl

research_simplify_term_concl 和 SimplifyConfig

RewriteResult