先週の記事（Lean 4に入門する - よーる）でLean 4に入門しました。 私がLean 4を使ってやってみたいことは、浮動小数点数アルゴリズムの性質を示すことと、浮動小数点数演算器の正しさを証明することです。

後者で最近特に気になっているのは、LZA（leading zeros anticipation, 先行ゼロの予測）のアルゴリズムの正しさの検証です。 LZAは高速な浮動小数点数積和演算器の実装に使われるハードウェアアルゴリズムですが（絶対値のLeading Zero Anticipatory (LZA)の勉強 - よーる）、その証明は自明と言えるものではありません。 正しく動作することを上記の記事では「どこかは分からないが、ある桁より上の桁に特定の性質を満たすものがあるはず」のような形で説明しましたが、ビット列の両端のコーナーケースや、何ビット余分に拡張すればいいのかなど、気になる点が複数あります。 そこで、そのような点も含めて、計算機に確認してもらいたいのです。

以下本記事では、まずはLZC（leading zeros count）を定義します。

BitVec

まず、LZCは入力となるビット列の長さに依存する点に注意します。 つまりC++の記法で書けば、leading_zeros_count<uint32_t>(0)は32ですが、leading_zeros_count<uint64_t>(0)は64であるということです。 そのため、符号なし整数（Nat）をそのまま使うのはかなり不便で、「nビットの符号なし整数」のようなものを扱う必要があります。 この目的のため、BitVecを使います。

基本的な使い方

使い方は以下のような感じです。

import Mathlib.Data.BitVec
import Mathlib.Tactic
def a : BitVec 8 := 0x3A
def b : BitVec 8 := 0xA9

example : a &&& b = 0x28 := by decide

よさそうですね。

練習1

ビット演算に関する性質を証明することで、BitVecの使い方に慣れていきます。

example (n : Nat) (a : BitVec n) (b : BitVec n) : a &&& b <= b := by
  induction n
  · cases a <;> rename_i da
    cases b <;> rename_i db
    cases da <;> rename_i qa
    cases db <;> rename_i qb
    cases qa <;> cases qb <;> simp [BitVec.and_self]
  · cases a <;> rename_i da
    cases b <;> rename_i db
    cases da <;> rename_i qa ha
    cases db <;> rename_i qb hb
    simp_all only [le_ofFin, toFin_and]
    cases qa <;> cases qb
    simp

BitVecはFinを使っているようなのですが、はがすのが大変な上、何を使って書き換えればいいのか探すのが本当に大変です。 40分くらいかけてここまでたどりつきましたが、詰まりました。

ChatGPTに聞いたところ、Nat.land_le_rightが使えると教えてくれました。 上で手に入れた書き換えルールを使って書き直したところ、次の正しい証明をすぐに書くことができました。

example (n : Nat) (a : BitVec n) (b : BitVec n) : a &&& b <= b := by
  cases' a with qa ha
  cases' b with qb hb
  simp [le_ofFin, toFin_and, Fin.le_def]
  exact Nat.and_le_right

そもそも、証明の最初の二行は特に意味がないので取り除けます。

example (n : Nat) (a : BitVec n) (b : BitVec n) : a &&& b <= b := by
  simp [le_ofFin, toFin_and, Fin.le_def]
  exact Nat.and_le_right

練習2

足し算に関する性質の証明も、LZAには必須でしょう。 nビット整数とnビット整数を足し合わせると、2ⁿ - 2以下になる、という命題を証明することでBitVecの使い方に慣れていきます。

実際の所、最初に書いた命題は<を使っていて正しくなく、30分ほど溶かしました。 なんでBitVecの<は符号付き比較なのでしょう？ それを直した後、30分ほどで、以下の証明を作ることができました。

example (n : Nat) (a : BitVec n) (b : BitVec n) : ((a.cons false) + (b.cons false)).ult (BitVec.fill (n+1) true) := by
  simp [BitVec.cons, BitVec.allOnes]
  rw [BitVec.add_ofFin]
  simp
  cases' a with qa
  cases' b with qb
  simp
  simp [Fin.add_def]
  simp [BitVec.ult]
  cases' qa with da ha
  cases' qb with db hb
  simp

  have h1 : da + db < 2 ^ (n + 1) - 1 := by
    omega
  have h2 : (da + db) % 2 ^ (n + 1) = da + db := by
    exact Nat.mod_eq_of_lt (by omega)

  rw [h2]
  exact h1

