以下の内容はhttps://lpha-z.hatenablog.com/entry/2025/07/20/231500より取得しました。

Lean 4に入門する

Lean 4は、定理証明支援系の一つで、純粋関数型言語でもあります。 先週浮動小数点数ルーチンの誤差解析をやって、計算機の言いなりになるのではなく自分でちゃんと証明ができたら（そしてその正しさを計算機で検証できたら）いいなと思ったので、定理証明支援系の勉強をはじめることにしました。 最も有名な定理証明支援系はおそらくCoqで（名前がRocqに変わってからは有名なんでしょうか？）、FlocqやGappaなどの浮動小数点数周りのライブラリもよく整備されている印象があります。 でも、Xで以下のポストが流れてきたので、これでLean 4を少し勉強しました。

以下、全然まとまっていないですが、初心者がどんなところで詰まっているのかみたいなものの資料になっていればいいと思って、うまくいかなかった点を含めてそのまま書いています。

Natural Number Game

手を動かして勉強したいと思ったので、Natural Number Gameをやってみました（フェルマーの最終定理以外は全部証明しました）。 複数のゴールができたり、タクティックを使って証明していく、というのは知っていたので、それほど驚きがあったわけではありませんでした。

第一印象としては、とにかくがちゃがちゃやっていると証明できてしまうということでした。 遠回りかつ無意味な場合分けや無意味な数学的帰納法を使った証明ができてしまっていることは感覚的に明らかでした。 実際、証明完了後に「たったこれだけで証明できるよ！」みたいな解説が出てくるのですが、到底それを思いつけると思いませんでした。 とにかく知っている定理をrwで使いまくって自明な形に帰着して直に証明する、という形になりがちで、定理が使える形に近づけて証明するという一般的な証明とかけ離れたものになってしまいます。 補題の名前がわかりづらく、補題の一覧も見づらいのが原因かもしれません。 いずれにせよ、証明を賢く作っているというよりは、証明の探索（ペアノ算術の論理的帰結は枚挙可能）をやらされているという、計算機と立場が逆転しているような感覚がありました。

もう一つの印象は、知っているタクティックだけを使って証明を進めがちで勉強にならない、ということでした。 どの形の時にはどのタクティックが有効、みたいなのを覚えていないと使えないわけですが、覚えているタクティックだけ使ってしまって遠回りな証明を完成させてばかりでした。 最後の方はtautoを連打すると証明が完成するといった感じで、どういう証明が行われているかわからない、でも計算機が正しいと言っているならいいんだろう――というこれまた本末転倒な感覚がありました。

以下のようなポストも見たので、本格的なところを触っていないのが原因ということもあるでしょう。 あまり深入りせず、次に進むことにします。 浮動小数点数の命題を証明する時も、全称型・高階型・依存型などはあまり使わなさそうですが。 ライブラリでは型レベル関数くらいまでは普通に使われているので、それくらいは読めないといけないですね。 そもそも、(x : ℚ) (hx: x > 0) : x ≧ 0とか書いた時点で、引数xの値に応じて後続の引数hxや返り値の型が変わる（hxの宇宙レベル（Sort）はPropだけれど、型はTrueもしくはFalse）ので、これが依存型になっているようです。 関数の引数の宇宙レベルが統一されていなかったりする（普通の型と命題では宇宙レベルが異なる）のが気になりましたが、これは高階型とは別の軸でしょう。

Flean

Lean 4のmathlib4（コミュニティ主導の事実上の標準ライブラリ、らしい→ChatGPT - Mathlib4の位置づけ）にはFloat（binary64）やFloat32（binary32）というのが含まれています。 しかし、ビット表現が直書きで指数部と仮数部の幅が決め打ちだったりするなど、「浮動小数点数」の性質を証明することには役立たなそうに思いました。 Fleanという、浮動小数点数の性質を証明することに役立ちそうなライブラリがあるので、これを使ってみました。

開発環境のセットアップ

IDE（統合開発環境）がないと話にならなさそうなので、Visual Studio Codeをインストールして、Lean 4をセットアップしました。 バージョン違いの問題があったようですが、以下のようなlakefileをつくればいいとChatGPTに教えてもらいました。

name = "Foo"
version = "0.1.0"
defaultTargets = ["Foo"]

[[require]]
name = "batteries"
git  = "https://github.com/leanprover-community/batteries"
rev  = "v4.16.0"

[[require]]
name = "mathlib"
git  = "https://github.com/leanprover-community/mathlib4"
rev  = "v4.16.0"

[[require]]
name = "flean"
git  = "https://github.com/josephmckinsey/Flean"
rev  = "main"

[[lean_lib]]
name = "Foo"

Fleanに入門

手始めに何か定理を証明してみようと思ったのですが、想像をはるかに超える大変さがあることがわかりました。 最初に書いた定理（証明ではない）は以下の感じでした。 まず、何を引数として与えないといけないのかがよくわからない感じで大変でした……。

import Flean
import Flean.Rounding

open Flean
open FloatCfg
open scoped Real

#check to_float

example {x y : ℚ}
    (hx : (to_float (C := DoubleCfg) (R := round_near) x).IsFinite)
    (hy : (to_float (C := DoubleCfg) (R := round_near) y).IsFinite)
    (h1 : y / 2 ≤ x)
    (h2 : x ≤ 2 * y) :
    to_rat (to_float (C := DoubleCfg) (R := round_near) (x-y)) =
        (to_rat (to_float (C := DoubleCfg) (R := round_near) x))
        -  (to_rat (to_float (C := DoubleCfg) (R := round_near) y)) := by sorry

関数の定義

