先週（Lean 4 で LZA の証明（その1） - よーる）はLean 4でLZCの定義と性質を結ぶ定理を証明しましたが、全く洗練されていなかったので、証明を簡潔化しました。
定義（再掲）
def lzc {n : Nat} (x : BitVec n) : Nat :=
if x.msb then 0 else
match n with
| 0 => 0
| Nat.succ m => 1 + lzc (BitVec.extractLsb' 0 m x)
補題1
xのMSBが0の時、xのMSB以外を切り出したものを0と連結すると、xと同じになるという定理です。
lemma cons_false_exctartLsb'_eq {n : Nat} {x : BitVec (n+1)} (hxm: ¬x.msb)
: x = (BitVec.extractLsb' 0 n x).cons false := by
refine BitVec.eq_of_getElem_eq_iff.mpr ?_ -- 各ビットが一致することで証明する
intro i
simp [BitVec.cons, BitVec.append_def]
by_cases hi : i >= n + 1
· -- x の上位ビットは自明に false
bound
by_cases hi : i = n
· -- 仮定 hxm（x.msb = false）より成り立つ
simp [BitVec.msb, BitVec.getMsbD] at hxm
simp [hi, hxm, BitVec.cons, BitVec.append_def]
have hi : i < n := by omega
-- 下の方のビットは自明に一致
simp [hi]
bound
補題2
s≧mの時、n+mビット整数xに対して、xのMSB側sビット目と、xの下nビットを切り出したもののs-mビット目が、一致するという定理です。
-- 使いたいのは m = 1 の時だけれど、一般的な場合を証明
lemma getMsbD_eq_getMsbD_extractLsb' {n s m : Nat} (x : BitVec (n+m)) (hs : s ≥ m)
: x.getMsbD s = (BitVec.extractLsb' 0 n x).getMsbD (s-m) := by
simp [BitVec.getMsbD]
by_cases hs1 : s < n + m
· have hs2 : s - m < n := by omega
have hs3 : n + m - 1 - s = n - 1 - (s - m) := by omega
have hs4 : n - 1 - (s - m) < n := by omega
simp [hs1, hs2, hs3, hs4]
· simp [hs1]
omega
補題3
x≠0のMSBが0の時、xのMSB以外を切り出したものをyとして、y≠0であるという定理です。 補題1の結果を中で使っているため、使用する側で補題1を呼び出さなくて済むよう、ペアで返すようにしました。
lemma lzc_eq_iff_msb_prefix_lemma_induction {n : Nat} {x : BitVec (n+1)} (hxm : ¬x.msb) (hxz : x ≠ 0)
: x = (BitVec.extractLsb' 0 n x).cons false ∧ (BitVec.extractLsb' 0 n x) ≠ 0 := by
set y := BitVec.extractLsb' 0 n x
have hxy : x = y.cons false := cons_false_exctartLsb'_eq hxm
have hy : y ≠ 0 := by
contrapose! hxz
rw [hxz] at hxy
simpa [hxz, BitVec.cons, BitVec.extractLsb'] using hxy
exact ⟨hxy, hy⟩
LZCの性質に関する定理
theorem lzc_eq_iff_msb_prefix {n : Nat} (x : BitVec n) (t : Nat)
: lzc x = t ↔ (x = 0 ∧ t = n) ∨ (x ≠ 0 ∧ x.getMsbD t ∧ (∀s: Nat, s < t → x.getMsbD s = false)) := by
by_cases hxz : x = 0
· subst hxz
induction n generalizing t with
| zero =>
simp [lzc]
bound
| succ m ih =>
have ih' := ih m
simp at ih' -- lzc 0#m = m
simp [lzc]
bound
apply Iff.intro
· show lzc x = t → _
induction n generalizing t with
| zero =>
have : x = 0 := by bound
contradiction
| succ m ih =>
intro h
right -- ∨ の右側が成り立つので証明する
refine ⟨hxz, ?_⟩ -- ∧ の左側（x ≠ 0）は前提 hxz により成立
show x.getMsbD t = true ∧ ∀ s < t, x.getMsbD s = false -- 本体である ∧ の右側を証明する
by_cases hxm : x.msb <;> simp [lzc, hxm] at h
· -- x.msb = true の時、t = lzc x = 0 を使って示す
simp [BitVec.msb] at hxm -- x.msb = x.getMsbD 0
bound -- ∧ の左は代入で自明。右は空虚な真
· -- x.msb = false の時、1 + lzc y = t を使って示す
obtain ⟨hxy, hy⟩ := lzc_eq_iff_msb_prefix_lemma_induction hxm hxz
set y := BitVec.extractLsb' 0 m x
have ih' := ih y (t - 1) -- 帰納法の仮定を y と t - 1 で使う
have ih'' := ih' hy (show lzc y = t - 1 from by omega) -- hy の適用後、仮定を使った書き換え
cases ih''; itauto; rename_i ih'' -- ∨ の左側が成り立たないことを示して ∨ の右側を得る
replace ih'' := ih''.right -- ∧ の左側（y ≠ 0）は hy と重複しているので捨てる
constructor
· -- x の t 番目に 1 が立っている ← y の t - 1 番目に 1 が立っている
exact
Std.Tactic.BVDecide.Reflect.Bool.lemma_congr
(y.getMsbD (t - 1))
(x.getMsbD t)
(getMsbD_eq_getMsbD_extractLsb' x (show t ≥ 1 from by omega))
ih''.left
· intro s hs1
by_cases hs2 : s = 0
· -- こちら向きだけで証明しないといけない単純な事実
simpa [hs2, BitVec.msb] using hxm -- s = 0 の時は仮定 hxm（¬x.msb）で示す
· -- x の s 番目が 0 ← y の s - 1 番目が 0
rw [
getMsbD_eq_getMsbD_extractLsb' x (show s ≥ 1 from by omega)]
exact ih''.right (s - 1) (by omega)
· show _ → lzc x = t
induction n generalizing t with
| zero =>
have : x = 0 := by bound
contradiction
| succ m ih =>
intro h
cases h; itauto; rename_i h -- ∨ の左側が成り立たないことを示して ∨ の右側を得る
replace h := h.right -- ∧ の左側（x ≠ 0）は前提 hxz と重複しているので捨てる
guard_hyp h : x.getMsbD t = true ∧ ∀ s < t, x.getMsbD s = false -- 本体である ∧ の右側の仮定を使う
by_cases hxm : x.msb <;> simp [lzc, hxm]
· -- x.msb = true の時、t = lzc x = 0 を示す
by_contra
simp [BitVec.msb] at hxm -- x.msb = x.getMsbD 0
exact Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false hxm (h.right 0 (by omega))
· -- x.msb = false の時、1 + lzc y = t を示す
obtain ⟨hxy, hy⟩ := lzc_eq_iff_msb_prefix_lemma_induction hxm hxz
set y := BitVec.extractLsb' 0 m x
have ih' := ih y (t - 1) -- 帰納法の仮定を y と t - 1 で使う
-- こちら向きだけで証明しないといけない単純な事実
have ht : t ≠ 0 := by -- 仮定 h（x.getMsbD t）と hxm（¬x.msb）が矛盾するため t = 0 はありえない
contrapose! hxm
simpa [hxm, BitVec.msb] using h
apply (show lzc y = t - 1 → 1 + lzc y = t from by omega) -- ゴールを書き換え
refine ih' hy ?_ -- hy の適用後、ゴール側へ移動
right -- ∨ の左側は成り立たないので ∨ の右側を示す
refine ⟨hy, ?_⟩ -- ∧ の左側（y ≠ 0）は hy により成立
constructor
· -- x の t 番目に 1 が立っている → y の t - 1 番目に 1 が立っている
exact
Std.Tactic.BVDecide.Reflect.Bool.lemma_congr
(x.getMsbD t)
(y.getMsbD (t - 1))
(Eq.symm (getMsbD_eq_getMsbD_extractLsb' x (show t ≥ 1 from by omega)))
h.left
· intro s hs1
-- x の s + 1 番目が 0 → y の s 番目が 0
rw [show s = s + 1 - 1 from rfl,
Eq.symm (getMsbD_eq_getMsbD_extractLsb' x (show s + 1 ≥ 1 from by simp))]
exact h.right (s + 1) (by omega)
この証明は以下のように構成されています。
2の証明と3の証明は、非常に似通ったものになっています（2の証明を見ながら3の証明を書いたので）。 証明を左右に並べて、対応づくように適宜改行を入れてみると、一目瞭然です。
前回の証明と異なり、→向きの証明と←向きの証明を分離したことで見通しが良くなった気がします。 それでも結局x=0の部分は使わなくて証明するときの荷物になっているだけなので、「x=0 → lzc x = t ↔ A」と「x≠0 → lzc x = t ↔ B」の二つの定理を証明したほうが見通しが良かったですね。 この辺のどういった命題を証明するべきものとして立てるかは、普通のプログラミングで何を関数とするかと同様、たくさん練習することで覚えていくしかなさそうです。
ちなみに証明をきれいにするのにかかった時間は、10時間20分でした。
→方向の証明は元の証明を見ながら書き直して、←方向の証明は元の証明は無視して→方向の証明をコピペして修正する形で書きました。
その過程で、重複した証明を補題に追い出しました。
最後の方は対応づくように順番を入れ替えとか、一画面に収まるように簡略化とか、そういったことをやっていたので、証明をきれいにするのにかかった正味の時間は9時間くらいでしょう。
あとは、∧を分解する方法（.leftと.right）、∨を分解する方法（cases）、∃を使う方法（obtain）、∀を証明する方法（intro）、即席で定理を作る方法（show ... from by omega）、仮定をsimpしてゴールと一致させて証明を終える方法（simpa ... using ...）あたりを覚え（勉強しなおし？）ました。
まとめ
今週はコスサミとかあって忙しかったので、証明をきれいにするだけでおしまいでした（このブログが公開される時間には私はきっと電車に乗っているでしょう）。