これを簡略化すると、以下のようになりました。

example (n : Nat) (a : BitVec n) (b : BitVec n) : ((a.cons false) + (b.cons false)).ult (BitVec.fill (n+1) true) := by
  simp [BitVec.cons, BitVec.allOnes]
  rw [BitVec.add_ofFin]
  cases' a with qa
  cases' b with qb
  simp [Fin.add_def]
  simp [BitVec.ult]
  cases' qa with da ha
  cases' qb with db hb

  have h : (da + db) % 2 ^ (n + 1) = da + db := by
    exact Nat.mod_eq_of_lt (by omega)

  rw [h]
  omega

補題hを作って即使っているのは無意味そうです。 ChatGPTに聞いたら、Nat.mod_eq_of_ltは等式を返すのでrwの[...]の中に直接かけるよ、と言われました。 これでdaとかdbを使わなくなったので、さらにシンプルになりました。

example (n : Nat) (a : BitVec n) (b : BitVec n) : ((a.cons false) + (b.cons false)).ult (BitVec.fill (n+1) true) := by
  simp [BitVec.cons, BitVec.allOnes]
  rw [BitVec.add_ofFin, Fin.add_def]
  simp [BitVec.ult]
  rw [Nat.mod_eq_of_lt (by omega)]
  omega

依然として、simpとrwの使い方がよくわかりませんし、_defのつくバージョンとつかないバージョンの違いもよくわかりません。

LZC

定義

LZCは次のように定義すればよいでしょう。 BitVecのスライスを作る関数の仕様を調べるのを含めて15分くらいで作ることができました。

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)

ところで、Nat.logで見かけたdecreasing_byはいらなかったんでしょうか？ 原始帰納関数の定義方法に則っているので大丈夫だったのかもしれません（Nat.logの定義は普通ではない帰納法に基づく定義です）。

いきなり高度な定理を証明するのは無理

さて、ここから加算結果のLZCに関する以下の命題を証明しようと思いましたが、30分くらいかけて証明を進めるうちに正しくないことがわかりました。

theorem LZC_of_add_eq_min_LZC {n : Nat} (a b : BitVec n) :
  1 + LZC ((a.cons false) + (b.cons false)) = Nat.min (LZC a) (LZC b) ∨ LZC ((a.cons false) + (b.cons false)) = Nat.min (LZC a) (LZC b)

正しくはこうでしょうか？

theorem LZC_of_add_eq_min_LZC {n : Nat} (a b : BitVec n) :
  1 + LZC ((a.cons false) + (b.cons false)) = Nat.min (LZC (a.cons false)) (LZC (b.cons false))
  ∨ LZC ((a.cons false) + (b.cons false)) = Nat.min (LZC (a.cons false)) (LZC (b.cons false))

これを証明するためにはまず次の補題が必要そうだったので、80分ほど頑張りましたが、→向きを証明したあたりで力尽きました。

theorem lt_LZC_iff_ge {n : Nat} (x : BitVec n) (q : Nat) (hq : q ≤ n)
  : lzc x < q ↔ x.toNat ≥ 2 ^ (n-q) := by

その途中では、使いそうだった以下の定理も証明しましたが、結局使いませんでした。

