kernel 教程

本教程直接使用 kernel 包的原始规则证明定理。读完后，你将能构造带类型的项，从十条原语推导出等式对称性等新规则，声明和定义常量，并理解为什么定理不能比其常量的含义存活更久。你不需要 parser 或 prover 包；这里的一切都是纯 MoonBit。

快速开始

把 QED 加入你的模块，并在使用它的包的 moon.pkg 中导入内核：

moon add Luna-Flow/QED@0.1.0

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

最小的证明只需一条规则：REFL 证明任意项等于自身。

test "quick start" {
  let st = @kernel.empty_kernel_state()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let th = @kernel.refl_checked(st, p).unwrap()
  inspect(
    @kernel.thm_to_string(th),
    content="[] |- Comb(Comb(Const(= : fun(bool, fun(bool, bool))), FVar(p : bool)), FVar(p : bool))",
  )
}

输出为 $\vdash p = p$：没有假设（[]），结论是把等号常量 =（类型为 $\mathit{bool} \to \mathit{bool} \to \mathit{bool}$）作用于两个 p。thm_to_string 打印内核实际使用的 De Bruijn 形式，因此自由变量显示为 FVar。

每条规则的第一个参数都是 KernelState。空状态知道类型 bool、ind 和 fun，以及内置等号和选择常量 @。

日常任务

构建项并进行类型检查

项用 mk_var、mk_comb、mk_abs 和 mk_eq 构建；在你请求其类型或在规则中使用该项之前，不做任何检查。

test "build terms" {
  let a = @kernel.mk_tyvar("A")
  let f = @kernel.mk_var("f", @kernel.fun_ty(a, a))
  let x = @kernel.mk_var("x", a)
  let fx = @kernel.mk_comb(f, x)
  inspect(@kernel.hol_type_to_string(@kernel.type_of(fx).unwrap()), content="A")
  // λx. f x has type A -> A
  let lam = @kernel.mk_abs(x, fx)
  inspect(@kernel.hol_type_to_string(@kernel.type_of(lam).unwrap()), content="fun(A, A)")
  // f applied to itself is ill-typed
  inspect(@kernel.type_of(@kernel.mk_comb(f, f)) is None, content="true")
  // α-equivalence ignores the name of the bound variable
  let y = @kernel.mk_var("y", a)
  inspect(@kernel.term_alpha_eq(lam, @kernel.mk_abs(y, @kernel.mk_comb(f, y))), content="true")
}

使用假设

ASSUME 引入一个假设，EQ_MP 利用命题之间的等式把证明从一侧移到另一侧。二者合起来证明 $\{p = q, p\} \vdash q$。

test "hypotheses" {
  let st = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  let th_eq = @kernel.assume_checked(st, @kernel.mk_eq(p, q).unwrap()).unwrap() // {p = q} |- p = q
  let th_p = @kernel.assume_checked(st, p).unwrap() // {p} |- p
  let th_q = @kernel.eq_mp_checked(st, th_eq, th_p).unwrap() // {p = q, p} |- q
  inspect(@kernel.thm_hyp_count(th_q), content="2")
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_q).unwrap()), content="Var(q : bool)")
  // EQ_MP checks that the second theorem proves the left-hand side
  inspect(@kernel.eq_mp_checked(st, th_eq, th_eq) is Err(@kernel.AlphaMismatch), content="true")
}

推导等式的对称性

内核没有对称性规则。它是可推导的，推导过程展示了如何由原语构建更大的规则。由 $\Gamma \vdash s = t$：

$$\begin{aligned} &\vdash (=) = (=) && \textsf{REFL} \\ &\Gamma \vdash (=)\,s = (=)\,t && \textsf{MK\_COMB} \text{ with the premise} \\ &\Gamma \vdash (s = s) = (t = s) && \textsf{MK\_COMB} \text{ with } \vdash s = s \\ &\Gamma \vdash t = s && \textsf{EQ\_MP} \text{ with } \vdash s = s \end{aligned}$$

