17.4. 为单子启用 `mvcgen`🔗

如果单子基于 Lean 标准库提供的单子变换器实现，例如 ExceptT 和 StateT，那么它通常不需要额外的实例。其他单子则需要 WP、LawfulMonad 和 WPMonad 实例。该策略旨在支持对可能中断、带状态的单线程控制进行建模的单子；换言之，即普通命令式编程中的各种效应。更奇特的效应尚未得到研究。

提供基本实例后，下一步是证明一个充分性引理。该引理应表明：运行单子计算并断言所需谓词时的最弱前置条件，确实足以证明该谓词。

除单子的定义外，典型的库还会提供一组原语运算符。每个原语都应配备一个规约引理。此外，将状态内部实现设为私有，并导出一组精心设计的断言运算符，可能也很有用。

库中原语运算符的规约引理最好给出这些运算符作为谓词变换器的精确规约。尽管按运算符如何将输入状态变换为输出状态来思考往往更容易，但当后置条件完全自由时，验证条件生成会更加可靠。这使自动化能够用下一条语句的确切前置条件来实例化后置条件，而无须证明一个蕴涵。换言之，把前置条件规定为后置条件之函数的规约，在实践中优于仅仅关联前置条件与后置条件的规约。

模式后置条件

函数 double 将自然数状态翻倍：

def double : StateM Nat Unit := do
  modify (2 * ·)

按时间顺序思考，一个合理的规约是输出状态的值为输入状态值的两倍。这使用一个代表初始状态的模式变量来表达：

theorem double_spec :
    ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := byn:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ double ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄
  simp [double]n:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ modify fun x => 2 * x ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄
  mvcgen with grindAll goals completed! 🐙

然而，若将后置条件视为模式变量，可得到一个等价的规约；在其他函数中使用 double 时，它会产生更小的验证条件：

@[spec]
theorem better_double_spec {Q : PostCond Unit (.arg Nat .pure)} :
    ⦃ fun s => Q.1 () (2 * s) ⦄ double ⦃ Q ⦄ := byQ:PostCond Unit (PostShape.arg Nat PostShape.pure)⊢ ⦃fun s => Q.fst () (2 * s)⦄ double ⦃Q⦄
  simp [double]Q:PostCond Unit (PostShape.arg Nat PostShape.pure)⊢ ⦃fun s => Q.fst () (2 * s)⦄ modify fun x => 2 * x ⦃Q⦄
  mvcgen with grindAll goals completed! 🐙

后置条件的第一个投影是其有状态断言。现在，前置条件只说明后置条件应当对初始状态的两倍成立。

在线查看 ↪

日志单子

单子 LogM 在计算期间维护一份只可追加的日志：

structure LogM (β : Type u) (α : Type v) : Type (max u v) where
  log : Array β
  value : α

instance : Monad (LogM β) where
  pure x := ⟨#[], x⟩
  bind x f :=
    let { log, value } := f x.value
    { log := x.log ++ log, value }

它还有一个 LawfulMonad 实例。

可以用 log 写入日志，并用 LogM.run 计算值及其相应日志。

