見出し画像

事例: Lean 4.24.0 正式リリースとともに Mathlib4 もアップデートされたことによる型自動推論の失敗

D.

ABC予想 形式化 Issue

Lean のアップデートによるエラー

概要

Lean 4.24.0 正式リリースとともに Mathlib4 もアップデートされたことによる型自動推論の失敗

対応対策

tsum_fintype (f := fun b => μ b) の型が解決できるように案内してあげる

      have hsum : μ true + μ false = 1 := by
        -- fixed: build ok: Lean 4.24.0-release
        have : tsum (fun b : Bool => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b) :=
          tsum_fintype (f := fun b : Bool => μ b)
        simpa using Eq.symm (this)
        -- build ok: Lean 4.24.0-rc1
        -- simpa using Eq.symm (tsum_fintype (f := fun b => μ b))


解説

以前までの Mathlib4 では以下の記述で自動推論が効いていました。

simpa using Eq.symm (tsum_fintype (f := fun b => μ b))

しかし、アップデート後はこの推論に失敗してしまってエラーとなります。

tsum_fintype (f := fun b => μ b)

この部分が、推論できなくなってました。なので事前に、

have : tsum (fun b : Bool => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b) :=
  tsum_fintype (f := fun b : Bool => μ b)

という事で型推論出来るようにヒントを与えておきます。

simpa による具体的な内容は良くわからないですが、calc で書くと

      -- false 成分は和が 1 であることから決まる
      have hsum : μ true + μ false = 1 := by
        calc  -- calc version
          μ true + μ false = (Finset.univ : Finset Bool).sum (fun b => μ b) := by simp
          _ = μ.toOuterMeasure (Finset.univ : Finset Bool) := by
            rw [PMF.toOuterMeasure_apply_finset μ (Finset.univ : Finset Bool)]
          _ = ∑' b, (Set.univ : Set Bool).indicator μ b := by
            rw [PMF.toOuterMeasure_apply_finset μ (Finset.univ : Finset Bool)]
            simp only [Set.indicator_univ]
            -- Finset.sum と tsum の一致は tsum_fintype で得られる
            rw [tsum_fintype]
          _ = ∑' b, μ b := by simp
          _ = 1 := μ.tsum_coe

として展開できるようです。


まとめ

仕組みは解説できません。Appendix 以下に記載のログによると、

要点（結論）
lake update の後、mathlib 側で tsum / ∑' の定式化が「SummationFilter」によって一般化されました。

その結果、tsum_fintype の型に新しい暗黙引数（SummationFilter に関する型クラス引数）が入りこみ、Lean がその型クラスインスタンスを決定できずに metavariable を残したため、式が期待どおり 1 に畳み込まれなくなっています（エラーメッセージ中の SummationFilter.LeAtTop ?m.50 がまさにこれ）。

対処法は「新しい暗黙引数を明示する」「その型クラスインスタンスが文脈に存在するようにする」か「別の補題を使って有限和側に下ろす」のいずれかです。


内部でどうやっているのか見えないのがこの言語の欠点です。

自動化は良いですが AI が何をどうやって考えて答えを出しているかみたいなブラックボックス化はやはり不安です。信頼で何とか繋がっている状態。

証明されたら by? で展開されたアセンブラみたいなコードで残すのが良いのかもしれませんが、まったく意味がわからなくなります。中間的な展開が欲しいですね。


なのに明らかに自明で単純な不等式、等式も、ちょっと型が変わるだけで simp では解決できないという。よーくわからない言語ですね。

2025/10/15 18:44

D.

#Lean #Lean4
#Mathlib #Mathlib4
#ビルドエラー #Error


Appendix

障害対策ログ

2025/10/15 14:12

lake update を実行
lake build でエラー

error: MathlibHello/ABC.lean:7594:29: typeclass instance problem is stuck, it is often due to metavariables
  SummationFilter.LeAtTop ?m.50
error: MathlibHello/ABC.lean:7615:8: Type mismatch: After simplification, term
  Eq.symm (tsum_fintype fun b ↦ μ b)
 has type
  μ true + μ false = ∑'[?m.154] (b : Bool), μ b
but is expected to have type
  μ true + μ false = 1

lake update 後にビルドし直してみたらエラーが出るように。
leanprover/lean4:v4.24.0-rc1 → leanprover/lean4:v4.24.0

短く結論 — まずはクリーン再ビルドと依存の同期を試してください。多くの場合、lake/Lean バージョンを切り替えたときに生じる「型クラス探索が詰まる」「metavariable が残る」エラーは、古いコンパイル成果物や不整合な mathlib4 のコミットが原因です。

やること（順番どおりに）

  1. クリーン

    • プロジェクトルートで以下を実行してビルドキャッシュを消す（安全のため git 管理外ファイルが消える操作をする前に必要ならバックアップを）:

      • lake clean

      • rm -rf .lake build _build (存在するディレクトリ名はプロジェクトによる)

      • あるいは git clean -fdx （未追跡ファイルも消えるので注意）

  2. 依存の同期・再取得

    • lake update

    • lake build

  3. Docker／ツールチェインの確認

    • Docker イメージやローカルの lean バイナリを v4.24.0 に揃えたなら、全ての依存（特に mathlib4）の lock が対応するコミットになっているか確認してください。mathlib4 が Lean 4.24.0 RC1 用の古いコミットのままだと不整合が出ます。

    • lakefile.toml / lake.lock を確認し、必要なら mathlib4 の commit/tag を v4.24.0 対応のものに更新してから再度 lake update → lake build。

  4. それでも直らないとき（追加の情報収集）

    • 問題が残る場合、該当するファイルの該当行まわり（今回だと ABC.lean の 7590〜7620 行程度）を貼ってください。エラーメッセージ全文（`lake build`の出力）と、使用している lean のバージョンと mathlib4 のコミット SHA（`lake env` や lake.lock の情報）を教えてください。

    • こちらがあるとより具体的に原因（lemma 名や型クラスインスタンスのシグネチャ変更、tsum_fintype の仕様変更など）を突き止められます。

