mvcgen
mvcgen は、モナディック(monadic)なプログラムを含むゴールを 検証条件(verification condition) に分解して処理するようなタクティクです。ただしここでいう検証条件とは、do 構文の背景にあるモナドを参照しない部分ゴールのことを指します。1
do 構文を使って手続き的に定義された関数に対して証明を行うことを支援するフレームワークが Lean には組み込まれているのですが、mvcgen はその一部です。
シンプルな使用例として、リストの和を for ループを使って計算する関数が、標準ライブラリに用意されている関数と等しいことを mvcgen を使って証明する例を紹介します。このとき、ループを回しても変わらずに成り立ち続ける 不変条件(invariant) を指定することに注意してください。
import Lean
-- mvcgen はまだ使用しないでというwarningを消す
set_option mvcgen.warning false
variable {α : Type} [Zero α] [Add α]
variable [@Std.Associative α (· + ·)] [@Std.LawfulIdentity α (· + ·) 0]
/-- for文を使って命令的に実装された、和を計算する関数 -/
@[grind]
def sumDo (l : List α) : α := Id.run do
let mut out := 0
for i in l do
out := out + i
return out
-- 証明の中で必要になる補題
@[grind =, simp]
theorem List.sum_append_singleton {l : List α} {x : α} :
(l ++ [x]).sum = l.sum + x := by
induction l with simp_all <;> grind
-- `scoped` で用意された表記法を有効にする
open Std.Do
/-- 手続き的に実装した和の計算と、標準ライブラリに用意されている`List.sum`関数が等しい -/
theorem sumImp_eq_sumFunc (l : List α) : sumDo l = List.sum l := by
-- モナディックに実装されている（`Id.run do ...`）部分にフォーカスする
generalize h : sumDo l = s
apply Id.of_wp_run_eq h
-- 検証条件に分解する
mvcgen
-- ループ全体を通して成り立たせたい不変条件を指定する
-- * `out` は `let mut` で導入した変数の現在値を表す
-- * `xs` は `List.Cursor` で，リストを接頭辞 `xs.prefix` と接尾辞 `xs.suffix` に
-- 分割して表すデータ構造。どこまでループが進んだかを追跡する。
-- つまり進捗（ループの到達位置）を記録する。
-- 不変条件は「`out` が接頭辞の総和を保持している」こと。
-- 記法 `⌜p⌝` は，純粋な命題 `p : Prop` をアサーション言語に埋め込む。
case inv1 => exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝
-- `mleave` はある決まった `simp` 補題に対する `simp only [...] at *` の糖衣構文。
all_goals mleave
-- 各反復で不変条件が保たれることを示す
case vc1.step pref cur suff hyp b ih =>
-- 与えられているリストは
-- * `pref`: for 文で既に処理された部分
-- * `cur`: 今回処理する要素
-- * `suff`: まだ処理されていない残りの部分
-- に分割されているという仮定がある。
guard_hyp hyp :ₛ l = pref ++ cur :: suff
-- そして今まで処理された部分に関しては不変条件が成り立っているという帰納法の仮定がある
guard_hyp ih :ₛ pref.sum = b
-- このとき、現在の要素 `cur` を処理した後でも不変条件が成り立つことを示せばよい
guard_target =ₛ (pref ++ [cur]).sum = b + cur
-- 証明そのものは `grind` で終わる
grind
-- ループ開始時に不変条件が成り立つことを示す
case vc2.a.pre =>
-- 空リストの和が 0 であることを示せばよい
guard_target =ₛ ([] : List α).sum = 0
grind
-- ループ終了時の不変条件から目標の性質が従うことを証明する
case vc3.a.post.success result hr =>
-- ループ終了時には「処理された部分」は全体なので、
-- 不変条件から次が成りたつ
guard_hyp hr :ₛ l.sum = result
-- したがって目標も成り立つ
grind
構文
mvcgen タクティクを使用するとき、まず不変条件を指定し、そのあとに all_goals mleave を実行するというパターンがよく見られます。そこで、定型文を減らすために以下のように mvcgen invariants という構文が用意されています。
import Std.Tactic.Do
set_option mvcgen.warning false
open Std.Do
/-- 素朴に実装されたべき乗関数 -/
def naiveExpo (x n : Nat) : Nat := Id.run do
let mut result := 1
for _ in [:n] do
result := result * x
return result
theorem naiveExpo_correct (x n : Nat) : naiveExpo x n = x ^ n := by
generalize h : naiveExpo x n = r
apply Id.of_wp_run_eq h
mvcgen invariants
-- 不変条件を指定する
-- ここでは`xs`がループの進捗を表していて、
-- `xs.prefix.length`はこれまでにループが回った回数を表す
-- `result`はループ内で更新される変数の値を表す
· ⇓⟨xs, result⟩ => ⌜result = x ^ xs.prefix.length⌝
with simp_all <;> grind -- すべてのゴールに対して `mleave` に加えて `simp_all <;> grind` を適用してみる
機能
早期リターン
for 文の途中で return 文があるような場合でも、mvcgen は対応できます。その場合は不変条件の書き方が変わって、「早期終了した場合」と「早期終了せず継続する場合」の２つを考慮する必要が生じます。
import Lean
open Std.Do
set_option mvcgen.warning false
variable {α : Type} [Hashable α] [DecidableEq α]
/-- リストに重複がないか判定する。
true なら重複がない。false なら重複がある。-/
def nodupDo (l : List α) : Bool := Id.run do
let mut seen : Std.HashSet α := ∅
for x in l do
if x ∈ seen then
return false
seen := seen.insert x
return true
/-- `nodupDo` の結果は標準ライブラリに用意されている `Nodup` と一致する -/
theorem nodup_correct (l : List α) : nodupDo l ↔ l.Nodup := by
generalize h : nodupDo l = r
apply Id.of_wp_run_eq h
mvcgen invariants
· Invariant.withEarlyReturn
-- forループの１ステップが平常終了したとき。
-- プログラム中の可変変数`seen`は、現在までに見た要素の集合`xs.prefix`に等しく、
-- かつ`xs.prefix`は重複がない。
(onContinue := fun xs seen => ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝)
-- 早期リターンしたとき。
-- 返り値は`false`であり、かつ`l`に重複がある
(onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
with grind
break 文
for ループを途中で抜ける構文としては return 文のほかに break 文もあります。break 文に対しては retrun 文のように不変条件を指定する方法がそれ専用に用意されていはいないため、不変条件に工夫が必要になります。具体的には、通常通りループが終了した場合でも break で抜けた場合でも成り立つような不変条件を考える必要があります。
以下は、takeWhile 関数を早期リターンと break のそれぞれを使って実装し、それぞれの不変条件を比較する例です。2
import Lean
open Std.Do
variable {α : Type}
/-- `takeWhile` を命令型スタイルで実装したもの。
`return` 文を使うバージョン。
（ただし、`result ++ [x]` の部分が非効率的で、あまり高速ではない）
-/
def takeWhileReturn (p : α → Bool) (l : List α) : List α := Id.run do
let mut result := []
for x in l do
if ! p x then
return result
result := result ++ [x]
return result
set_option mvcgen.warning false
@[grind =, simp]
theorem takeWhile_simplify_false (P : α → Bool) (pref suff : List α) (cur : α) (h : P cur = false) :
List.takeWhile P (pref ++ cur :: suff) = List.takeWhile P pref := by
fun_induction List.takeWhile with simp_all
@[grind =>]
theorem takeWhile_eq_self_iff_all (P : α → Bool) (l : List α) :
List.takeWhile P l = l ↔ l.all P := by
fun_induction List.takeWhile with simp_all
theorem takeWhileReturn_spec (p : α → Bool) (l : List α) :
takeWhileReturn p l = l.takeWhile p := by
generalize h : takeWhileReturn p l = r
apply Id.of_wp_run_eq h
mvcgen invariants
· Invariant.withEarlyReturn
(onContinue := fun cursor result =>
⌜result = cursor.prefix ∧ result = cursor.prefix.takeWhile p⌝)
(onReturn := fun ret result => ⌜ret = result ∧ result = l.takeWhile p⌝)
with grind
/-- `takeWhile` を命令型スタイルで実装したもの。
`break` 文を使うバージョン。-/
def takeWhileBreak (p : α → Bool) (l : List α) : List α := Id.run do
let mut result := []
for x in l do
if ! p x then
break
result := result ++ [x]
return result
theorem takeWhileBreak_spec (p : α → Bool) (l : List α) :
takeWhileBreak p l = l.takeWhile p := by
generalize h : takeWhileBreak p l = r
apply Id.of_wp_run_eq h
mvcgen invariants
· ⇓⟨cursor, result⟩ =>
-- `return` を使うものと比較すると、不変条件に `cursor.suffix = []` が追加されている。
-- これは `break` でループを抜けた場合にも成り立つようにするための工夫
⌜(cursor.suffix = [] ∨ result = cursor.prefix) ∧ result = cursor.prefix.takeWhile p⌝
with grind
continue 文
continue 文がある場合も break 文の場合と同様で、continue で抜けた場合でも通常終了した場合でも常に成り立つような不変条件を考えて指定します。
import Lean
variable {α : Type}
/-- `continue` 文を使って実装した `Array.filter` -/
def Array.filterDo (p : α → Bool) (l : Array α) : Array α := Id.run do
let mut res : Array α := #[]
for x in l do
if ! p x then
continue
res := res.push x
return res
-- 証明のための補題を用意する
attribute [grind =] Array.toList_inj
attribute [grind _=_] Array.toList_filter
open Std.Do
set_option mvcgen.warning false
theorem Array.filterDo_spec (p : α → Bool) (l : Array α) :
l.filterDo p = l.filter p := by
generalize h : l.filterDo p = r
apply Id.of_wp_run_eq h
mvcgen invariants
· ⇓⟨cursor, res⟩ => ⌜res.toList = cursor.prefix.filter p⌝
with grind
複数の可変変数
for ループの中で複数の可変変数が let mut で導入されている場合には、以下のように不変条件の書き方を変えることで対応できます。3
import Lean
open Std.Do
/-- フィボナッチ数列の仕様 -/
@[grind]
def fibSpec (n : Nat) : Nat :=
match n with
| 0 => 0
| 1 => 1
| k + 2 => fibSpec (k + 1) + fibSpec k
/-- 手続き的に実装された、フィボナッチ数列の実装 -/
def fibImpl (n : Nat) : Nat := Id.run do
if n = 0 then
return 0
let mut b := 1
let mut a := 0
for _i in [1:n] do
let a' := a
a := b
b := a' + b
return b
-- `mvcgen` はまだ安定していないという警告を消す
set_option mvcgen.warning false
theorem fibImpl_eq_fibSpec (n : Nat) : fibImpl n = fibSpec n := by
generalize h : fibImpl n = r
apply Id.of_wp_run_eq h
mvcgen invariants
-- 不変条件の指定。
-- `a` と `b` はループ内で更新される可変変数。
-- `let mut` で定義された順番ではなくて、アルファベット順に拘束されることに注意。
-- `cursor.pos` はループの進捗を表していて、いままでにループが回った回数を表す。
· ⇓⟨cursor, a, b⟩ => ⌜a = fibSpec cursor.pos ∧ b = fibSpec (cursor.pos + 1)⌝
with grind
二重のforループ
for ループがネストしていても mvcgen は対応できます。その場合は、外側のループと内側のループそれぞれについて不変条件を指定する必要があります。また、内側のループの不変条件において、外側のループの進捗状況に言及することができます。
import Lean
open Std.Do
-- `α` は加法的な可換モノイドであると仮定する
variable {α : Type} [Add α] [Zero α]
variable [@Std.Associative α (· + ·)] [@Std.LawfulIdentity α (· + ·) 0]
variable [@Std.Commutative α (· + ·)]
/-- 二重リストに対する和を計算する、関数型スタイルで定義された関数 -/
@[grind]
def doubleSum (l : List (List α)) : α :=
l.foldr (fun xs acc => acc + xs.sum) 0
/-- 二重リストに対する和を計算する、命令型スタイルで定義された関数 -/
def doubleSumDo (l : List (List α)) : α := Id.run do
let mut result := 0
for sublist in l do
for x in sublist do
result := result + x
return result
set_option mvcgen.warning false
@[grind =, simp]
theorem List.sum_append_singleton {l : List α} {x : α} :
(l ++ [x]).sum = l.sum + x := by
induction l with simp_all <;> grind
/-- `doubleSum` は `append` を和に変換する -/
@[grind =]
theorem doubleSum_append {l1 l2 : List (List α)} :
doubleSum (l1 ++ l2) = doubleSum l1 + doubleSum l2 := by
induction l1 with grind
theorem doubleSum_spec (l : List (List α)) : doubleSumDo l = doubleSum l := by
generalize h : doubleSumDo l = r
apply Id.of_wp_run_eq h
mvcgen invariants
-- 外側のループについての不変条件。
-- `cursor.prefix` はこれまでに外側の`for`ループで見てきた部分を指している
· ⇓⟨cursor, result⟩ => ⌜result = doubleSum cursor.prefix⌝
-- 内側のループについての不変条件。
· ⇓⟨cursor, result⟩ => by
expose_names -- すべての死んだ変数に名前を付ける
-- `pref` は外側のループで今まで見てきた部分を表していて、
-- `l = pref ++ (cur :: suff)` が成り立つ。
guard_hyp h_1 :ₛ l = pref ++ cur :: suff
-- `cursor` は内側のループの進捗を表している。
exact ⌜result = doubleSum pref + (cursor.prefix).sum⌝
with grind
使用例
インデックスアクセスを使った和の計算
配列やリストに対するインデックスアクセスを使用して書かれたプログラムについて、仕様を検証する例を紹介します。
import Lean
variable {α : Type} [Add α] [Zero α]
/-- 配列に対するインデックスアクセスを使用して和を計算する関数 -/
def Array.sumDo (arr : Array α) : α := Id.run do
let mut out := 0
for hi : i in [0:arr.size] do
out := out + arr[i]
return out
-- α は加法的な可換モノイド
variable [@Std.Associative α (· + ·)] [@Std.LawfulIdentity α (· + ·) 0]
variable [@Std.Commutative α (· + ·)]
theorem List.sum_append_singleton {l : List α} {x : α} :
(l ++ [x]).sum = l.sum + x := by
induction l with (simp_all; grind only)
@[grind =, simp]
theorem Array.sum_append_singleton (arr : Array α) (a : α) :
(arr ++ #[a]).sum = arr.sum + a := by
simp [← sum_eq_sum_toList, List.sum_append_singleton]
@[grind =]
theorem Array.extract_stop_add_one {α : Type} {arr : Array α} {i j : Nat}
(hj : j < arr.size) (hij : i ≤ j) :
arr.extract i (j + 1) = arr.extract i j ++ #[arr[j]] := by
simp only [append_singleton, push_extract_getElem, Nat.min_eq_left, hij]
open Std.Do
set_option mvcgen.warning false
/-- `Array.sumDo` は配列の要素の和を正しく計算する -/
theorem Array.sumDo_eq_sum (arr : Array α) : arr.sumDo = arr.sum := by
generalize h : arr.sumDo = r
apply Id.of_wp_run_eq h
mvcgen invariants
· ⇓⟨cursor, out⟩ => ⌜(arr.take cursor.pos).sum = out⌝
with (simp_all <;> grind)
農民の掛け算
農民の掛け算は、２で割る操作と２倍する操作と足し算だけで掛け算を行うアルゴリズムです。mvcgen を使って、このアルゴリズムが正しいことを証明する例を紹介します。4
import Lean
set_option mvcgen.warning false
open Std.Do
/-- 農民の掛け算。２で割る操作と２倍する操作と足し算だけで掛け算を行う -/
def peasantMul (x y : Nat) : Nat := Id.run do
let mut curX := x
let mut curY := y
let mut prod := 0
for _ in [0:x] do
if curX % 2 = 1 then
prod := prod + curY
curX := curX / 2
curY := curY * 2
if curX = 0 then
break
return prod
attribute [grind =] Nat.div_div_eq_div_mul
@[grind ->]
theorem div2_mul2_odd (x : Nat) (odd : x % 2 = 1) : x = (x / 2) * 2 + 1 := by
grind
@[grind ->]
theorem div2_mul2_even (x : Nat) (even : x % 2 = 0) : x = (x / 2) * 2 := by
grind
@[grind =, simp]
theorem div_pow_self_two_eq_zero (n : Nat) : n / 2 ^ n = 0 := by
have : n < 2 ^ n := Nat.lt_two_pow_self
simp_all
example (x y : Nat) : peasantMul x y = x * y := by
generalize h : peasantMul x y = s
apply Id.of_wp_run_eq h
mvcgen invariants
· ⇓⟨cursor, curX, curY, prod⟩ =>
⌜curX = x / 2 ^ cursor.pos ∧ curX * curY + prod = x * y⌝
with (simp at * <;> grind)
繰り返し自乗法による指数計算
繰り返し自乗法(binary exponentiation)は、x ^ n を計算する際に指数部を２冪の和に分解することで計算を高速化するアルゴリズムのことです。mvcgen を使って、このアルゴリズムが正しいことを証明する例を紹介します。5
import Lean
/-- 繰り返し自乗法で自然数の指数計算を行う -/
def binaryExpo (root n : Nat) : Nat := Id.run do
let mut x := root
let mut y := 1
let mut e := n
for _ in [0:n] do
if e % 2 = 1 then
y := x * y
e := e - 1
else
x := x * x
e := e / 2
if e = 0 then
break
return y
open Std.Do
set_option mvcgen.warning false
@[grind =]
theorem Nat.Grind.pow_zero {n a : Nat} (h : a = 0) : n ^ a = 1 := by
simp_all
@[grind =]
theorem Nat.pow_mul_self_halve_of_even (x e : Nat) (he : e % 2 = 0) :
(x * x) ^ (e / 2) = x ^ e := calc
_ = (x ^ 2) ^ (e / 2) := by grind
_ = x ^ (2 * (e / 2)) := by grind [Nat.pow_mul]
_ = x ^ e := by grind
@[grind! ·]
theorem Nat.mul_pow_sub_one_of_odd (x e : Nat) (he : e % 2 = 1) :
x * x ^ (e - 1) = x ^ e := calc
_ = x ^ (1 + (e - 1)) := by grind
_ = x ^ e := by congr; grind
theorem binaryExpo_spec (root n : Nat) :
binaryExpo root n = root ^ n := by
generalize h : binaryExpo root n = r
apply Id.of_wp_run_eq h
mvcgen invariants
-- 不変条件の指定。
-- ローカル可変変数は定義順ではなくアルファベット順に拘束されることに注意。
· ⇓⟨cursor, e, x, y⟩ => ⌜y * x ^ e = root ^ n ∧ e + cursor.pos ≤ n⌝
with grind
先頭から足して和が0未満になる時点があるか判定する
整数のリストに対して、前から順に足していったときに和が0未満になる瞬間があるかチェックする関数について仕様を証明する例を紹介します。6
import Std.Tactic.Do
/-- `operations : List Int` を先頭から順に足していったときに、
どこかの時点で合計値が 0 未満になることがあるか判定する -/
def belowZero (operations : List Int) : Bool := Id.run do
let mut balance := 0
for op in operations do
balance := balance + op
if balance < 0 then
return true
return false
namespace List
variable {α : Type}
/-- リスト `l` の先頭からある部分までを取り出せば述語 `P : List α → Prop` が成り立つ -/
def HasPrefix (P : List α → Prop) (l : List α) : Prop := ∃ n, P (l.take n)
/-- `HasPrefix` の定義を言い換えるだけの定義 -/
theorem hasPrefix_iff {P : List α → Prop} {l : List α} :
l.HasPrefix P ↔ ∃ n, P (l.take n) := by
simp [HasPrefix]
/-- 空リストの接頭辞は自分しかない -/
@[simp, grind =]
theorem hasPrefix_nil {P : List α → Prop} : [].HasPrefix P ↔ P [] := by
simp [hasPrefix_iff]
/-- 空リストに対して成り立つなら、接頭辞に対しても成り立つ -/
@[simp, grind =>]
theorem hasPrefix_of_nil {P : List α → Prop} {l : List α} (h : P []) : l.HasPrefix P := by
exists 0
/-- 全体に対して成り立つなら、接頭辞に対しても成り立つ -/
@[simp, grind =>]
theorem hasPrefix_of_all {P : List α → Prop} {l : List α} (h : P l) : l.HasPrefix P := by
exists l.length
simpa
@[grind =]
theorem hasPrefix_cons {P : List α → Prop} {a : α} {l : List α} :
(a :: l).HasPrefix P ↔ P [] ∨ l.HasPrefix (fun l' => P (a :: l')) := by
constructor
· intro ⟨n, hn⟩
by_cases nzero : n = 0
· simp_all
· right
exists n - 1
suffices a :: take (n - 1) l = take n (a :: l) from by
simp_all
grind [take_cons]
· rintro (h | ⟨⟨n, hn⟩⟩)
· grind
· exists n + 1
@[grind =]
theorem hasPrefix_append {P : List α → Prop} {l l' : List α} :
(l ++ l').HasPrefix P ↔ l.HasPrefix P ∨ l'.HasPrefix (fun l'' => P (l ++ l'')) := by
induction l generalizing P with grind
@[grind =]
theorem sum_append_singleton {α : Type} {l : List α} {x : α}
[Add α] [Zero α] [@Std.Associative α (· + ·)] [@Std.LawfulIdentity α (· + ·) 0] :
(l ++ [x]).sum = l.sum + x := by
induction l with simp_all <;> grind
end List
open Std.Do
set_option mvcgen.warning false
theorem belowZero_iff {l : List Int} : belowZero l ↔ l.HasPrefix (fun l => l.sum < 0) := by
generalize h : belowZero l = res
apply Id.of_wp_run_eq h
mvcgen invariants
-- 早期終了がある場合の不変条件
· Invariant.withEarlyReturn
-- 早期終了しなかった場合、現在の接頭辞の和が `balance` に等しく、
-- かつ「今までループで見てきた部分」は「和が0未満になる接頭辞」を持たない
(onContinue := fun cursor balance =>
⌜balance = cursor.prefix.sum ∧ ¬ cursor.prefix.HasPrefix (fun l => l.sum < 0)⌝)
-- 早期終了した場合、返り値の`ret`は`true`であり、かつ和が0未満になる接頭辞がある
(onReturn := fun ret balance => ⌜ret = true ∧ l.HasPrefix (fun l => l.sum < 0)⌝)
with grind
-
このページの内容およびコード例は、公式のドキュメントである Verifying imperative programs using mvcgen を参考にしています。 ↩
-
このコード例は Lean の公式 Zulip の new monadic program verification framework というトピックにおける Sebastian Graf さんの投稿を参考にしました。 ↩
-
このコード例は、Lean のリポジトリの doLogicTests.lean の内容を参考にしました。 ↩
-
このコード例は Lean の公式 Zulip の new monadic program verification framework というトピックにおける pandaman さんの投稿を参考にしました。 ↩
-
このコード例は Lean の公式 Zulip の new monadic program verification framework というトピックにおける Aaron Liu さんの投稿を参考にしました。 ↩
-
このコード例は human-eval-lean のコードを参考にしています。 ↩