たくさん同じようなコードが出てくるので、まとめました。 あと、open scoped RealはChatGPTが除算のために必要だとか言ってきたので書いていたのですが、いらなさそうだったので消しておきました。 また、定理を証明するのに必要だと思ったので、指数部を取り出す部分関数を書いてみました（というかChatGPTにどうやって書いたらいいのって聞きまくりました）。 assertとかするのではなく、契約プログラミングみたいなことができるのはうれしいですね。

import Flean
import Flean.FloatCfg
import Flean.Rounding

open Flean
open FloatCfg
open RoundingMode

def round_near : Rounding := ⟨nearest⟩
def fp64_config : FloatCfg := { prec := 53, emin := -1022, emax := 1023, emin_lt_emax := by decide, prec_pos := by decide }
def to_fp64 := to_float (C := fp64_config) (R := round_near)
def round_fp64 := fun x => to_rat (to_fp64 x)

def get_exp {C : FloatCfg} (f : Float C) (hf : f.IsFinite) : ℤ := by
    cases f with
    | inf _ => cases hf
    | nan => cases hf
    | normal f _ _ => exact f.e
    | subnormal _ _ => exact C.emin

テスト

さて、この関数が正しいのかテストしようと思いました。 テストはexampleとしてコード内に書けるのもうれしい感じです。

まず、#eval to_rat (to_fp64 2.5)とかやってみましたが挙動が変です。 どうも、precは53ではなくて2^53と書かないといけなかったようです（かなり後になってDoubleCfgの定義を覗いたら2^52が正しかったようですが、まぁ二冪が必要ということです）。

引数として必要な証明を作る

この関数を呼び出すためにはまず、f.IsFiniteの証明を作る必要があります。 しかしながら、これが大仕事でした。 90分くらいかけて、以下の証明を作ることができました。 ChatGPTがなければこれを作ることすら不可能だったでしょうが、かなり幻覚だらけなのでなかなか大変です。 あと、ゴールがFalseだとか仮定にFalseがあるだとか、その辺がこんがらがってわけわからなくなっていました。

import Flean
import Flean.FloatCfg
import Flean.Rounding
import Mathlib.Tactic

open Flean
open FloatCfg
open RoundingMode
open Mathlib.Tactic

def round_near : Rounding := ⟨nearest⟩
def fp64_config : FloatCfg := { prec := 2^53, emin := -1022, emax := 1023, emin_lt_emax := by decide, prec_pos := by decide }
def to_fp64 := to_float (C := fp64_config) (R := round_near)
def round_fp64 := fun x => to_rat (to_fp64 x)

example : (to_fp64 5).IsFinite := by
  cases h : to_fp64 5 with
  | inf s =>
      simp [Float.IsFinite]
      simp [to_fp64, to_float] at h
      simp [Nat.log, roundsub, subnormal_round, round_function, round_near, fp64_config, round_rep, roundf, roundnearest, round_near_int] at h
      norm_num at h
      simp only [Int.reduceNeg, FloatRep.normalize, Nat.reduceEqDiff, ↓reduceIte, Int.reduceLT,
        ↓reduceDIte, reduceCtorEq] at h
  | nan =>
      simp [Float.IsFinite]
      simp [to_fp64, to_float] at h
      simp [Nat.log, roundsub, subnormal_round, round_function, round_near, fp64_config, round_rep, roundf, roundnearest, round_near_int] at h
      norm_num at h
      simp only [Int.reduceNeg, FloatRep.normalize, Nat.reduceEqDiff, ↓reduceIte, Int.reduceLT,
        ↓reduceDIte, reduceCtorEq] at h
  | normal rep he hm =>
      simp [Float.IsFinite]
  | subnormal sm hlt =>
      simp [Float.IsFinite]

まずとにかく、計算を手順に従って進めればわかることをなぜ証明できないのが疑問でした。 この計算の停止性は、関数を定義できた時点で明確なので、とにかく計算を進めてほしいと感じました。 そもそも、何が原因で計算が止まっているのかもよくわかりません。 simpのあとの角括弧に関数定義を入れる必要があるというのがなかなか理解できませんでした。 最後のほうの自明な計算をどうやるのかは、simp?で生成したので、どういう定理なのかは把握していません。

ここでできた証明は不必要に冗長なはずなので、どのように縮めることができるか、というかそもそも場合分けなんかせずに素直に計算を進めればいいのでは……ということをChatGPTに聞きました。 この辺はLLMの得意な分野でしょう。 あと、矢印とかの意味も聞きました。 こういうのは検索しにくいのでLLMに聞くのがよいですね。

example : (to_fp64 5).IsFinite := by
  dsimp [to_fp64, to_float, round_near, fp64_config]
  simp [Nat.log, round_rep, roundf, round_function, roundnearest, round_near_int, FloatRep.normalize]
  norm_num
  simp [Float.IsFinite]

やっとテスト

これで(to_fp64 5).IsFiniteの証明が得られたので、以下のケースをテストすることができました。

example : get_exp (to_fp64 5) to_fp64_5_finite = 2 := by
  dsimp [to_fp64, to_float, round_near, fp64_config]
  simp [Nat.log, round_rep, roundf, round_function, roundnearest, round_near_int, FloatRep.normalize]
  norm_num -- ここまででto_fp64を評価完了
  simp [get_exp]

さて、全く同じコードが二回出てきてしまっています。 どうにかできないのかChatGPTに聞いたところ、タクティックとしてまとめる方法があると教えてくれました。

import Flean
import Flean.FloatCfg
import Flean.Rounding
import Mathlib.Tactic

open Flean
open FloatCfg
open RoundingMode
open Mathlib.Tactic
open Lean Elab Tactic

def round_near : Rounding := ⟨nearest⟩
def fp64_config : FloatCfg := { prec := 2^53, emin := -1022, emax := 1023, emin_lt_emax := by decide, prec_pos := by decide }
def to_fp64 := to_float (C := fp64_config) (R := round_near)
def round_fp64 := fun x => to_rat (to_fp64 x)