補足（原因の可能性）

  • "SummationFilter.LeAtTop ?m.50 が stuck" や "μ true + μ false = ∑'[?m.154] (b : Bool), μ b" のような出力は、tsum / summable のインスタンス解決が期待どおりに進んでいない（右辺の ∑' に残ったメタ変数がインスタンス探索で埋まらない）ことを示します。これは多くの場合ライブラリのバージョン不一致か、コンパイル済みアーティファクトが別バージョンで作られたために型情報がずれていることに起因します。

もし上の手順（クリーン → lake update → lake build）で直れば OK です。直らない場合は、上に書いた追加情報（該当コード部分と lake.lock / lean バージョン）を貼ってください。こちらでさらに掘り下げます。

Lean version: Lean (version 4.24.0, x86_64-unknown-linux-gnu, commit 797c613eb9b6d4ec95db23e3e00af9ac6657f24b, Release)
Mathlib version(revision): a0187b2361a9c9b82580bb0d68c25e16f9e96a9e
Lake version: Lake version 5.0.0-src+797c613 (Lean version 4.24.0)
Elan version: elan 4.1.2 (58e8d545e 2025-05-26)
✖ [7363/7368] Building MathlibHello.ABC (67s)
trace: .> LEAN_PATH=...
error: MathlibHello/ABC.lean:7594:29: typeclass instance problem is stuck, it is often due to metavariables
  SummationFilter.LeAtTop ?m.50
error: MathlibHello/ABC.lean:7615:8: Type mismatch: After simplification, term
  Eq.symm (tsum_fintype fun b ↦ μ b)
 has type
  μ true + μ false = ∑'[?m.154] (b : Bool), μ b
but is expected to have type
  μ true + μ false = 1
warning: MathlibHello/ABC.lean:8633:8: declaration uses 'sorry'
warning: MathlibHello/ABC.lean:14663:8: declaration uses 'sorry'
error: Lean exited with code 1
Some required targets logged failures:

- MathlibHello.ABC
/--
PMF Bool と ENNReal の区間 Set.Icc (0 : ENNReal) 1 との同型（equivalence）。

概要：
- toFun は二値確率分布 μ をその true 成分 probTrue μ（型は ENNReal）に写すことで、
  ENNReal 上の閉区間 [0,1] の元を得る。probTrue μ は 0 ≤ μ true ≤ 1 を満たすため
  Set.Icc (0 : ENNReal) 1 の要素となることを示す。
- invFun は区間の点 p を PMF.bernoulli (p.1.toNNReal) ... に送ることで二値の PMF を構成する。
  ここで p.1.toNNReal は p.1 ≤ 1（p の上界条件）に基づき有界な ENNReal を NNReal に落とす操作を用いる。
- left_inv は任意の PMF μ について invFun (toFun μ) = μ を示す。true 成分は ENNReal と NNReal
  間の coercion (ENNReal.coe_toNNReal) によって復元され、false 成分は μ true + μ false = 1 から 1 - μ true として導かれる。
- right_inv は区間の要素 p について toFun (invFun p) = p を示す。ここでは p.1 ≠ ⊤ をまず示し、
  ENNReal.coe_toNNReal を用いて↑(p.1.toNNReal) = p.1 を得て、bernoulli の true 成分が期待通りになることを確かめる。

注意事項：
- 定義は noncomputable であり、ENNReal と NNReal の変換（toNNReal, coe）や PMF.apply_ne_top,
  tsum_fintype, ENNReal.eq_sub_of_add_eq といった補題に依存している。