theorem LZC_le_BitWidth {n : Nat} (x : BitVec n) : LZC x ≤ n := by
  induction n with
  | zero => exact Nat.le_zero.mpr rfl
  | succ m hn => simp [LZC]
                 split
                 · exact Nat.le_add_left 0 _
                 · have h (q : BitVec m): LZC q ≤ m := by bound
                   have h1 : LZC (BitVec.extractLsb' 0 m x) ≤ m := by simp [h]
                   linarith [h1]

boundはhintタクティックで提示されたタクティックで、その内容はよくわかっていません。 BitVec関連の補題を証明するときに、hintで出てくることが多い気がします。

計算的定義と性質に関する定理

少し前に、ライブラリにdecide版とそうでないものが含まれていることを不思議に思ってChatGPTに聞いたことがありました。 その回答には、以下のような部分が含まれており、これに納得しました。

このことを考えると、現状は計算的定義しか存在せず、それが不便を生み出している気がします。 そこで次の、性質に関する命題を証明しましょう。

theorem lzc_eq_iff_msb_prefix {n : Nat} (x : BitVec n) (t : Nat)
  : lzc x = t ↔ x.getMsbD t ∧ (∀s: Nat, s < t → x.getMsbD (s) = false)

この定理の名前はChatGPTに考えてもらいました。

ChatGPTが「個人的には」とか言うので驚きました。

なお、Lean 4では基本はsnake_caseだと言われたので、関数名をlzcに書き換えました。

delta と simp

simp [lzc]とすると定義が展開された上で簡略化が働きます。 この簡略化を嫌ってdelta [lzc]と書いたら、関数の浮動点表示に展開されて途方にくれました。 両者はともに定義の展開を行いますが、再帰関数の場合はそういう違いがあるようです。

LZC 0 のややこしさ

一瞬tに関する帰納法で進めようとしてしまいましたが、lzcの定義的にnに関する帰納法の方が扱いやすそうなのでその方針で進めていきます（ChatGPTもその方針を提示していました）。 というわけでベースケース（n = 0）を証明しようとしましたが、明らかに証明できないことがわかりました。 つまり、先ほど示した命題は間違いであり、正しくは以下のようになるはずです。

theorem lzc_eq_iff_msb_prefix {n : Nat} (x : BitVec n) (t : Nat)
  : lzc x = t ↔ (x = 0 ∧ t = n) ∨ (x.getMsbD t ∧ (∀s: Nat, s < t → x.getMsbD s = false))

LZC 0周りのコーナーケースは良く混乱するところなので、計算機で証明をチェックできることのありがたさを今一度体感しました。

generalizing tが必要

ChatGPTが提示したスケッチを元に証明を進めていたら、以下のような感じになりました。

theorem lzc_eq_iff_msb_prefix {n : Nat} (x : BitVec n) (t : Nat)
  : lzc x = t ↔ (x = 0 ∧ t = n) ∨ (x.getMsbD t ∧ (∀s: Nat, s < t → x.getMsbD s = false)) := by
  apply Iff.intro
  · intro h
    induction n with
    | zero => left
              simp [lzc] at h
              bound
    | succ m ih => right
                   cases hx : x.msb <;> simp [lzc, hx] at h ⊢
                   · have ih' := ih (BitVec.extractLsb' 0 m x) (t-1)

ここで型が合わないというエラーになって途方にくれました。

冷静に考えると、induction n generalizing t withで始めないといけませんでしたね（Natural Number Gameでちゃんと教わります。よくできたカリキュラムです）。 それを解決したらうまくいきました。 帰納法の仮定はこのように使うんですね。

あと、仮定も結論もsimpしたいときは、⊢を使えるんですね。 この記号は見た目通り（？）\|-で入力できます。

帰納法の仮定の引数の型をちゃんと表示してほしいと思いましたが、後になって考えると、∀がついているのが引数なんですね。 ∀で導入された変数は、外側の変数を隠すので、同じ変数名でも外側のものを指しているわけではないので、さらに混乱します。

x ≠ 0 ↔ ∃t, x.getMsbD t

80分ほど頑張りましたが、かなり証明がつらいです。 つらさの原因は、帰納法で示したい命題に∨が出てくるところにあります。 x ≠ 0 ↔ ∃t, x.getMsbD t が成り立つので、∨の右側はx ≠ 0の時にしか成り立たず、つまりここに出てくる∨は実際には排他です。 排他な∨は、証明する分には不便ではありませんが、帰納法の仮定部分で出てくると不便です。 具体的には、x = 0を示したいので∨の左側を取り出したいのですが、このときに∨の右側が成り立たないことを示す必要が出てきます。

x ≠ 0 ↔ ∃t, x.getMsbD tを補題として先に示したほうがよさそうです。 130分かけて以下のように証明しました。 力尽きたので簡略化は行っていません。

theorem forall_lt_testBit_imply_le_two_pow {x : Nat} (p: ∀i ≥ n, Nat.testBit x i = false) : x < 2^n := by
  contrapose! p
  simp_all only [Bool.not_eq_false]
  exact Nat.exists_ge_and_testBit_of_ge_two_pow p

theorem add_shiftRight (a b c : Nat) : a >>> (b + c) = a >>> b >>> c := by
  simp [Nat.shiftRight_add]

lemma lt_of_shiftRight_le_one (a b : Nat) (h : a ≤ b) : a >>> 1 ≤ b >>> 1 := by
  simp [Nat.shiftRight_eq_div_pow]
  exact Nat.div_le_div_right h