fn sym(st : @kernel.KernelState, th : @kernel.Thm) -> @kernel.Thm raise @kernel.LogicError {
  let (s, _) = @kernel.dest_eq(@kernel.thm_concl(th).unwrap_or_error()).unwrap_or_error()
  let ty = @kernel.type_of(s).unwrap()
  let eq = @kernel.mk_const("=", @kernel.fun_ty(ty, @kernel.fun_ty(ty, @kernel.bool_ty())))
  let refl_eq = @kernel.refl_checked(st, eq).unwrap_or_error()
  let th1 = @kernel.mk_comb_rule_checked(st, refl_eq, th).unwrap_or_error()
  let refl_s = @kernel.refl_checked(st, s).unwrap_or_error()
  let th2 = @kernel.mk_comb_rule_checked(st, th1, refl_s).unwrap_or_error()
  @kernel.eq_mp_checked(st, th2, refl_s).unwrap_or_error()
}

test "derived symmetry" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let th = @kernel.assume_checked(st, @kernel.mk_eq(x, y).unwrap()).unwrap() // {x = y} |- x = y
  let flipped = sym(st, th) // {x = y} |- y = x
  let (l, r) = @kernel.dest_eq(@kernel.thm_concl(flipped).unwrap()).unwrap()
  inspect(@kernel.term_to_string(l) + " = " + @kernel.term_to_string(r), content="Var(y : A) = Var(x : A)")
  inspect(@kernel.thm_hyp_count(flipped), content="1")
  // a premise that is not an equation makes sym raise
  let not_eq = @kernel.assume_checked(st, @kernel.mk_var("p", @kernel.bool_ty())).unwrap()
  let r = try sym(st, not_eq) catch { e => Err(e) } noraise { th => Ok(th) }
  inspect(r is Err(@kernel.NotAnEquality), content="true")
}

unwrap_or_error 把 Err 变成抛出的 LogicError，因此当前提不是等式时，sym 会以 NotAnEquality 干净地失败。每个中间定理都由内核检查；sym 本身无需信任。logic 包以 logic_eq_sym 提供了这条规则。

用 β 归约和抽象进行计算

BETA 证明可约式等于其收缩结果，ABS 则在绑定变量不在任何假设中自由出现时，把等式提升到绑定子之下。

test "beta and abs" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let k = @kernel.mk_abs(x, @kernel.mk_abs(y, x)) // λx. λy. x
  // BETA: (λx. λy. x) y = λ_. y; the inner binder is renamed, not captured
  let th = @kernel.beta_rule_checked(st, @kernel.mk_comb(k, y)).unwrap()
  let (_, rhs) = @kernel.dest_eq(@kernel.thm_concl(th).unwrap()).unwrap()
  inspect(@kernel.term_to_string(rhs), content="Abs(Var(_b0 : A), Var(y : A))")
  // ABS over x: |- λx. x = λx. x from |- x = x
  let th_abs = @kernel.abs_rule_checked(st, x, @kernel.refl_checked(st, x).unwrap()).unwrap()
  inspect(@kernel.thm_hyp_count(th_abs), content="0")
  // but not over a variable that a hypothesis mentions
  let th_h = @kernel.assume_checked(st, @kernel.mk_eq(x, y).unwrap()).unwrap()
  inspect(@kernel.abs_rule_checked(st, x, th_h) is Err(@kernel.VarFreeInHyp), content="true")
}

声明常量并留意作用域

常量存在于带作用域的签名中。定理会记录它的每个常量指向哪个声明，内核拒绝在当前生效的并非该声明的地方使用它。

test "scopes" {
  let st0 = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let st1 = @kernel.ks_add_const(st0, "c", bool).unwrap()
  let c = @kernel.ks_mk_const(st1, "c").unwrap()
  let th = @kernel.refl_checked(st1, c).unwrap() // |- c = c, about c#1
  // an inner scope declares another c
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "c", bool).unwrap()
  inspect(@kernel.thm_is_admissible(st2, th), content="false")
  inspect(@kernel.trans_checked(st2, th, th) is Err(@kernel.InvalidInstantiation), content="true")
  // after popping the scope the theorem is usable again
  let st3 = @kernel.ks_pop_scope(st2).unwrap()
  inspect(@kernel.trans_checked(st3, th, th) is Ok(_), content="true")
}

定义常量

定义同时引入一个常量及其定义定理。闸门检查该定义不会使理论不一致。