- 結果として、Bool 型上の確率質量関数全体は ENNReal 上の区間 [0,1] と一対一対応することが得られる。
- ドメイン上の全ての PMF は各点で ⊤ をとらないこと（PMF.apply_ne_top）を利用している。
- invFun では ENNReal.one_ne_top と p.2.right（p ≤ 1）を使って ENNReal → NNReal への単調性を確保している。
- 証明は各成分ごとの等式検証に還元され、bern oulli の具体的な適用則を用いて閉じられる。
- この同型は Bool 上のベルヌーイ分布と実際の確率 p ∈ [0,1] を対応させる標準的な同値である。
- 日本語コメントは定義の意図と主要な技術点を説明することを目的としている。
-/
noncomputable def pmfBoolEquivUnit : PMF Bool ≃ Set.Icc (0:ENNReal) 1 :=
{ toFun := fun μ =>
    ⟨probTrue μ, ⟨zero_le (probTrue μ), by
      -- 0 ≤ μ true ≤ 1 は PMF の和が 1 であることから従う
      have hsum : μ true + μ false = 1 := by
        simpa using Eq.symm (tsum_fintype (f := fun b => μ b)) -- ### Error ###
      calc
        μ true ≤ μ true + μ false := by
          apply le_add_of_nonneg_right
          exact zero_le (μ false)
        _ = 1 := by simp [hsum]
    ⟩⟩,
  invFun := fun p => PMF.bernoulli p.1.toNNReal (ENNReal.toNNReal_mono ENNReal.one_ne_top p.2.right),
  left_inv := by
    intro μ
    apply PMF.ext
    intro b
    cases b
    case true =>
      -- true 成分は定義通り
      -- μ true は PMF によって ⊤ にならないので ENNReal の toNNReal と逆変換で元に戻せる
      have : ↑((μ true).toNNReal) = μ true := ENNReal.coe_toNNReal (PMF.apply_ne_top μ true)
      simp [probTrue, this]
    case false =>
      -- false 成分は和が 1 であることから決まる
      have hsum : μ true + μ false = (1 : ENNReal) := by
        simpa using Eq.symm (tsum_fintype (f := fun b => μ b)) -- ### Error ###
      -- μ true ≠ ⊤ なので μ true = ↑(μ true).toNNReal
      have h_true : μ true = ↑(μ true).toNNReal := Eq.symm (ENNReal.coe_toNNReal (PMF.apply_ne_top μ true))
      -- μ false も ⊤ でない（PMF の性質）
      have h_false : μ false ≠ ⊤ := PMF.apply_ne_top μ false
      -- add の順序を入れ替えてから引き算の等式を得る
      have hsum_comm : μ false + μ true = (1 : ENNReal) := by
        rw [add_comm] at hsum
        exact hsum
      -- use the ENNReal-specific lemma so Lean picks the correct subtraction instance
      have h_false_eq : μ false = (1 : ENNReal) - μ true := ENNReal.eq_sub_of_add_eq (PMF.apply_ne_top μ true) hsum_comm
      have : μ false = (1 : ENNReal) - ↑(μ true).toNNReal := by
        rw [h_true] at h_false_eq
        exact h_false_eq
      simp [probTrue, this]
  right_inv := by
    intro p
    -- p.1 ∈ Set.Icc 0 1 なので p.1 ≠ ⊤
    have h_ne_top : p.1 ≠ ⊤ := by
      intro H
      -- H : p.1 = ⊤ と p.2.right : p.1 ≤ 1 から (⊤ : ENNReal) ≤ 1 を得る
      have hle : (⊤ : ENNReal) ≤ 1 := by
        rw [←H]; exact p.2.right
      -- しかし 1 ≤ ⊤ も成り立つので le_antisymm で ⊤ = 1 となり、1 ≠ ⊤ と矛盾する
      have heq : (⊤ : ENNReal) = 1 := le_antisymm hle (le_top : (1 : ENNReal) ≤ (⊤ : ENNReal))
      have : (1 : ENNReal) = ⊤ := Eq.symm heq
      exact absurd this ENNReal.one_ne_top
    -- ↑(p.1.toNNReal) = p.1
    have h_coe : ↑(p.1.toNNReal) = p.1 := ENNReal.coe_toNNReal h_ne_top
    -- 2つの構造体が等しいことを示す：toFun (invFun p) の true 成分が p.1 になることを示す
    apply Subtype.ext
    -- 定義を展開して true 成分の等式に帰着させる
    dsimp [probTrue]
    -- bernoulli の true 成分は ↑(p.1.toNNReal) に等しいのでそれを示す
    have hb : (PMF.bernoulli (p.1.toNNReal) (ENNReal.toNNReal_mono ENNReal.one_ne_top p.2.right)) true
      = ↑(p.1.toNNReal) := by
      simp [PMF.bernoulli_apply]
    -- 最後に coercion lemma を使って p.1 に戻す
    simp [hb, h_coe]
}

lake clean や rm -rf .lake 実行後

lake update
lake build

の、結果です。

原因と対処法（要点）

  • エラーは tsum_fintype を使った箇所が原因で、Lean が期待する型（μ true + μ false = 1）と tsum_fintype の返す等式の形が食い違い、さらに内部での型クラス解決が詰まっていることから起きています。ログの "SummationFilter.LeAtTop ?m.50" は ENNReal に関する和（tsum）の収束／フィルターの型クラス周りでメタ変数が残っていることを示しています。

  • 解決策は PMF がもともと持っている「全質量は 1」(tsum = 1) の補題を直接使うことです。mathlib の PMF 構造体には tsum = 1 を表す補題（たとえば PMF.tsum_eq_one やその同等物）があり、それを使えば tsum_fintype を経由する必要がなくなり、型クラスの迷走も回避できます。

修正例（差分）
問題になっている行（例）

have hsum : μ true + μ false = (1 : ENNReal) := by
  simpa using Eq.symm (tsum_fintype (f := fun b => μ b))

を次のように書き換えてください（PMF.tsum_eq_one が利用可能な名前である前提）：

have hsum : μ true + μ false = (1 : ENNReal) := by
  simpa using (PMF.tsum_eq_one μ).symm

あるいは .symm の代わりに Eq.symm を使っても構いません：

have hsum : μ true + μ false = (1 : ENNReal) := by
  simpa using Eq.symm (PMF.tsum_eq_one μ)

補足

  • PMF.tsum_eq_one の名前がリポジトリのバージョンで異なる場合（たとえば PMF.tsum_eq_one ではなく PMF.tsum_eq_one' 的な別名）、`#check` や `grep` で確認して適切な補題名に置き換えてください。たとえば `PMF tsum_eq_one` や `PMF.tsum_eq_one` で見つかるはずです。

  • tsum_fintype を直接使いたい場合は、返される等式の RHS がどういう形（∑' なのか finset.sum なのか）になっているかを明確にして、それに合わせて目標を作る必要がありますが、上のように PMF の補題を用いる方が簡潔で安全です。

  • 「declaration uses 'sorry'」の警告は今回のビルド失敗とは別問題ですが、将来的に正式な証明に差し替える必要があれば対処してください。

もし PMF.tsum_eq_one の名前が見つからない、あるいは別のエラーが残る場合はそのときの最新版の補題名と該当するファイル行（周辺の few lines）を教えてください。具体的なファイル先頭からの行番号とエラーメッセージをもう一度貼っていただければ、より正確なパッチを提示します。


      -- 0 ≤ μ true ≤ 1 は PMF の和が 1 であることから従う
      have hsum : μ true + μ false = 1 := by
        have : tsum (fun b : Bool => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b) :=
          tsum_fintype (f := fun b : Bool => μ b)
        simpa using Eq.symm (this)

これで、直りました。解説。

説明します。

ポイントは tsum_fintype が「有界（fintype）な型についての無限和 tsum を Finset.sum に書き換える」補題である点です。Bool の場合 (Finset.univ : Finset Bool) は {true, false} を表すので、その和は μ true + μ false になります。