theorem lt_of_shiftRight_le (a b : Nat) (h : a ≤ b) : a >>> k ≤ b >>> k := by
  induction k
  case zero => exact h
  case succ m ih =>
    have (x n : Nat) : x >>> (n + 1) = x >>> n >>> 1 := by exact add_shiftRight x n 1
    rw [this] -- repeat rwだと、 x >>> 1 >>> 0 >>> ... >>> 0 >>> n に無限展開されるのでNG
    nth_rewrite 2 [this]
    exact lt_of_shiftRight_le_one (a >>> m) (b >>> m) ih

theorem non_zero_iff_exists_getMsbD {n : Nat} (x : BitVec n)
  : x ≠ 0 ↔ ∃t, x.getMsbD t := by
  by_cases hn : n = 0

  have hx : x = 0 := by bound
  apply Iff.intro
  · intro
    contradiction
  · intro ho
    contrapose! ho
    simp [BitVec.getMsbD]
    omega

  -- n ≠ 0
  apply Iff.intro
  · show x ≠ 0 → ∃t, x.getMsbD t
    intro hx
    have hxn : x.toNat ≠ 0 := by
      intro h0
      apply hx
      exact BitVec.eq_of_toNat_eq h0
    have hxpos : 0 < x.toNat := Nat.pos_of_ne_zero hxn
    have ht : x.toNat ≤ 2^n - 1 := by omega
    have : 2^0 ≤ x.toNat := by linarith
    rcases Nat.exists_ge_and_testBit_of_ge_two_pow this with ⟨k, hk₁, hk₂⟩
    have hk₂' : x.toNat >>> k ≥ 1 := by
      have : x.toNat >>> k % 2 = 1 := by
        simp [Nat.testBit] at hk₂
        exact hk₂
      contrapose! this
      have : x.toNat >>> k = 0 := by
        linarith -- omegaではだめ
      rw [this]
      simp
    have hk₃ : k < n := by
      contrapose! hk₂'
      have hx2 : x.toNat ≤ 2^n - 1 := by omega
      have hl : x.toNat >>> k ≤ (2^n - 1) >>> k := by
        exact lt_of_shiftRight_le x.toNat (2^n - 1) ht
      have : (2^n - 1) >>> k = 0 := by
        simp [Nat.shiftRight_eq_div_pow]
        refine Nat.sub_one_lt_of_le ?_ ?_
        exact Nat.two_pow_pos n
        refine Nat.pow_le_pow_of_le ?_ hk₂'
        decide
      linarith

-- testBit_toNatの定義↓
-- theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl


    use n - 1 - k
    simp [BitVec.getMsbD]
    have : n - 1 - k < n := by omega
    constructor
    · exact this
    · have : n - 1 - (n - 1 - k) = k := by omega
      rw [this]
      simp [BitVec.getLsbD]
      exact hk₂
  · show (∃ t, x.getMsbD t = true) → x ≠ 0
    intro ht
    aesop

x ≠ 0の扱い