elab "unfold_to_fp64" : tactic => do
  evalTactic (← `(tactic| dsimp [to_fp64, to_float, round_near, fp64_config]))
  evalTactic (← `(tactic| simp [Nat.log, round_rep, roundf, round_function, roundnearest, round_near_int, FloatRep.normalize]))
  evalTactic (← `(tactic| norm_num))

def get_exp {C : FloatCfg} (f : Float C) (hf : f.IsFinite) : ℤ := by
    cases f with
    | inf _ => cases hf -- unreachable
    | nan => cases hf -- unreachable
    | normal n _ _ => exact n.e
    | subnormal _ _ => exact C.emin

lemma to_fp64_5_finite : (to_fp64 5).IsFinite := by
  unfold_to_fp64
  simp [Float.IsFinite]

example : get_exp (to_fp64 5) to_fp64_5_finite = 2 := by
  unfold_to_fp64
  simp [get_exp]

関数を増やす

この調子で、仮数部を取り出す関数とそのテストも作成しました。いい感じです。

def get_mant {C : FloatCfg} (f : Float C) (hf : f.IsFinite) : ℤ := by
    cases f with
    | inf _ => cases hf -- unreachable
    | nan => cases hf -- unreachable
    | normal n _ _ => exact if n.s then -(n.m + C.prec : Int) else (n.m + C.prec : Int)
    | subnormal s _ => exact if s.s then -(s.m : Int) else (s.m : Int)

example : get_mant (to_fp64 5) to_fp64_5_finite = 5 * 2^51 := by
  unfold_to_fp64
  simp [get_mant]

証明その2 (to_fp64 ((5 : Rat) / 2)).IsFinite

非正規化数もテストしようと思ったのですが、非正規仮数どころか、分数だと（？）作ったタクティックがうまく機能しないということがわかりました。

lemma to_fp64_5pm1_finite : (to_fp64 ((5 : Rat) / 2)).IsFinite := by
  unfold_to_fp64
  simp [Float.IsFinite]

↓

tactic 'simp' failed, nested error:
maximum recursion depth has been reached

どうやら計算に詰まっているようですが、何が原因で詰まっているのかを調べるのが本当に大変です。 特に、記号で書かれた関数を展開するためにsimpに入れるべき名前を調べることが大変です。 その手の記号は多相関数になっていることが多いことも厄介です。 hintを使っても証明が完了するかを探索するようで、次の一手を教えてくれるわけではないので、ChatGPTに「(5 / 2).numの評価が進まない場合はどうしたらよいですか？」「FloorRing.floor { num := 5, den := 2, den_nz := ⋯, reduced := ⋯ }の評価を進めるためにはどうすればよいですか？」などと聞き続けていました。 結局よくわからず、構造体のフィールドを取り出す補題を書くみたいなことをやっていました……。

5時間くらい苦労して以下を書きましたが、行き詰りました。 contrapose!のあとに仮定をclearしているのは、長大に展開された式が仮定に入っているとゴールが何であるかスクロールしないと見れないからです。 つまり、展開しなくても矛盾が示せるのに、気づかずに展開してしまったというミスです。

lemma to_fp64_5pm1_finite : (to_fp64 ((5 : Rat) / 2)).IsFinite := by
  have h8: ((5 : Rat) / 2).num = 5
  norm_num
  have h9: ((5 : Rat) / 2).den = 2
  norm_num
  have h10: ((5 : Rat) / 2).den ≠ 0
  norm_num
  dsimp [to_fp64, to_float, round_near, fp64_config]
  simp [Int.reduceNeg, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_self, ↓reduceDIte, gt_iff_lt]
  simp [abs_of_pos (show (0 : ℚ) < 5 / 2 by norm_num)]
  simp [Int.log]
  simp [one_le_div_iff]
  simp [roundsub, subnormal_round, round_function, roundnearest, round_near_int]
  split <;> rename_i h1
  split <;> rename_i h2
  split <;> rename_i h3
  split
  simp [Float.IsFinite]
  simp [Float.IsFinite]
  split <;> rename_i h4
  split
  simp [Float.IsFinite]
  simp [Float.IsFinite]
  split
  split
  simp [Float.IsFinite]
  simp [Float.IsFinite]
  split
  simp [Float.IsFinite]
  simp [Float.IsFinite]
  simp [Float.IsFinite]
  split <;> rename_i h5
  contrapose! h5
  split <;> rename_i h6
  contrapose! h6
  simp [round_rep, roundf, round_function, roundnearest, round_near_int]
  split <;> rename_i h7
  simp_all only [not_lt, not_false_eq_true, Float.inf.injEq]
  simp [Int.log]
  split <;> rename_i h11
  simp [Rat.abs_def, Rat.num, Rat.den, mkRat, Rat.normalize, Int.natAbs, Rat.num, Rat.inv_def, Int.mul_comm]
  simp [h8, h9, h10, Nat.floor, FloorSemiring.floor, Int.floor, Int.toNat, FloorRing.floor]
  norm_num
  simp [Rat.floor_def]
  simp [Rat.mul_def, Rat.num, Rat.den, mkRat, Rat.normalize, Int.natAbs, Rat.num, Rat.inv_def, Int.mul_comm]
  simp [Nat.log] <;> norm_num
  simp [Rat.mul_def, Rat.sub_def, Rat.normalize, Rat.num, Rat.den, mkRat, Rat.normalize, Int.natAbs, Rat.num, Rat.inv_def, Int.mul_comm]
  simp [FloatRep.normalize]
  simp [Int.log, Rat.abs_def, Rat.mul_def, Rat.sub_def, Rat.divInt, Rat.num, Rat.den, Int.natAbs, mkRat, Rat.normalize] <;> norm_num -- 1/6
  contrapose! h11
  clear h11
  simp [Rat.abs_def, mkRat, Rat.normalize, Int.natAbs, Rat.num, Rat.den, h8, h9, Rat.divInt, h10, Rat.le_def] -- 1/5
  contrapose! h6
  clear h6
  simp_all only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, not_lt, Float.inf.injEq]
  intro

ここまでで得た知識を使って、書き直してみたら1時間ほどで証明を完成させることができました。

lemma to_fp64_5pm1_finite : (to_fp64 ((5 : Rat) / 2)).IsFinite := by
  have h8: ((5 : Rat) / 2).num = 5
  norm_num
  have h9: ((5 : Rat) / 2).den = 2
  norm_num
  have h10: ((5 : Rat) / 2).den ≠ 0
  norm_num
  have h13: Rat.floor ((5 : Rat) / 2) = 2
  simp [Rat.floor, h8, h9]
  have h12: Int.log 2 |(5 : ℚ) / 2| = 1
  simp [Int.log, Rat.abs_def, Rat.mul_def, Rat.sub_def, Rat.divInt]
  simp [h8, h9, h10, Rat.divInt, Rat.le_def, mkRat, Rat.normalize, Nat.floor, FloorSemiring.floor, Int.floor]
  simp [Rat.floor_def]
  simp [Nat.log]
  have h14: ((5 : Rat) / 2) > 0
  norm_num
  have h15: ((5 : Rat) / 2) ≠ 0
  norm_num
  have h16: |(5 : Rat) / 2| = (5 : Rat) / 2
  simp [Rat.abs_def, Rat.divInt, mkRat, h8, h9, Rat.normalize]
  exact Rat.ext (Eq.symm h8) (Eq.symm h9)

  dsimp [to_fp64, to_float, round_near, fp64_config]
  -- 5/2 ≠ 0
  split <;> rename_i h
  trivial

  -- not subnormal
  split <;> rename_i h
  rw [h12] at h
  trivial

  split <;> rename_i h
  contrapose! h
  simp [round_rep, roundf, round_function, h12, roundnearest] <;> norm_num
  simp [h16, Inv.inv, Rat.inv, Rat.mul_def, h8, h9, Rat.normalize, Rat.sub_def, round_near_int]
  simp [FloatRep.normalize, Float.IsFinite]

  -- not Inf
  trivial

上のコメントは今見ると一部誤っています。 最初のspiltで生成された枝は、0であればsubnormal 0を返すのでIsFiniteが真になる、という証明を行っています（5/2 = 0という矛盾を指摘したほうがスマートですね）。 三個目の枝は、指数部を具体的に計算して、inf signではないことを示しています。 最後の枝は、normal sign expo mantを返す枝で、自明にIsFiniteが真になる、という証明を行っています。

証明その3 (x : ℚ) (h1: 1 ≤ x) (h2: x < 2) : (to_fp64 x).IsFinite

一回目

ここまでで力もついてきたので、ただ計算すればわかるような命題ではなく、一般的な命題を示してみましょう。 1～2の範囲の有理数を浮動小数点数に変換すると、IsFiniteが満たされるという全称命題を示すことにします。 50分くらいかけて、とりあえず以下のように書きました。

theorem OneToTwo_is_Finite (x : ℚ) (h1: 1 ≤ x) (h2: x < 2) : (to_fp64 x).IsFinite := by
    have h16: |x| = x
    norm_num
    linarith
    have h17: x.den > 0
    simp [Rat.den_pos]
    have h18: x.num > 0
    simp [Rat.num_pos]
    linarith
    have h13: ⌊x⌋ < 2
    exact Int.floor_lt.mpr h2
    have h19: 1 ≤ ⌊x⌋
    exact Int.le_floor.mpr h1

    have h12: Int.log 2 |x| = 0
    simp [Int.log, h16, h1, Nat.floor, FloorSemiring.floor, Int.toNat]
    split
    simp_all only [abs_eq_self, gt_iff_lt, Rat.num_pos, Int.ofNat_eq_coe, Nat.cast_lt_ofNat, Nat.one_le_cast]
    trivial

    have h20: 0 ≤ |x| - 1
    rw [h16]
    linarith
    have h21: |x| - 1 < 1
    rw [h16]
    linarith

    have h22: 0 ≤ (|x| - 1) * 9007199254740992
    linarith

    have h23:  (|x| - 1) * 9007199254740992 < 9007199254740992
    linarith

    dsimp [to_fp64, to_float, round_near, fp64_config]
    -- 0 is finite
    split
    trivial
    -- not subnormal
    split <;> rename_i h
    rw [h12] at h
    trivial

    split <;> rename_i h
    contrapose! h
    simp [round_rep, roundf, round_function, h12, roundnearest, Int.natAbs]
    split <;> rename_i h
    simp [FloatRep.normalize]
    split <;> rename_i h
    tauto
    tauto

    simp [FloatRep.normalize]
    split

9007199254740992のパターンと9007199254740991のパターンの証明が求められたので、証明の方針が全探索なのかな？と思って、見通しも悪くなってきたので一旦やり直すことにしました。 どうもこれは、仮数部が ofNat 9007199254740992またはnegSucc 9007199254740991（つまり \pm 2^{53}）であるときは指数部を1増やす、という分岐に対応していて、別に全探索にはなっていなかったようですが、その時は気づきませんでした。

二回目

補題を作る

やり直していくうちに、うまく補題を作ることを覚えました。 例えば以下の補題h41は、既存の補題をうまく組み合わせることで作ることのできた、直観的に理解しやすい補題です。

    have h41 (x : ℚ)(h1: 0 ≤ x ) : 0 ≤ round_near_int (x)
    simp [round_near_int, Inv.inv, Rat.inv]
    split
    exact Int.floor_nonneg.mpr h1
    split
    exact Int.ceil_nonneg h1
    split
    exact Int.floor_nonneg.mpr h1
    exact Int.ceil_nonneg h1

ここで使っている定理は、hintによって提案されたものです。 複数回同じものが出てくることに気づいたので、まとめる方法があるかChatGPTに聞いたら、split_ifs <;>を使えばいいと教えてくれました。 このように書けるのはなかなか面白いと思いました。

    have h41 (x : ℚ)(hx: 0 ≤ x ) : 0 ≤ round_near_int (x)
    simp [round_near_int, Inv.inv, Rat.inv]
    split_ifs <;> simp [Int.floor_nonneg.mpr hx, Int.ceil_nonneg hx]

証明の全体像

そんなこんなで、（上記h41を証明するのも含めて、）書き直し始めてから90分くらいで証明を完了できました。

theorem OneToTwo_is_Finite (x : ℚ) (h1: 1 ≤ x) (h2: x < 2) : (to_fp64 x).IsFinite := by
    have h16: |x| = x
    norm_num
    linarith
    have h17: x.den > 0
    simp [Rat.den_pos]
    have h18: x.num > 0
    simp [Rat.num_pos]
    linarith
    have h13: ⌊x⌋ < 2
    exact Int.floor_lt.mpr h2
    have h19: 1 ≤ ⌊x⌋
    exact Int.le_floor.mpr h1

    have h12: Int.log 2 |x| = 0
    simp [Int.log, h16, h1, Nat.floor, FloorSemiring.floor, Int.toNat]
    split
    simp_all only [abs_eq_self, gt_iff_lt, Rat.num_pos, Int.ofNat_eq_coe, Nat.cast_lt_ofNat, Nat.one_le_cast]
    trivial

    have h20: 0 ≤ |x| - 1
    rw [h16]
    linarith
    have h21: |x| - 1 < 1
    rw [h16]
    linarith

    have h22: 0 ≤ (|x| - 1) * 9007199254740992
    linarith

    have h23:  (|x| - 1) * 9007199254740992 < 9007199254740992
    linarith

    have h25 (q : ℚ) : ⌊q⌋ ≤ q
    exact Int.floor_le q

    have h27 (q : ℚ) : ⌈q⌉ < q + 1
    exact Int.ceil_lt_add_one q

    have h30 (q : ℚ) : ⌈q⌉ ≤ q + 1
    have h : ⌈q⌉ < q + 1 := by exact Int.ceil_lt_add_one q
    linarith

    have h24 (x : ℚ) (y : ℚ) (h1: x ≤ y ) : round_near_int (x) ≤ y + 1
    simp [round_near_int, Inv.inv, Rat.inv]
    split
    have h26:  ⌊x⌋ ≤ y
    exact (h25 x).trans h1
    linarith
    split
    have h31: x + 1 ≤ y + 1 := by linarith
    exact (h30 x).trans h31
    split
    have h32: ⌊x⌋ ≤ x := by exact h25 x
    linarith
    have h33: ⌈x⌉ ≤ x + 1 := by exact h30 x
    linarith

    have h41 (x : ℚ)(hx: 0 ≤ x ) : 0 ≤ round_near_int (x)
    simp [round_near_int, Inv.inv, Rat.inv]
    split_ifs <;> simp [Int.floor_nonneg.mpr hx, Int.ceil_nonneg hx]

    dsimp [to_fp64, to_float, round_near, fp64_config]
    -- not zero
    split
    trivial
    -- not subnormal
    split <;> rename_i h
    rw [h12] at h
    trivial

    -- inf
    split <;> rename_i h
    contrapose! h
    simp [round_rep, roundf, round_function, h12, roundnearest, Int.natAbs]
    cases h40: round_near_int ((|x| - 1) * 9007199254740992)
    simp [FloatRep.normalize] <;> rename_i g
    split <;> rename_i h
    rw [h] at h40
    tauto
    tauto
    rename_i g
    have h42: 0 ≤ round_near_int ((|x|-1) * 9007199254740992) := by tauto
    rw [h40] at h42
    tauto

    -- normal
    simp [Float.IsFinite]

正しさが保証される

おもしろかったのは、「なんでうまくいかないんだろう？」となった時に、実は示したい補題が間違っていた、ということがあったことです。 (q : ℚ) : ⌊q⌋ < qを示そうと四苦八苦していたのですが、まぁ間違っている補題なので証明できるわけがないわけです（ChatGPTに相談して、それ成り立つとは限らないよって言われました……orz）。

他にも、x ≧ 0からx > 0を証明しようとしてlinarithを使うも証明できずなんで？？となっていたところ、よく見たら証明できない命題だったということもありました。

定理を検索できる

ceil側も証明しようと思ったとき、補完でceilという名前が入っている定理を検索できたのも、証明支援系を名乗るだけのことはある、と思いました。 (q : ℚ) : ⌈q⌉ < q + 1が成り立つわけですが、ぱっと思い出せるものでもないので、定理ライブラリが充実しているというのは証明支援系を選ぶポイントだと思いました。

証明をきれいにする

splitしたあとtautoし続けるみたいなことをやっていて、無意味なことをやっていそうです。 tautoは仮定の一覧から矛盾が導けるみたいな時にそれを自動でやってくれるようですが、どの補題を使ったのかが表面上わからないのが不満です。 とりあえずより読みやすい形に変えていきます。 その過程で、使われていない補題があることも判明しました。

他にも、以下を覚えました。

  • byを使ってインデントできる
  • ビュレット（どうやって入力するのだろう*1）を使うことで、サブゴールがどこで終わっているのかを明確化できる（ChatGPT）
  • trivial（名前に反して複数のタクティックを試すらしい）よりもdecideの方がより明示的（ChatGPT）
  • フィールドを計算しなくともコンストラクタの名前だけで結果が確定する場合、rflタクティックでよい（hint）
  • linarithの引数で補題を渡せる。無名の補題を作るときはshowを使う（ChatGPT）
theorem PositiveRoundNearInt (x : ℚ) (hx: 0 ≤ x) : 0 ≤ round_near_int (x) := by
  simp [round_near_int]
  split_ifs <;> simp [Int.floor_nonneg.mpr hx, Int.ceil_nonneg hx]

theorem OneToTwo_is_Finite (x : ℚ) (h1: 1 ≤ x) (h2: x < 2) : (to_fp64 x).IsFinite := by
    have hPositive: |x| = x := by
      norm_num
      linarith

    have hRoughExpoIsZero: Int.log 2 |x| = 0 := by
      simp [Int.log, hPositive, h1, Nat.floor, FloorSemiring.floor, Int.toNat]
      split
      · simp_all only [Int.ofNat_eq_coe]
        linarith [show ⌊x⌋ < 2 from Int.floor_lt.mpr h2]
      · decide -- 0 < 2

    have hMantissaBitsIsPositive: 0 ≤ round_near_int ((|x|-1) * 9007199254740992) := by
      have h22: 0 ≤ (|x| - 1) * 9007199254740992 := by linarith
      exact PositiveRoundNearInt ((|x| - 1) * 9007199254740992) h22


    dsimp [to_fp64, to_float, round_near, fp64_config]

    -- zero
    split
    rfl -- (subnormal 0) is Finite

    -- subnormal
    split <;> rename_i h
    rw [hRoughExpoIsZero] at h
    contradiction

    -- inf
    split <;> rename_i h
    contrapose! h
    simp [round_rep, roundf, round_function, hRoughExpoIsZero, roundnearest, Int.natAbs]
    cases g: round_near_int ((|x| - 1) * 9007199254740992) with
    | ofNat   => simp [FloatRep.normalize]
                 split <;> norm_num
    | negSucc => rw [g, Int.negSucc_not_nonneg] at hMantissaBitsIsPositive
                 contradiction

    -- normal
    rfl

hMantissaBitsIsPositiveは今見るとhMantissaBitsIsNonNegativeな気がしますが、まぁ気にしないことにします。

証明その4 (x : ℚ) (h1: 1 ≤ x) (h4: x < 4) : (to_fp64 x).IsFinite

とりあえず作った証明

OneToTwo_is_Finiteは、指数部が（繰り上がらなければ）0と確定していたので、一般化の度合いが低かったと言えます。 とりあえず範囲を広げて、1～4の範囲について、浮動小数点数に変換した時の有限性を示すことにします。 途中、ChatGPTからは「0, 1, 2, 3の全パターンを示せばいいんじゃない？」みたいに言われましたが、それだと一般化度合いの高い命題を示す勉強にならないので、そうならないようにしました。

【g &lt; 4 から Nat.log 2 g &lt; 2 を示す最短経路 Nat.log の設計上、底が 2 なら 　gの値が0,1 → Nat.log 2 gが0; gの値が2,3 → Nat.log 2 gが1; gの値が≧4 → Nat.log 2 gが2以上; なので g &lt; 4 ⇒ 結果は 0 か 1。 全ての場合分けしてしまうのがシンプルで機械的です。】
ChatGPTの出力。日本語がやや変

3時間ほどかけて、以下の証明を作ることができました。 simp [Nat.log]が無限ループになるのが大変でしたが、deltaを使うべきだとChatGPTに教わりました。 また、set ... with ...で項を名前付きで取り出せるということも教わりました。

おもしろかったのは、 p \le q \rightarrow b^p \le b^qみたいな補題があるはず……と思って補完機能で探しに行って見つけた補題に、ちゃんと 1 \le bが仮定に入っていたりすることです。 こういうところはうっかりしがちなので、形式的にやるメリットだと感じました。 特に bとして具体的なものを考えている時は忘れがちだと思います。 このくらい自明なものはby decideで証明を用意できるので、厳密過ぎて自明なこともいちいち証明しないといけない、とは感じませんでした。

theorem OneToFour_is_Finite (x : ℚ) (h1: 1 ≤ x) (h4: x < 4) : (to_fp64 x).IsFinite := by
    have hPositive: |x| = x := by
      norm_num
      linarith

    have ho: 1 ≤ ⌊x⌋ := by
      exact Int.le_floor.mpr h1

    have hf: ⌊x⌋ < 4 := by
      exact Int.floor_lt.mpr h4

    have hRoughExpoGtZero : 0 ≤ Int.log 2 |x| := by
      simp [Int.log, hPositive, h1, Nat.floor, FloorSemiring.floor, Int.toNat]

    have hRoughExpoLtTwo : Int.log 2 |x| < 2 := by
      simp [Int.log, hPositive, h1, Nat.floor, FloorSemiring.floor, Int.toNat]
      split <;> rename_i g hg
      have h : g < 4 := by
        simp_all
      have hz : g ≠ 0 := by
        cases g
        rw [hg] at ho
        contradiction
        linarith

      have h2 : Nat.log 2 g < 2 := by
        have h3 : g < Nat.pow 2 2 := by norm_num; exact h
        have h4 : g < 2 ^ 2 ↔ Nat.log 2 g < 2 := by
          exact Nat.lt_pow_iff_log_lt (b := 2) (hb := by decide) (x := 2) (y := g) (hy := hz)
        simp_all

      exact h2
      omega

    have hExpoUpperLtThree : Int.log 2 |x| + 1 < 3 := by
      linarith

    have hMantissaBitsIsPositive: 0 ≤ round_near_int ((|x|-1) * 9007199254740992) := by
      have h22: 0 ≤ (|x| - 1) * 9007199254740992 := by linarith
      exact PositiveRoundNearInt ((|x| - 1) * 9007199254740992) h22


    set k : ℚ := (2 : ℚ) ^ (Int.log 2 x) with hk
    have hk0 : 1 ≤ k := by
      rw [← hPositive] at hk
      rw [hk]
      have hq : (1 : ℚ) = 2 ^ 0 := by decide
      rw [hq]
      have hqq (y : ℤ) (hy: 0 ≤ y) : (2 : ℚ) ^ 0 ≤ 2 ^ y := by
        exact zpow_le_zpow_right₀ (a := (2 : ℚ)) (ha := by decide) (m := 0) (n := y) hy
      tauto

    dsimp [to_fp64, to_float, round_near, fp64_config]

    -- zero
    split
    rfl -- (subnormal 0) is Finite

    -- subnormal
    split <;> rename_i h
    linarith [hRoughExpoGtZero]


    -- inf
    split <;> rename_i h
    contrapose! h
    simp [round_rep, roundf, round_function]
    simp [roundnearest, Int.natAbs]
    cases g: round_near_int ((x * (2 ^ Int.log 2 x)⁻¹ - 1) * 9007199254740992) with
    | ofNat   => simp [FloatRep.normalize]
                 split
                 aesop
                 linarith
                 linarith
                 aesop
                 linarith
                 linarith
    | negSucc =>
        simp [FloatRep.normalize]
        split
        split
        aesop
        linarith
        aesop
        linarith
        aesop
        linarith
        linarith

    -- normal
    rfl

証明をきれいにする

まず目につくのは、splitしたあとaesopとlinarithしている部分です（ここのaesopはhintで提示されたものですが、実際には構造体のフィールドを取り出しているだけで、simpで十分だったようです）。 ここは<;>でつなぐように書き換えられました。 ただ、一つの分岐だけはsimpが進まないので単純にはうまくいきませんが、tryが使えることに気づきました。 探索的なタクティックを作るために使うものだと思っていましたが、こういう使い方もあるんですね。

結局、多少きれいにしたものは以下のような感じになりました。 タクティックが補題をいい感じに選んで進めてくれるので、補題の命名が適当になりがちという問題があると思いました（責任転嫁）。

theorem OneToFour_is_Finite (x : ℚ) (h1: 1 ≤ x) (h4: x < 4) : (to_fp64 x).IsFinite := by
    have hPositive: |x| = x := by
      norm_num
      linarith

    have ho: 1 ≤ ⌊x⌋ := by
      exact Int.le_floor.mpr h1

    have hf: ⌊x⌋ < 4 := by
      exact Int.floor_lt.mpr h4

    have hExpoGtZero : 0 ≤ Int.log 2 |x| := by
      simp [Int.log, hPositive, h1, Nat.floor, FloorSemiring.floor, Int.toNat]

    have hRoughExpoLtTwo : Int.log 2 |x| < 2 := by
      simp [Int.log, hPositive, h1, Nat.floor, FloorSemiring.floor, Int.toNat]
      split <;> rename_i g hg
      have hz : g ≠ 0 := by
        cases g
        rw [hg] at ho
        contradiction
        linarith
      simp_all [Nat.lt_pow_iff_log_lt (b := 2) (hb := by decide) (x := 2) (y := g) (hy := hz)]

      omega

    have hExpoUpperLtThree : Int.log 2 |x| + 1 < 3 := by
      linarith

    set k : ℚ := (2 : ℚ) ^ (Int.log 2 x) with hk
    have hk0 : 1 ≤ k := by
      rw [hk, ← hPositive, show ((1 : ℚ) = 2 ^ 0) by decide]
      have hqq (y : ℤ) (hy: 0 ≤ y) : (2 : ℚ) ^ 0 ≤ 2 ^ y := by
        exact zpow_le_zpow_right₀ (a := (2 : ℚ)) (ha := by decide) (m := 0) (n := y) hy
      exact hqq (Int.log 2 |x|) hExpoGtZero

    dsimp [to_fp64, to_float, round_near, fp64_config]

    -- zero
    split
    rfl -- (subnormal 0) is Finite

    -- subnormal
    split
    linarith [hExpoGtZero]

    -- inf
    split <;> rename_i h
    contrapose! h
    simp [round_rep, roundf, round_function]
    simp [roundnearest, Int.natAbs]
    cases g :
      round_near_int ((x * (2 ^ Int.log 2 x)⁻¹ - 1) * 9007199254740992)
      <;> simp [FloatRep.normalize]
      <;> split <;> split <;> try simp; linarith

    -- normal
    rfl

<;>でまとめたのはcases gのところですが、結局8分岐を全部証明しているので、読み込ませたときにここでかなり時間がかかるようになってしまいました。 快適に作業を進めるためには、検証しやすい証明を書く必要があるということでしょうか。 ――と思っていたのですが、ブログを書くにあたって各段階のコードを読み込ませていたところ、まとめる前からcases gのところで遅くなっていることがわかりました。 なんだか大きな有理数の計算をやっているので遅いとかその辺でしょうか。

to_float_in_range

証明に必要な証明を作る

無限再帰する

Fleanのライブラリをながめていたら、to_float_in_rangeという、まさにやっていたことそのものの定理がありました。 絶対値がmax_float_q (C : FloatCfg) : ℚ以下であるという証明を元に、IsFiniteの証明を作成してくれるようです。 そこで、次のように証明を作ってみました。 あまりにも有理数演算の評価が進まなくてイライラしていた痕跡が証明に残っています。

lemma to_fp64_5_4_finite : (to_fp64 ((5 : Rat) / 4)).IsFinite := by
  have h1: |(5 : Rat) / 4| ≤ max_float_q fp64_config := by
    simp [Rat.abs_def]
    simp [max_float_q]
    simp [Inv.inv, Rat.inv]
    split <;> rename_i h2
    simp [Rat.sub_def, Rat.normalize, fp64_config, Rat.mul]
    norm_num
    linarith
    split <;> rename_i h1
    norm_num
    simp [Rat.sub_def, Rat.normalize, fp64_config, Rat.mul]
    norm_num
    norm_num
    norm_num
    norm_num
    simp [Rat.mul_def, Rat.normalize]
    norm_num
    contradiction

↓

(kernel) deep recursion detected

大きな数は取り扱えない？

証明はあっていると思うのですが、再帰が深いというエラーが出てうまくいきません。 大きな数を取り扱うとうまくいかないから2^1024を具体的に計算せずに不等式で示すとかを頑張っていましたが、直りませんでした。

have h: |(5 : Rat) / 4| ≤ max_float_q fp64_config := by
    simp [Rat.abs_def]
    simp [max_float_q]
    simp [Inv.inv, Rat.inv]

    /-
    have h2 : (2 : ℚ) ≤ 2 ^ fp64_config.emax := by
      nth_rewrite 1 [show (2 : ℚ) = 2 ^ 1 by decide]
      have h3 : 1 ≤ fp64_config.emax := by decide

      have hqq (y : ℤ) (hy: 1 ≤ y) : (2 : ℚ) ^ (1 : ℤ) ≤ 2 ^ y := by
        exact zpow_le_zpow_right₀ (a := (2 : ℚ)) (ha := by decide) (m := 1) (n := y) hy
      simp_all only [zpow_one, pow_one]

    have h4 : (fp64_config.prec : ℚ)⁻¹ ≤ 1 := by
      simp [Inv.inv, Rat.inv]
      decide

    have h5 : (2 - (fp64_config.prec : ℚ)⁻¹) ≥ 1 := by
      linarith

    have h6 (a : ℚ) (b : ℚ) (c : ℚ) (ha: a ≤ 2) (hb: b ≥ 1) (hc: 2 ≤ c) : a ≤ b * c := by
      have hbnn : 0 ≤ b := by linarith
      have hbnn : 0 ≤ c := by linarith
      have h7 : 1 * (2 : ℚ) ≤ b * c := by
    -/


    split <;> rename_i h2
    simp [fp64_config]
    norm_num
    linarith
    split <;> rename_i h1
    simp [Rat.sub_def, fp64_config, Rat.mul_def]
    norm_num
    simp [Rat.normalize]
    norm_num
    simp [Rat.sub_def, fp64_config, Rat.mul_def, Rat.normalize]
    norm_num
    contrapose! h1
    dsimp [fp64_config]
    have : 9007199254740992 = 2 ^ 53 := by decide
    rw [this]
    have h1 : 2 ^ 0 ≤ 2 ^ 53 := by exact pow_le_pow_right₀ (a := 2) (ha := by decide) (hmn := by decide) (m := 0) (n := 53)
    have h0 : 0 < 2 ^ 0 := by decide
    exact lt_of_lt_of_le h0 h1

今度はメモリを食い尽くす

simpタクティックは一方通行ではない挙動をするとか言う話を聞いたので、

simp [Rat.sub_def, fp64_config, Rat.mul_def]

としていたところを

    simp [Rat.sub_def]
    simp [fp64_config, Rat.mul_def]

のように変えたところ、メモリを確保し続けてWindowsがフリーズする感じになりました。

その後3時間くらい格闘し続けましたが駄目でした（ブログを書くために確認したら先ほどの個所が悪かったということが分かったのであって、格闘していた時はどこが原因かわかっていませんでした）。

よくわからないが直った

今やってみると以下のような感じに簡略化できて、エラーもメモリの問題も解決しました。 simpなどを使うと証明がそこで終わったり終わらなかったりして、証明を修正するときに不便なので、積極的にビュレットを使っていきたいですね。 zifyは、「lean 4 便利なタクティック」で検索して出てきたタクティク - Lean by Exampleのページをながめていたら見つけたタクティックで、自然数に関する命題を整数に関する命題に変換するタクティックです。

lemma to_fp64_5_4_finite : (to_fp64 ((5 : Rat) / 4)).IsFinite := by
  have h1: |(5 : Rat) / 4| ≤ max_float_q fp64_config := by
    simp [Rat.abs_def, max_float_q, Inv.inv, Rat.inv]
    split
    · have h2: 0 < fp64_config.prec := fp64_config.prec_pos
      zify at h2
      linarith
    · simp [Rat.sub_def, fp64_config, Rat.mul_def]
      norm_num
      simp [Rat.normalize]
      norm_num
  exact to_float_in_range (C := fp64_config) (R := round_near) (q := ((5 : Rat) / 4)) (h := h1)

結局、無限再帰に陥る理由やメモリを確保し続ける理由はよくわかりませんでした。 set_option trace.FooBar trueみたいなオプションをつけても何も出てこないので、デバッグしようにもできません（Lean 4の環境構築 #lean4 - QiitaによればVisual Studio Codeではできない？）。 メモリを確保し続ける方に至っては本当に意味不明で、一度発生すると終了する以外に方法がないようでした。 また、言語サーバーを終了させた後もう一度起動した場合、そのファイルの証明検査がもう一度走る（Fleanライブラリ内の検査もやっている？）ようで、どこが悪い記述なのかを試すのも一苦労です。

まとめ

Lean 4に入門しました。 ある程度理解してきて、Lean 4固有の部分に苦労するのではなく証明を書く方に集中できるようになってきた気がします。 ただ、最後に意味不明な挙動を見せられてトラウマになりました。

明日はKPですね。 ひさしぶりな気がしますが、ブログを始めたのはもっと前だということに少し驚いています。

*1:適当に試していたら、\.でいけることがわかりました



以上の内容はhttps://lpha-z.hatenablog.com/entry/2025/07/20/231500より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます
不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14