あなたのコードの流れを分解するとこうなります。

  • tsum_fintype (f := fun b => μ b) は
    tsum (fun b => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b)
    を与える。

  • Eq.symm (this) で向きを反転して
    (Finset.univ : Finset Bool).sum μ = tsum μ
    になる。

  • そのまま simpa を使うと、Finset.univ の和が μ true + μ false に簡約され、また文脈に tsum μ = 1（PMF の和が 1）があればそれも使って右辺が 1 に簡約され、目的の
    μ true + μ false = 1
    が得られます。

別の書き方の例をいくつか示します（どれも同じ意味）：

  • 直接 simp を使う（文脈に tsum μ = 1 がある場合）:

  have hsum : μ true + μ false = 1 := by
    simp [tsum_fintype, hμ]  -- hμ は tsum μ = 1 の仮定

  • 手順を明示する:

  have hsum : μ true + μ false = 1 := by
    calc
      μ true + μ false = (Finset.univ : Finset Bool).sum μ := by simp
      _ = tsum μ := (tsum_fintype (f := μ))
      _ = 1 := hμ

  • tsum_fintype を使ってから転置して trans する:

  have hsum : μ true + μ false = 1 := by
    have A := (tsum_fintype (f := μ)).symm  -- Finset.sum μ = tsum μ
    simpa using A.trans hμ

最後に、μ true が 0 ≤ μ true ≤ 1 となるのは、μ true ≥ 0（PMF の非負性）と μ true ≤ μ true + μ false = 1（上で示した等式）から直ちに従います。

simpa using Eq.symm (tsum_fintype (f := fun b => μ b))
error: MathlibHello/ABC.lean:7594:29: typeclass instance problem is stuck, it is often due to metavariables
  SummationFilter.LeAtTop ?m.50
error: MathlibHello/ABC.lean:7615:8: Type mismatch: After simplification, term
  Eq.symm (tsum_fintype fun b ↦ μ b)
 has type
  μ true + μ false = ∑'[?m.154] (b : Bool), μ b
but is expected to have type
  μ true + μ false = 1

今回の修正で解ったこと。
lake update にて、何が変わってこのエラーが発生してしまったのか原因を分析解説。

要点（結論）

  • lake update の後、mathlib 側で tsum / ∑' の定式化が「SummationFilter」によって一般化されました。

  • その結果、tsum_fintype の型に新しい暗黙引数（SummationFilter に関する型クラス引数）が入りこみ、Lean がその型クラスインスタンスを決定できずに metavariable を残したため、式が期待どおり 1 に畳み込まれなくなっています（エラーメッセージ中の SummationFilter.LeAtTop ?m.50 がまさにこれ）。

  • 対処法は「新しい暗黙引数を明示する」「その型クラスインスタンスが文脈に存在するようにする」か「別の補題を使って有限和側に下ろす」のいずれかです。

詳しい説明（何が変わったのか）

  • 以前のバージョンでは tsum_fintype : (f : α →_) → _ という形で、fintype 上の tsum が直接有限和に等しいことを返す補題で、暗黙引数は少なかったか既定のインスタンスがすぐに解決されていました。

  • 最近の更新で tsum/∑' の定義が一般化され、どの種の「総和フィルタ（SummationFilter）」の下で収束を考えるかを表す型クラス（SummationFilter）を導入しました。これにより tsum_fintype もその一般化された形に合わせて型が変わり、暗黙の SummationFilter 関連の引数が増えています。

  • 今回のエラーメッセージを見ると、Eq.symm (tsum_fintype ...) の結果が
    μ true + μ false = ∑'[?m.154] (b : Bool), μ b
    になっており、右辺の ∑' の SummationFilter 引数が ?m.154 という未決定 metavariable のまま残っています。これが Lean によるさらなる簡約（= 1 に帰着）を妨げています。加えて typeclass search が SummationFilter.LeAtTop ?m.50 で詰まっている、というメッセージが出ています（インスタンス解決失敗）。

どうデバッグするか（実務上の手順）

  1. tsum_fintype の本当の型を確かめる

    • ソース内で `#check @tsum_fintype` や `#print tsum_fintype` を使い、どの暗黙引数（型クラス）が追加されているか確認してください。そこに SummationFilter 関連の引数が見えるはずです。

  2. エラー箇所に局所的に `by infer_instance` や `show` を入れて、どのインスタンスが欠けているか確かめる。

  3. エラーメッセージの SummationFilter.LeAtTop ?m.50 を手掛かりに、そのインスタンスを用意できないか検討する。

具体的な回避策（いくつかの選択肢）

  • 明示的に SummationFilter 引数を渡す（暗黙引数を明示化する）
    例えば tsum_fintype の暗黙引数が一つ目に SummationFilter ならば、`tsum_fintype (f := ...) (by infer_instance)` のようにしてインスタンス解決を強制できます（関数の正確な引数順は #check で確認してください）。

  • 文脈にインスタンスを追加する
    lemma の前に `instance : SummationFilter.LeAtTop ... := ...` のように局所インスタンスを置く（可能ならば）か、対象のファイルで必要なインポートを追加して既存のインスタンスが見えるようにする。

  • tsum_fintype を使わずに有限和で処理する
    Bool のような明らかに有限な指標なら、まず finset.sum に下してから処理するのが素直です。例えば

    • (finset.univ : Finset Bool).sum μ = μ true + μ false を simp 等で得て、必要なら tsum_fintype で ∑' と結びつける。
      こうすると SummationFilter の事情に巻き込まれずに式を簡約できます。

補足（なぜ以前は動いていたのか）

  • 以前の mathlib/mathlib4 のバージョンだと、SummationFilter の一般化が入る前で、デフォルトのインスタンスが自動的に解決されていたか、あるいはそもそもその引数が存在しなかったため、Eq.symm (tsum_fintype ...) が期待する「1」へと定義的に書き換えられていました。lake update により mathlib の新しいコミットが取り込まれ、その API 変更に合わせて書き換えが必要になった、というのが今回の状況です。