def log (v : β) : LogM β Unit := { log := #[v], value := () }

def LogM.run (x : LogM β α) : α × Array β := (x.value, x.log)

WP 实例没有从头编写，而是使用 PredTrans.pushArg。该运算符原本用于建模状态单子，但 LogM 可以视为一个只能向状态追加内容的状态单子。这种追加体现在实例主体中：初始状态会与操作产生的日志相拼接：

instance : WP (LogM β) (.arg (Array β) .pure) where
  wp
    | { log, value } =>
      PredTrans.pushArg (fun s => PredTrans.pure (value, s ++ log))

WPMonad 实例同样受益于这一状态单子的概念模型，证明十分简短：

instance : WPMonad (LogM β) (.arg (Array β) .pure) where
  wp_pure x := byα:Type ?u.5σ:List (Type u)ps:PostShapex✝:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20x:α✝⊢ wp (pure x) = pure x
    extα:Type ?u.5σ:List (Type u)ps:PostShapex✝:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20x:α✝Q✝:PostCond α✝ (PostShape.arg (Array β) PostShape.pure)s✝:Array β⊢ (wp⟦pure x⟧ Q✝ s✝).down ↔ ((pure x).apply Q✝ s✝).down
    simp [wp, pure]All goals completed! 🐙

  wp_bind _ _ := byα:Type ?u.5σ:List (Type u)ps:PostShapex:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20β✝:Type ?u.20x✝¹:LogM β α✝x✝:α✝ → LogM β β✝⊢ (wp do
    let a ← x✝¹
    x✝ a) =
  do
  let a ← wp x✝¹
  wp (x✝ a)
    extα:Type ?u.5σ:List (Type u)ps:PostShapex:PredTrans ps αy:PredTrans ps αQ:Assertion psβ:Type ?u.20α✝:Type ?u.20β✝:Type ?u.20x✝¹:LogM β α✝x✝:α✝ → LogM β β✝Q✝:PostCond β✝ (PostShape.arg (Array β) PostShape.pure)s✝:Array β⊢ (wp⟦do
        let a ← x✝¹
        x✝ a⟧
      Q✝ s✝).down ↔
  ((do
          let a ← wp x✝¹
          wp (x✝ a)).apply
      Q✝ s✝).down
    simp [wp, bind]All goals completed! 🐙

充分性引理有一个重要细节：最弱前置条件变换的结果被应用于空数组。这是必要的，因为日志计算被建模为只可追加的状态，因此必须存在某个初始状态。从语义上说，选择空数组才不会把并非来自程序的项放入日志；从技术上说，它还必须是与数组追加运算符可交换的值。

theorem LogM.of_wp_run_eq {x : α × Array β} {prog : LogM β α}
    (h : LogM.run prog = x) (P : α × Array β → Prop) :
    (⊢ₛ wp⟦prog⟧ (⇓ v l => ⌜P (v, l)⌝) #[]) → P x := byα:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P x
  rw [← hα:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P prog.run]α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]) → P prog.run
  intro h'α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Proph':⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun v l => ⌜P (v, l)⌝) #[]⊢ P prog.run
  simp [wp] at h'α:Type u_1β:Type u_1x:α × Array βprog:LogM β αh:prog.run = xP:α × Array β → Proph':P (prog.value, prog.log)⊢ P prog.run
  exact h'All goals completed! 🐙

接下来，应为库中的每个运算符提供规约引理。这里只有一个运算符：log。对于新的单子，这些证明往往必须突破霍尔三元组和最弱前置条件的抽象边界；它们提供的规约随后可由库的客户端抽象地使用。

theorem log_spec {x : β} :
    ⦃ fun s => ⌜s = s'⌝ ⦄ log x ⦃ ⇓ () s => ⌜s = s'.push x⌝ ⦄ := byβ:Types':Array βx:β⊢ ⦃fun s => ⌜s = s'⌝⦄ log x ⦃PostCond.noThrow fun x_1 s => ⌜s = s'.push x⌝⦄
  simp [log, Triple, wp]All goals completed! 🐙

log 的更好规约使用模式后置条件：

variable {Q : PostCond Unit (.arg (Array β) .pure)}

@[spec]
theorem log_spec_better {x : β} :
    ⦃ fun s => Q.1 () (s.push x) ⦄ log x ⦃ Q ⦄ := byβ:TypeQ:PostCond Unit (PostShape.arg (Array β) PostShape.pure)x:β⊢ ⦃fun s => Q.fst () (s.push x)⦄ log x ⦃Q⦄
  simp [log, Triple, wp]All goals completed! 🐙

函数 logUntil 会记录不超过某个界限的所有自然数，其所得日志的长度总是等于它的参数：

def logUntil (n : Nat) : LogM Nat Unit := do
  for i in 0...n do
    log i

theorem logUntil_length : (logUntil n).run.2.size = n := byn:Nat⊢ (logUntil n).run.snd.size = n
  generalize h : (logUntil n).run = xn:Natx:Unit × Array Nath:(logUntil n).run = x⊢ x.snd.size = n
  unfold logUntil at hn:Natx:Unit × Array Nath:(do
      forIn (0...n) PUnit.unit fun i __s => do
          log i
          pure (ForInStep.yield PUnit.unit)
      pure ()).run =
  x⊢ x.snd.size = n
  apply LogM.of_wp_run_eq hn:Natx:Unit × Array Nath:(do
      forIn (0...n) PUnit.unit fun i __s => do
          log i
          pure (ForInStep.yield PUnit.unit)
      pure ()).run =
  x⊢ ⊢ₛ
  wp⟦do
      forIn (0...n) PUnit.unit fun i __s => do
          log i
          pure (ForInStep.yield PUnit.unit)
      pure ()⟧
    (PostCond.noThrow fun v l => ⌜(v, l).snd.size = n⌝) #[]
  mvcgen invariants
  · ⇓⟨xs, _⟩ s => ⌜xs.pos = s.size⌝
  with
    simp_all [List.Cursor.pos]All goals completed! 🐙 <;>
    grind [Std.PRange.Nat.size_rco, Std.Rco.length_toList]

在线查看 ↪

17.4. 为单子启用 mvcgen🔗

17.4. 为单子启用 `mvcgen`🔗