Luna Flow
简体中文

research_rewrite 教程

本教程运行 research_rewrite 包的重写原型：用局部等式重写一个子项，检查记录下来的重放义务，并化简一个联结词应用。该包仅用于研究，不属于发行的 prover，因此只用来做实验，不要在其上构建。

快速开始

在 moon.pkg 中导入这些包：

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/logic",
  "Luna-Flow/QED/research_rewrite",
}

用局部假设 h : p = q 把 f p 重写为 f q：

test "quick start" {
  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())]
  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()], // the argument of f p
  )
  match @research_rewrite.research_rewrite_term_concl(st, pre, locals, @kernel.mk_comb(f, p), req) {
    Rewritten(after, _) => inspect(@kernel.term_to_string(after), content="Comb(Var(f : fun(bool, bool)), Var(q : bool))")
    _ => fail("expected a rewrite")
  }
}

请求指明等式（按名称指定的局部变量）、方向，以及要替换的子项的路径。

日常任务

检查重放义务

每次重写都附带其背后内核步骤的记录。验证会重建这些步骤；若它们依赖的上下文缺失，则失败：

test "obligation" {
  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())]
  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(_, obligation) else {
    fail("expected a rewrite")
  }
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, locals, obligation) is Ok(_), content="true")
  inspect(@research_rewrite.research_validate_replay_obligation(st, pre, [], obligation) is Err(_), content="true")
}

化简联结词

research_simplify_term_concl 展开联结词常量并进行 β 规范化，直到不再变化：

test "simplify" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let not_p = @kernel.mk_comb(@kernel.ks_mk_const(st, "not").unwrap(), p) // the constant `not` applied to p
  let cfg = @research_rewrite.research_simplify_config(10, true, true, [])
  match @research_rewrite.research_simplify_term_concl(st, pre, [], not_p, cfg) {
    Rewritten(after, obligation) => {
      inspect(@kernel.term_alpha_eq(after, @logic.prop_mk_not(st, pre, p).unwrap()), content="true")
      inspect(obligation.segments.length(), content="1")
    }
    _ => fail("expected a simplification")
  }
  // a variable has nothing to simplify
  inspect(@research_rewrite.research_simplify_term_concl(st, pre, [], p, cfg) is NoChange, content="true")
}

查看诚实失败

不支持的请求会说明失败原因：

test "failures" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let not_p = @kernel.mk_comb(@kernel.ks_mk_const(st, "not").unwrap(), p)
  // a step limit of 0 allows no segment
  let tight = @research_rewrite.research_simplify_config(0, true, true, [])
  match @research_rewrite.research_simplify_term_concl(st, pre, [], not_p, tight) {
    HonestFailure(msg) => inspect(msg, content="step limit exceeded")
    _ => fail("expected a failure")
  }
  // the path asks for an abstraction where there is an application
  let req = @research_rewrite.research_rewrite_request(
    @research_rewrite.research_beta_normalization(),
    @research_rewrite.research_left_to_right(),
    [@research_rewrite.research_site_abs_body()],
  )
  match @research_rewrite.research_rewrite_term_concl(st, pre, [], not_p, req) {
    HonestFailure(msg) => inspect(msg, content="rewrite site expected a lambda abstraction")
    _ => fail("expected a failure")
  }
}

进一步使用

用定理重写。 research_explicit_theorem(th) 把任意等式定理用作见证，例如来自 @logic.logic_eq_sym 的定理。与 research_right_to_left() 组合可向另一方向重写。

链接多个请求。 把若干请求放入 SimplifyConfig.rewrite_requests；每一轮应用匹配的请求，义务为每个已应用的步骤记录一段。

阅读研究笔记。 设计和晋升闸门位于 research/rewrite-simplify/；research_rewrite 设计概述了晋升还缺少什么。

常见陷阱

  • 指望得到定理。 重写返回一个项和一个义务。没有任何东西证明原始目标。
  • 在 λ 之下重写。 AbsBody 位置会被拒绝。
  • 折叠定义。 CanonicalUnfold 和 BetaNormalization 只能从左到右工作。
  • 依赖该包。 它仅用于研究，可能变更或被移除。

后续步骤