まとめ（対応のおすすめ順）

  1. まず #check で tsum_fintype の現在の型を確認する（何が暗黙引数か把握する）。

  2. 暗黙引数を明示的に供給するか、文脈に必要な SummationFilter インスタンスを置く。

  3. それが面倒なら、Bool の場合は finset.univ.sum を使って finite sum に下ろして処理する。

  4. 必要なら該当の mathlib の変更（SummationFilter 関連の PR）を確認し、変更の意図を把握してコードを追随させる。

もしよければ、あなたのファイル内で `#check @tsum_fintype` の出力か、該当箇所の周辺コード（どの命題の中でこの simpa をやっているか）を貼ってください。具体的にどの引数を明示させればうまくいくか、実際の修正コード例を出してお示しします。

@tsum_fintype : ∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [L.LeAtTop] [inst_3 : Fintype β] (f : β → α), ∑'[L] (b : β), f b = ∑ b, f b

theorem tsum_fintype.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [L.LeAtTop] [inst_3 : Fintype β] (f : β → α), ∑'[L] (b : β), f b = ∑ b, f b :=
fun {α} {β} [AddCommMonoid α] [TopologicalSpace α] {L} [L.LeAtTop] [Fintype β] f ↦
  tsum_eq_sum
    (of_eq_true
      (Eq.trans
        (forall_congr fun b ↦
          Eq.trans
            (implies_congr (Eq.trans (congrArg Not (eq_true (mem_univ b))) not_true_eq_false) (Eq.refl (f b = 0)))
            (propext IsEmpty.forall_iff))
        (implies_true β)))
noncomputable def pmfBoolEquivUnit : PMF Bool ≃ Set.Icc (0:ENNReal) 1 :=
{ toFun := fun μ =>
    ⟨probTrue μ, ⟨zero_le (probTrue μ), by
      -- 0 ≤ μ true ≤ 1 は PMF の和が 1 であることから従う
      have hsum : μ true + μ false = 1 := by
        -- fixed: build ok: Lean 4.24.0-release
        have : tsum (fun b : Bool => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b) :=
          tsum_fintype (f := fun b : Bool => μ b)
        simpa using Eq.symm (this)
        -- build ok: Lean 4.24.0-rc1
        -- simpa using Eq.symm (tsum_fintype (f := fun b => μ b))
      calc
        μ true ≤ μ true + μ false := by
          apply le_add_of_nonneg_right
          exact zero_le (μ false)
        _ = 1 := by simp [hsum]
    ⟩⟩,
  invFun := fun p => PMF.bernoulli p.1.toNNReal (ENNReal.toNNReal_mono ENNReal.one_ne_top p.2.right),
  left_inv := by
    intro μ
    apply PMF.ext
    intro b
    cases b
    case true =>
      -- true 成分は定義通り
      -- μ true は PMF によって ⊤ にならないので ENNReal の toNNReal と逆変換で元に戻せる
      have : ↑((μ true).toNNReal) = μ true := ENNReal.coe_toNNReal (PMF.apply_ne_top μ true)
      simp [probTrue, this]
    case false =>
      -- false 成分は和が 1 であることから決まる
      have hsum : μ true + μ false = 1 := by
        have : tsum (fun b : Bool => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b) :=
          tsum_fintype (f := fun b : Bool => μ b)
        simpa using Eq.symm (this)
      -- μ true ≠ ⊤ なので μ true = ↑(μ true).toNNReal
      have h_true : μ true = ↑(μ true).toNNReal := Eq.symm (ENNReal.coe_toNNReal (PMF.apply_ne_top μ true))
      -- μ false も ⊤ でない（PMF の性質）
      have h_false : μ false ≠ ⊤ := PMF.apply_ne_top μ false
      -- add の順序を入れ替えてから引き算の等式を得る
      have hsum_comm : μ false + μ true = (1 : ENNReal) := by
        rw [add_comm] at hsum
        exact hsum
      -- use the ENNReal-specific lemma so Lean picks the correct subtraction instance
      have h_false_eq : μ false = (1 : ENNReal) - μ true := ENNReal.eq_sub_of_add_eq (PMF.apply_ne_top μ true) hsum_comm
      have : μ false = (1 : ENNReal) - ↑(μ true).toNNReal := by
        rw [h_true] at h_false_eq
        exact h_false_eq
      simp [probTrue, this]
  right_inv := by
    intro p
    -- p.1 ∈ Set.Icc 0 1 なので p.1 ≠ ⊤
    have h_ne_top : p.1 ≠ ⊤ := by
      intro H
      -- H : p.1 = ⊤ と p.2.right : p.1 ≤ 1 から (⊤ : ENNReal) ≤ 1 を得る
      have hle : (⊤ : ENNReal) ≤ 1 := by
        rw [←H]; exact p.2.right
      -- しかし 1 ≤ ⊤ も成り立つので le_antisymm で ⊤ = 1 となり、1 ≠ ⊤ と矛盾する
      have heq : (⊤ : ENNReal) = 1 := le_antisymm hle (le_top : (1 : ENNReal) ≤ (⊤ : ENNReal))
      have : (1 : ENNReal) = ⊤ := Eq.symm heq
      exact absurd this ENNReal.one_ne_top
    -- ↑(p.1.toNNReal) = p.1
    have h_coe : ↑(p.1.toNNReal) = p.1 := ENNReal.coe_toNNReal h_ne_top
    -- 2つの構造体が等しいことを示す：toFun (invFun p) の true 成分が p.1 になることを示す
    apply Subtype.ext
    -- 定義を展開して true 成分の等式に帰着させる
    dsimp [probTrue]
    -- bernoulli の true 成分は ↑(p.1.toNNReal) に等しいのでそれを示す
    have hb : (PMF.bernoulli (p.1.toNNReal) (ENNReal.toNNReal_mono ENNReal.one_ne_top p.2.right)) true
      = ↑(p.1.toNNReal) := by
      simp [PMF.bernoulli_apply]
    -- 最後に coercion lemma を使って p.1 に戻す
    simp [hb, h_coe]
}

