上下文系统 - inline-function/Sublimation GitHub Wiki

上下文系统与自动证明

把"断言"写进类型，交给编译器自动证明——这是凝华最核心的卖点。证明通过的代码才给编译，失败即编译错误。

一句话原理

函数/结构体可以携带命题：

fun f(x: Nat)<x > 0>: Nat <$ >= 0> = x + 1
//            └── 上文（调用前必须满足）
//                              └── 下文（调用后保证成立，$ = 返回值）
  • 上文：调用 f 前，编译器必须证明 x > 0。证不出 → E-PRE-UNPROVEN。
  • 下文：调用 f 后，编译器把 f的返回值 >= 0 注入后续上下文。

伴生命题

每个"调用"都有一个伴生命题：f<实参> 成立意味着"这一调用的下文已兑现"。

fun halve(n: Nat)<n % 2 = 0>: Nat = n / 2
// halve(10) 的伴生命题是 halve<10> → 10 % 2 = 0 已被证明

自然命题

编译器自动注入的事实，你不需要手写：

触发 自动注入
var n = 0 n : Nat、n = 0、n ≥ 0
n 是 Nat 类型参数/字段 n ≥ 0
纯函数 f pure<f>
结构体实例 u self = u、各字段 
fun demo(n: Nat, m: Nat) {
    ∴ n ≥ 0                 // 自然命题：Nat 参数自动有 n ≥ 0
    ∴ m ≥ 0
}

因为 / 又因为 / 所以

∵ p        // "因为"：证明 p 成立后注入 Γ（用于后续推导）
+∵ p       // "又因为"：验证 p 在上下文中成立后注入 Γ（否则 E-CANNOT-PROVE）
∴ q        // "所以"：求证 q，证不出即 E-CANNOT-PROVE

+∵ 3 >= 0                // 常量折叠：3 >= 0 直接判定为真 → 注入
∴ 3 >= 0                 // 求证：成立
var r = 3 + 1
∴ r = 4                  // 常量归约：r=3+1 → 4

数学记号

源码直接写：∈ ≥ ≤ = ≠、∀、∃、n ∈ (0..30)。

+∵ n ∈ (0..30)
∴ n ≥ 0                 // 命中定理 rangeLowerBound

自动证明器能干什么

编译器内置 10 通道自动证明器，按顺序尝试：

  1. 常量折叠（1+1=2、2<3）
  2. 单变量边界（0 ≤ x ≤ 5 → x ≥ 0）
  3. 差分约束（x ≤ y, y ≤ z → x ≤ z）
  4. 等式传递/对称/代换
  5. 合取/蕴含/否定/矛盾爆炸
  6. 构造子同余（a=b → Some(a)=Some(b)）
  7. 自定义命题展开（def p<…> ↔ …）
  8. 类型判定（x : Nat）
  9. 排中律/双否/逆否（经定理库）
  10. 全称引入（∀ n. n = n）

常见工程场景能做到自动覆盖；非线性算术、德摩根变形、∃! 唯一性等数学证明题不自动证（报错要求人工）。

定理函数 @theorem

标注 @theorem 的函数是定理：编译器擦除它，只供证明位使用。

@theorem
fun leqRefl[a]: Null <a <= a>

预置定理库（stdlib/ 自动挂载）：logic.subl（区间下界、≤传递、合取左件右件、MP 等 10 条）+ classic.subl（排中律、双重否定、逆否 3 条）。

结构体伴生命题

结构体也能携带命题，构造时证明：

struct PosPoint(x: Nat, y: Nat)<x > 0, y > 0>

var p = PosPoint(1, 2)      // 自动证明 1>0 且 2>0 → ✅
// var q = PosPoint(0, 2)   // 证不出 0>0 → 编译错误 E-STRUCT-PROP-UNPROVEN

关键规则

  • 上下文里的表达式必须是纯的（证明系统不处理副作用）。
  • 证不出 → 编译错误并列出尝试过的定理；绝不悄悄放行。
  • 需要绕过时用 unchecked（显式逃逸）。
⚠️ **GitHub.com Fallback** ⚠️