結局この補題を証明しましたが、いちいち補題を適用するのすら面倒に感じました。 そこで、あまりきれいではありませんが、証明する定理を以下に切り替えました（x ≠ 0を追加しました）。 必要であれば、x ≠ 0を取り除けばいいでしょう。

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
  induction n generalizing t with
  | zero =>
      apply Iff.intro
      · intro h
        left
        constructor
        · exact hxz
        · simp_all [lzc]
      · intro h
        contrapose! h
        simp [lzc] at h
        tauto
  | succ m ih =>
      apply Iff.intro
      · intro h
        left
        simp [lzc] at h
        have : BitVec.msb x = false := by simp_all only [BitVec.ofNat_eq_ofNat, true_and, ne_eq, not_true_eq_false, BitVec.getMsbD_zero,
  Bool.false_eq_true, implies_true, and_true, and_self, or_false, BitVec.msb_zero, ↓reduceIte, BitVec.extractLsb'_zero]
        simp [this] at h
        set y := BitVec.extractLsb' 0 m x
        have yz : y = 0 := by bound
        have ih' := ih y m
        simp [yz] at ih'
        constructor
        exact hxz
        have : lzc y = m := by bound
        rw [this] at h
        linarith
      · intro h
        simp [hxz] at h
        rw [h]
        simp [lzc]
        have : BitVec.msb x = false := by simp_all only [BitVec.ofNat_eq_ofNat, true_and, ne_eq, not_true_eq_false, BitVec.getMsbD_zero,
  Bool.false_eq_true, implies_true, and_true, and_self, or_false, BitVec.msb_zero, ↓reduceIte, BitVec.extractLsb'_zero]
        simp [this]
        set y := BitVec.extractLsb' 0 m x
        have yz : y = 0 := by bound
        have ih' := ih y m
        simp [yz] at ih'
        have : lzc y = m := by bound
        rw [this]
        exact Nat.add_comm 1 m

  induction n generalizing t with
  | zero =>
      have : x = 0 := by bound
      contradiction
  | succ m ih =>
      apply Iff.intro
      · intro h
        right
        constructor; exact hxz
        simp [lzc] at h
        by_cases hxm : x.msb
        · simp [hxm] at h
          rw [← h]
          simp [BitVec.getMsbD]
          exact Lean.Grind.Bool.eq_true_of_and_eq_true_right hxm
        · set y := BitVec.extractLsb' 0 m x
          have hy : y.cons false = x := by
            simp [y]
            refine BitVec.eq_of_getElem_eq_iff.mpr ?_
            intro i
            by_cases hi : i >= m + 1
            omega
            by_cases hi : i = m
            simp [hi, BitVec.cons]
            simp [BitVec.msb, BitVec.getMsbD] at hxm
            simp [hxm]
            simp [BitVec.append_def]
            have hi : i < m := by omega
            simp [BitVec.cons, BitVec.extractLsb']
            simp [BitVec.append_def]
            simp [hi]
            simp [BitVec.getLsbD]
            exact fun hi => rfl
          simp [hxm] at h
          have ih' := ih y (t-1)
          have hy2 : y ≠ 0 := by
            by_contra!
            rw [this] at hy
            rw [← hy] at hxz
            contrapose! hxz
            simp [BitVec.cons]
          have ih'' := ih' hy2
          have hz : y.getMsbD (t - 1) = true ∧ ∀ s < t - 1, y.getMsbD s = false := by aesop
          constructor
          · rw [← hy]
            simp [BitVec.cons]
            constructor
            · linarith
            · simp [hz]
          · intro s
            intro hs1
            by_cases hs2: s = 0
            · rw [← hy, hs2]
              simp [BitVec.getMsbD, BitVec.cons, BitVec.append_def]
            · contrapose! hz
              intro hy3
              use s-1
              constructor
              · omega
              · rw [← hy] at hz
                simp [BitVec.getMsbD, BitVec.cons, BitVec.append_def] at hz hy3 ⊢
                constructor
                · have : t - 1 < m := by linarith
                  omega
                · have : m - 1 - (s - 1) = m - s := by omega
                  rw [this]
                  tauto
      · intro h
        contrapose! h
        constructor
        intro
        contradiction
        intro
        intro htop
        contrapose! h
        simp [lzc]
        by_cases xmsb: x.msb
        · simp [xmsb]
          have hq : x.getMsbD 0 = true := by
            simp [BitVec.msb] at xmsb
            exact xmsb
          contrapose! hq
          contrapose! h
          have : 0 < t := by omega
          use 0
          constructor
          · exact this
          · exact ne_false_of_eq_true xmsb
        · simp [xmsb]
          set y := BitVec.extractLsb' 0 m x
          have hy : y.cons false = x := by
            simp [y]
            refine BitVec.eq_of_getElem_eq_iff.mpr ?_
            intro i
            by_cases hi : i >= m + 1
            omega
            by_cases hi : i = m
            simp [hi, BitVec.cons]
            simp [BitVec.msb, BitVec.getMsbD] at xmsb
            simp [xmsb]
            simp [BitVec.append_def]
            have hi : i < m := by omega
            simp [BitVec.cons, BitVec.extractLsb']
            simp [BitVec.append_def]
            simp [hi]
            simp [BitVec.getLsbD]
            exact fun hi => rfl
          have ht : t ≠ 0 := by
            by_contra ht
            simp [ht, BitVec.getMsbD, BitVec.msb] at htop xmsb
            exact Std.Tactic.BVDecide.Reflect.Bool.false_of_eq_true_of_eq_false htop xmsb
          have ih' := ih y (t-1)
          have hy2 : y ≠ 0 := by
            by_contra!
            rw [this] at hy
            rw [← hy] at hxz
            contrapose! hxz
            simp [BitVec.cons]
          have ih'' : (lzc y = t - 1 ↔ y = 0 ∧ t - 1 = m ∨ y ≠ 0 ∧ y.getMsbD (t - 1) = true ∧ ∀ s < t - 1, y.getMsbD s = false) := by
            exact ih y (t - 1) hy2
          have ih''' : (y = 0 ∧ t - 1 = m ∨ y ≠ 0 ∧ y.getMsbD (t - 1) = true ∧ ∀ s < t - 1, y.getMsbD s = false) → lzc y = t - 1 := by tauto
          contrapose! ih'''
          constructor
          · right
            constructor
            exact hy2
            constructor
            simp [BitVec.getMsbD, BitVec.getLsbD] at htop ⊢
            constructor
            omega
            have : m-1 - (t-1) = m -t := by omega
            rw [this]
            contrapose! htop
            intro
            rw [← hy]
            simp [BitVec.cons]
            exact eq_false_of_ne_true htop
            contrapose! h
            rw [← hy]
            simp [BitVec.cons]
            contrapose! h
            intro s
            intro hs
            contrapose! h
            use s + 1
            simp
            constructor
            · omega
            · exact eq_true_of_ne_false h
          omega

この証明には230分ほどかかったようです。 同じ補題をコピペで導入しているところもあり、もっと構造化できそうです。

かなり無意味なことをやっている部分がいくつかあります。 仮定に含まれる∧や∨を分解する方法がわからないので、

• ∧であれば、contrapose!してからleftかrightでいらないほうを破棄して、contrapose!でもどす
• ∨であれば、contrapose!してからconstructで自明に成り立たない方（否定形なので自明に成り立つ）を証明して消して、contrapose!でもどす

などとしています。 覚えていることだけでやろうとしている弊害です。（←調べろ）

そもそも、∃や∀が含まれる命題をcontraposeするとものすごく見にくくなるので、それも混乱します。 ちゃんと調べるべきですね。

一方で、∃s<t,とか∀s<tとか→が含まれる命題を本当にcontraposeしたいときは、手でやると間違えるので、計算機が機械的に変形してくれるのはありがたいです。 この辺は、まともに数学の証明を（手で）たくさん書いていれば、息をするように書き換えられるのでしょうけれど……。

他、気づいたことを雑多にまとめます。

• rw??というタクティックを使うと、GUI上で選択した部分を書き換える方法の候補が表示される
• use 0とかやるとゴールにsorryが出てきて混乱するが、改行すると直る
• exactには引数が必要だが、exactと入力した時点で（＝引数がない状態で）赤線も引かれずに終わった感じになるので混乱しがち
• Natの引き算は普通ではない（x < y で x - y = 0となる）のでlinarithでは証明できないことが多い。omegaでも証明できないことが多いが、「普通でない」ケースが発生しないことを補題で証明しておけば、omegaで証明できる。補題の証明自体もomegaでできるので全部omegaだけでできないの？と言う感じだけれど、おそらく何が必要かをこちらから示すのが大事なのだろう
• linarithで証明できてomegaでは証明できないことがある。自然数に関してはlinarithの上位互換のような気がするのだけれど、なぜ？

感想です。

• 証明に詰まったあたりで、どのような補題が必要か考えて、その補題を証明……という風にやっているけれど、成り立たない補題の証明（“ミスパス”）に迷い込んでしまうことがよくある。見通しが極端に悪いので、迷い込んだことが発覚するのもかなり先になる。深さ優先的に突き進むのではなく、やはり全体像を把握して証明のスケッチを作ってから進める方がよさそう
• 今回の命題はx = 0か否かの分岐・induction・iffの三つが絡み合っているが、どの順番で解きほぐせばいいのかがよくわからなかった。x = 0か否かの分岐を先に片付けるのは良かった。inductionを先に使う今回の証明方針は、iffを帰納法の仮定に置ける、つまり仮定が強まるので良いだろうと思ったが、結局逆向きは使わなかった気がするので、取り出すのが面倒になっただけであった。やはり証明のスケッチを書いてから証明に臨むべきである

まとめ

LZAの性質を証明しようと思いましたが、まずはLZC単体の性質を示すだけで時間切れとなりました。