該当箇所と #check #print 内容です。分析解説。

以下、提示された箇所の要点と動作・使っている補題の意味、証明の流れを日本語で解説します。必要に応じて補題名や型の説明を交えます。

  1. tsum_fintype の役割と与件

  • 定理宣言（簡略化）：
    ∀ {α β} [AddCommMonoid α] [TopologicalSpace α] {L : SummationFilter β} [L.LeAtTop] [Fintype β] (f : β → α),
    ∑'[L] b, f b = ∑ b, f b

  • 直感：β が有限型（Fintype）で、適切な summation filter（ここでは L.LeAtTop が仮定されている）を取るとき、非可算級の無限和 tsum（トップロジーの下での無限和）と Finset の和（∑ : Finset.univ.sum）が一致する、という典型的な補題です。

  • 証明の構造（与えられた自動生成っぽいコードの読み取り）：

    • tsum_eq_sum（または同様の補題）に帰着している。

    • 「ある条件が真である（of_eq_true）」ことを示して、tsum_eq_sum の前提（例えば「非零項の集合が有限である」など）を満たしているとする形になっています。

    • 要するに「Fintype の下では（ほとんど自明な）有限性条件が成立するので tsum = finset.sum」が出る、という証明です。

  1. pmfBoolEquivUnit の全体像

  • 型：PMF Bool ≃ Set.Icc (0 : ENNReal) 1
    → Bool 上の確率分布（PMF）が、ENNReal の区間 [0,1]（閉区間）と同型になることを示しています。

  • toFun：PMF μ を probTrue μ（= μ true と同じ）だけ取り出して、それを Set.Icc の要素（subtype）にする。

    • 具体的には ⟨probTrue μ, ⟨0 ≤ probTrue μ, probTrue μ ≤ 1⟩⟩ を返す。

    • 上の 0 ≤ μ true は ENNReal の zero_le で即時。

    • μ true ≤ 1 は μ true + μ false = 1 から単純に導けます（右辺で tsum_fintype を使って tsum = finset.sum としている）。

  • invFun：p : Set.Icc 0 1 を受け取って PMF.bernoulli を作る。

    • パラメータは p.1.toNNReal（ENNReal → NNReal の toNNReal）。

    • 引数の第二要素は ENNReal.toNNReal_mono ENNReal.one_ne_top p.2.right で、p.2.right が p.1 ≤ 1 という仮定から NNReal 側での上界証明を作るための変換です。

  1. left_inv（toFun ∘ invFun = id） の流れ

  • goal：任意 μ : PMF Bool に対し invFun (toFun μ) = μ を示す（構成体ごとの同値）。

  • PMF.ext を使い、各ブール値 b ∈ {true, false} について成分ごとに示す。

  • b = true の場合：

    • Bernoulli による true 成分は ↑( (μ true).toNNReal ) になっており、μ true は PMF なので ⊤（無限大）にはならない。従って ENNReal.coe_toNNReal (PMF.apply_ne_top μ true) により ↑( (μ true).toNNReal ) = μ true が成り立つ。

    • よって真成分は元に戻る。

  • b = false の場合：

    • μ false は μ true から 1 を引いたものであることを示す必要がある：

      • まず tsum_fintype を使って tsum (fun b => μ b) = (Finset.univ : Finset Bool).sum (fun b => μ b) を得て、これを使って μ true + μ false = 1（hsum）を得る。

      • μ true は ⊤ でないので h_true : μ true = ↑(μ true).toNNReal を得る。

      • μ false も ⊤ ではない（PMF.apply_ne_top μ false）。

      • hsum を交換して μ false + μ true = 1 とし、ENNReal.eq_sub_of_add_eq を使って μ false = 1 - μ true と表す（ENNReal の引き算の補題）。

      • さらに h_true を代入して μ false = 1 - ↑(μ true).toNNReal となるので、Bernoulli の false 成分と一致することが確かめられる。

  • まとめ：両成分で一致するから left_inv 成立。

  1. right_inv（invFun ∘ toFun = id） の流れ

  • goal：任意 p : Set.Icc 0 1 に対し toFun (invFun p) = p を示す（Subtype.ext による toFun の値の first 成分が等しいことを示せば良い）。

  • まず p.1 が ⊤ でないことを示す（さもなければ ⊤ ≤ 1 が導かれて 1 = ⊤ になり矛盾）。

  • その結果 ENNReal.coe_toNNReal h_ne_top により ↑(p.1.toNNReal) = p.1 が得られる（coercion と toNNReal の逆関係）。

  • Bernoulli の true 成分は ↑(p.1.toNNReal) なので、それと上の等式を合わせて toFun (invFun p) の first 成分が p.1 に等しいことが示される。

  • Subtype.ext, dsimp, simp により終了。

  1. 使っている主要補題・定理の説明

  • tsum_fintype：Fintype の場合に tsum = finset.sum を与える補題（今回重要な点は PMF の全確率 1 を finset.sum の形にできること）。

  • PMF.apply_ne_top：PMF の各成分は ⊤（無限大）にならない、すなわち有限（ENNReal の有限元）であることを示す補題。これにより toNNReal や coe_toNNReal が使える。

  • ENNReal.coe_toNNReal：x ≠ ⊤ のとき ↑(x.toNNReal) = x。（ENNReal と NNReal 間の変換の整合性）

  • ENNReal.toNNReal_mono：ENNReal の大小関係を NNReal の大小関係に運ぶ補題（p.1 ≤ 1 を NNReal 側の条件に変えるために使用）。

  • ENNReal.eq_sub_of_add_eq：ENNReal 上で a + b = c のとき b = c - a を与える補題（ただし a が ⊤ でない等の前提あり）。

  • PMF.bernoulli_apply（あるいは PMF.bernoulli の定義展開）：Bernoulli 分布の true/false 成分がどのような ENNReal の表現になっているかを示す。

  1. 実装上の注意と改善案

  • tsum_fintype は妥当な補題だが、PMF に関しては「PMF の総和が 1」であることを表す既存の補題（ライブラリにより命名は異なるが）を直接使えることが多いです。たとえば "μ.sum_to_one" 的な補題があるなら tsum_fintype を取り除いて直接使える場合があります。ただし、その補題が tsum を使っているのか finset.sum を使っているのかで差があるので、今回のように finset.sum = tsum の変換が必要になることがあります。

  • ENNReal / NNReal のやり取りでは toNNReal, coe_toNNReal, toNNReal_mono のような補題を適切に使い、必ず ⊤ でないこと（≠ ⊤）の証明を用意すること。PMF 側の apply_ne_top がこの役割を果たします。

  • 証明中で simpa や dsimp, simp を多用して短く整えることができます（提示例でも simpa を使って tsum_fintype の式から hsum を得ている）。