test "define" {
  let st0 = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let x = @kernel.mk_var("x", bool)
  let (st1, def_th) = @kernel.ks_define_const_thm(
    st0,
    "id_bool",
    @kernel.fun_ty(bool, bool),
    @kernel.mk_abs(x, x),
  ).unwrap()
  // |- id_bool = λx. x
  let (lhs, _) = @kernel.dest_eq(@kernel.thm_concl(def_th).unwrap()).unwrap()
  inspect(@kernel.term_to_string(lhs), content="Const(id_bool#1 : fun(bool, bool))")
  // the definition is recorded for audit
  let (gate, heads, _) = @kernel.ks_extension_cert_at(st1, 0).unwrap()
  inspect(gate is @kernel.DefOK && heads == ["id_bool"], content="true")
  // a right-hand side with a free variable is refused
  inspect(@kernel.ks_define_const(st0, "bad", bool, x) is Err(@kernel.DefinitionNotClosed), content="true")
}

进一步使用

把派生规则构建为函数。 上面的 sym 是所有派生规则的模式：一个由定理到定理的 MoonBit 函数，调用原始规则并传播其错误，方式是返回 Result 或用 unwrap_or_error 抛出。logic 包就是这类函数的库：logic_eq_sym、logic_apply_fun_eq、logic_beta_normalize_eq，以及 logic API 中的命题规则。你自己的规则也这样写，就无需为可靠性审查它们，只需考虑其用处。

实例化。 INST_TYPE 和 INST 把一般定理特化。对类型变量 A 证明的定理，在状态所允许的每个类型上都成立：

test "instantiate" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let th = @kernel.refl_checked(st, x).unwrap() // |- x = x  at A
  let th_bool = @kernel.inst_type(st, [("A", @kernel.bool_ty())], th).unwrap()
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  let x_bool = @kernel.mk_var("x", @kernel.bool_ty())
  let th_p = @kernel.inst_checked(st, [(x_bool, p)], th_bool).unwrap() // |- p = p
  inspect(@kernel.term_alpha_eq(@kernel.thm_concl(th_p).unwrap(), @kernel.mk_eq(p, p).unwrap()), content="true")
  // a type the state does not know is refused
  let bad = @kernel.inst_type(st, [("A", @kernel.mk_tyapp("nat", []))], th)
  inspect(bad is Err(@kernel.InvalidInstantiation), content="true")
}

扩展理论。 ks_register_type_definition 由现有类型的非空子集添加新类型，ks_specify_const 在给出见证的情况下添加由某性质刻画的常量。两者都在 kernel API 页面中展示。请保留扩展之前的状态：ks_conservative_replay_ok(base, extended, th) 检查扩展之后证明、但以旧语言陈述的定理是否仍是旧理论的定理。

处理错误。 所有失败都是 LogicError 或 SigError 的值。用 is 匹配它们以应对特定失败，或在会抛出 LogicError 的函数中用 unwrap_or_error 传播。

向上一层。 逐条规则地写证明是内核被测试的方式，而不是证明本应被书写的方式。tactics 教程从目标反向工作，prover 教程则运行由这里所示规则检查的定理脚本。

常见陷阱

• 结构化地比较项。 从定理读回的项带有生成的绑定名，如 _b0。请用 term_alpha_eq 比较，常量标识可能不同时用 term_logical_eq，切勿使用 term_to_string。
• 用 mk_const 构建常量。 mk_const 使常量保持未解析，规则会拒绝状态中未声明的常量（TypeMismatch）。请使用 ks_mk_const 或 ks_mk_const_instance，它们从状态取得标识和模式。等号常量 = 是例外：它是内置的。
• 在另一类型下复用绑定名。 mk_abs(mk_var("x", A), mk_var("x", B)) 在 De Bruijn 边界被拒绝（BoundaryFailure）。请使用不同的名称。
• 跨状态使用定理。 定理针对传给每条规则的状态进行检查。遮蔽某常量之后，关于外层常量的旧定理会以 InvalidInstantiation 失败，直到该作用域被弹出。
• 假设非命题。 ASSUME、ADD_ASSUM 和 EQ_MP 需要 bool 类型的项；否则返回 NotBoolTerm。
• 以为 unwrap 是安全的。 示例为简洁起见使用 unwrap。库代码应对 Result 进行匹配。

后续步骤

• kernel API 列出每个函数及其确切的失败情形。
• kernel 设计解释了这些规则为何可靠，以及定理类型为何是抽象的。
• logic 教程在内核之上构建命题联结词。
• 形式化规范是每条规则的规范性定义。