まとめ

  • 全体としてやっていることは単純で、Bool の場合は μ true を取れば μ が一意に決まり、その逆写像はその値をパラメータとする Bernoulli 分布にする、という自然な同型を形式的に示しています。

  • 技術的なポイントは ENNReal ↔ NNReal の変換と、有限個（ここでは 2 個）の和を tsum（無限和）から finset.sum に変換するところです。提示コードはこれらを正しく扱っており、使用している補題群（PMF.apply_ne_top, ENNReal.coe_toNNReal, ENNReal.eq_sub_of_add_eq, tsum_fintype など）は妥当です。

もし特に気になる箇所（tsum_fintype の内部の細かい式変形や、PMF 側の具体的な補題名の確認、または Lean のバージョン差に起因するエラー等）があれば、その箇所を指定してください。より詳細に掘り下げて説明します。

coe というのがありますね。

@[simp]
theorem tsum_coe (p : PMF α) : ∑' a, p a = 1 :=
  p.hasSum_coe_one.tsum_eq
theorem apply_eq_one_iff (p : PMF α) (a : α) : p a = 1 ↔ p.support = {a} := by
  refine ⟨fun h => Set.Subset.antisymm (fun a' ha' => by_contra fun ha => ?_)
    fun a' ha' => ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
    fun h => _root_.trans (symm <| tsum_eq_single a
      fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
  suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm
  classical
  have : 0 < ∑' b, ite (b = a) 0 (p b) := lt_of_le_of_ne' zero_le'
    (ENNReal.summable.tsum_ne_zero_iff.2
      ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩)
  calc
    1 = 1 + 0 := (add_zero 1).symm
    _ < p a + ∑' b, ite (b = a) 0 (p b) :=
      (ENNReal.add_lt_add_of_le_of_lt ENNReal.one_ne_top (le_of_eq h.symm) this)
    _ = ite (a = a) (p a) 0 + ∑' b, ite (b = a) 0 (p b) := by rw [eq_self_iff_true, if_true]
    _ = (∑' b, ite (b = a) (p b) 0) + ∑' b, ite (b = a) 0 (p b) := by
      congr
      exact symm (tsum_eq_single a fun b hb => if_neg hb)
    _ = ∑' b, (ite (b = a) (p b) 0 + ite (b = a) 0 (p b)) := ENNReal.tsum_add.symm
    _ = ∑' b, p b := tsum_congr fun b => by split_ifs <;> simp only [zero_add, add_zero]

theorem coe_le_one (p : PMF α) (a : α) : p a ≤ 1 := by
  classical
  refine hasSum_le (fun b => ?_) (hasSum_ite_eq a (p a)) (hasSum_coe_one p)
  split_ifs with h <;> simp only [h, zero_le', le_rfl]
theorem toOuterMeasure_apply_eq_one_iff : p.toOuterMeasure s = 1 ↔ p.support ⊆ s := by
  refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩
  · refine by_contra fun hs => ne_of_lt ?_ (h.trans p.tsum_coe.symm)
    have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
    have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
    exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s)
      (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa
  · classical suffices ∀ (x) (_ : x ∉ s), p x = 0 from
      _root_.trans (tsum_congr
        fun a => (Set.indicator_apply s p a).trans
          (ite_eq_left_iff.2 <| symm ∘ this a)) p.tsum_coe
    exact fun a ha => (p.apply_eq_zero_iff a).2 <| Set.notMem_subset h ha

このあたりを使うということでしょうか？

はい。要点は tsum_fintype に頼らず PMF 側の補題を使うことです。PMF.tsum_coe（p.tsum_coe）と PMF.toOuterMeasure_apply_finset / PMF.toOuterMeasure_apply を組み合わせれば、SummationFilter の暗黙引数問題を回避できます。下は該当箇所を置き換える提案パッチです。

// ...existing code...
      have hsum : μ true + μ false = 1 := by
        calc
          μ true + μ false = (Finset.univ : Finset Bool).sum (fun b => μ b) := by simp
          _ = μ.toOuterMeasure (Finset.univ : Finset Bool) := by
            rw [PMF.toOuterMeasure_apply_finset μ (Finset.univ : Finset Bool)]
          _ = ∑' b, (Finset.univ : Set Bool).indicator μ b := by
            rw [PMF.toOuterMeasure_apply μ (Finset.univ : Set Bool)]
          _ = ∑' b, μ b := by simp
          _ = 1 := μ.tsum_coe
// ...existing code...
      have hsum : μ true + μ false = 1 := by
        calc
          μ true + μ false = (Finset.univ : Finset Bool).sum (fun b => μ b) := by simp
          _ = μ.toOuterMeasure (Finset.univ : Finset Bool) := by
            rw [PMF.toOuterMeasure_apply_finset μ (Finset.univ : Finset Bool)]
          _ = ∑' b, (Finset.univ : Set Bool).indicator μ b := by
            rw [PMF.toOuterMeasure_apply μ (Finset.univ : Set Bool)]
          _ = ∑' b, μ b := by simp
          _ = 1 := μ.tsum_coe
// ...existing code...

簡単な説明：

  • μ.tsum_coe は ∑' b, μ b = 1 を与える補題（PMF 定義からの補題）なので最終的な 1 への帰着に使う。

  • Finset.univ.sum = μ true + μ false は simp で簡約できる。

  • Finset 側の和と無限和を繋ぐのに tsum_fintype を使う代わりに、PMF.toOuterMeasure_apply_finset / PMF.toOuterMeasure_apply を経由して等式をつなげることで SummationFilter の暗黙引数に依存しない形にしている。

この差分で lake build が通るか確認してください。必要ならさらに小さく手直し案を出します。どうしますか？

以下でビルドが通りました。

    intro b
    cases b
    case true =>
      -- true 成分は定義通り
      -- μ true は PMF によって ⊤ にならないので ENNReal の toNNReal と逆変換で元に戻せる
      have : ↑((μ true).toNNReal) = μ true := ENNReal.coe_toNNReal (PMF.apply_ne_top μ true)
      simp [probTrue, this]
    case false =>
      -- false 成分は和が 1 であることから決まる
      have hsum : μ true + μ false = 1 := by
        calc  -- calc version
          μ true + μ false = (Finset.univ : Finset Bool).sum (fun b => μ b) := by simp
          _ = μ.toOuterMeasure (Finset.univ : Finset Bool) := by
            rw [PMF.toOuterMeasure_apply_finset μ (Finset.univ : Finset Bool)]
          _ = ∑' b, (Set.univ : Set Bool).indicator μ b := by
            rw [PMF.toOuterMeasure_apply_finset μ (Finset.univ : Finset Bool)]
            simp only [Set.indicator_univ]
            -- Finset.sum と tsum の一致は tsum_fintype で得られる
            rw [tsum_fintype]
          _ = ∑' b, μ b := by simp
          _ = 1 := μ.tsum_coe

ビルド通ったのは良いですね。補足・簡潔化案を挙げます。

あなたの証明は正しいですが、false 成分のところで PMF.toOuterMeasure_apply_finset を何度も使っているのは冗長です。Bool は有限なので簡単に tsum_fintype を使って直接 tsum に変換し、μ.tsum_coe を使えば短く書けます。例えばこんな感じがシンプルです:

intro b
cases b
case true =>
  have : ↑((μ true).toNNReal) = μ true := ENNReal.coe_toNNReal (PMF.apply_ne_top μ true)
  simp [probTrue, this]
case false =>
  calc
    μ true + μ false = ∑' b, μ b := by simp [tsum_fintype]
    _ = 1 := μ.tsum_coe

あるいは simp にまとめても良いです:

case false => simp [tsum_fintype, -Finset.sum, μ.tsum_coe]

補足:

  • ENNReal.coe_toNNReal (PMF.apply_ne_top μ true) の部分は、μ true ≠ ⊤ を PMF.apply_ne_top で与えられるので妥当です。

  • 元の長い calc はわかりやすさのために残すのはありですが、短く書ける箇所は短くすると保守しやすくなります。

必要ならさらにリファクタ例を出します。

了解しました — 詳細に残しておく方針、とても良いと思います。simp に依存した自動推論はバージョンや他の定義の追加で挙動が変わりやすく、見えない依存関係を生みやすいので、冗長に書いておくことで将来の障害発見がずっと楽になります。

参考までに、今後のメンテナンスや将来の仕様変更に備えるための実践的なポイントを挙げておきます。

  • 当面は冗長な証明を残す

    • 明示的なステップを残すことで、どの等式・帰結に依存しているかが可視化されます。後で簡潔化する際にも安全に置き換えられます。

    • 置き換える前に元の（冗長な）証明をコメントや別名で保管しておくと安心です。

  • simp の適用範囲を限定する

    • simp に任せる場合は、global な simp ルールの追加・変更で挙動が変わるため、必要な補題だけを列挙して `simp only [...]` 的に限定するのが安定します。

    • あるいは局所的に `by simp [foo, bar]` のように、明示的に使う補題を指定すると予期せぬ副作用を防げます。

  • simp ルールの付与は慎重に

    • `@[simp]` を付けると便利ですが、汎用的すぎる simp ルールは他の証明を壊すことがあります。副作用を考えて付与しましょう。

    • 大きな変更をする際は、どの新しい simp ルールが既存の証明へ影響するかを確認してください。

  • 内部の処理を可視化する工夫

    • 証明の途中に中間補題（命名しておく）を挟むと、どの等式が重要なのかが分かりやすくなります。

    • 可能であれば、簡潔な証明（例：`by simp`）と冗長な証明の両方を用意し、コメントで切り替え方法を残しておくと便利です。

  • CI とバージョン固定

    • ライブラリやツールチェーンの更新で突然壊れることがあるので、CI で定期的にビルド・テストを回し、必要ならバージョンをピン留めしておくと安心です。

必要なら、該当の証明を一緒に見て

  • どの箇所が simp に依存しているかを切り出したり、

  • 冗長な証明を簡潔な one-liner（by simp 等）に安全に置き換える手順を作ったり、

  • または影響が出にくい simp-only の形に書き換えたり

といった作業を手伝えます。お気軽に該当箇所（抜粋）を貼ってください。原因究明の共有、こちらこそありがとうございました。


AI 提案 Lean コードが一度でも、そのまま貼って動いた試しがない…。✍️

いいなと思ったら応援しよう！

D. 🐺賢狼👨‍✈️Copilot のご飯代を、私には🍺代を。 または 宇宙式 $N+u^d=(P+u)^d$ を使って新しい発見を！