Lean4: リファクタリング

２万行を超えるコードになってしまったので 🐺 AI も読むのが大変です。

hp_pos という補助補題

素数 p が０より大きいのか？これを毎度 Lean に教えなきゃいけない！
なんて面倒な！

$$
\Large
0\ <\ p \quad (p \in \mathbb{P})
$$

AI 生成コードによる例でも、毎回３～５行の証明コードを出します。
Mathlib4 には、標準で備わってないの？🤔

実は備わっている

Nat.Prime.pos

theorem Prime.pos {p : ℕ} (pp : Prime p) : 0 < p :=
  Nat.pos_of_ne_zero pp.ne_zero

なんで AI はコレを利用しないのでしょうかね？
質問してみると、存在は知っている。しかし、使わない。
コード中探してみると結構、遠回しに証明している（笑）→ Appendix

{p : ℕ} (pp : Prime p) という仮定パラメータによって p は素数と決まる。

素数に関する補題・定理を書く時は、だいたいこの仮定パラメータを書いてある。なので、この仮定を渡してあげれば、この定理が $${0 < p}$$ を返してくれる。

フック補題を書いておく

/-- lemma about the positivity of prime numbers -/
lemma prime_pos {p : ℕ} (pp : Nat.Prime p) : 0 < p := by
  exact Nat.Prime.pos pp

have hp_pos と、書き置きたい時は、これを呼べば良い。

状況により $${0 < p \in \R}$$ な実数素数（実数化した素数だけど整数です）
素数が計算でに利用される場合など実数化した素数を事前に示したいときに必要になる。そんな時は、以下の補題

lemma prime_rpos {p : ℕ} (pp : Nat.Prime p) : 0 < (p : ℝ) := by
  exact Nat.cast_pos.mpr (prime_pos pp)

違いは、

• 0 < (p : ℝ) で返す

• 証明は Nat.cast_pos.mpr (prime_pos pp) とすると認識してくれる

0 < p → 1 ≤ p

０を含まないなら自然数 p は 1 から上になりますが、Lean 君はバカ正直なので $${0 < p\ \ne\ 1 \le p}$$ は違うと言います。

だから、これも事前に補題として用意しておきます。

lemma prime_ge1 {p : ℕ} (pp : Nat.Prime p) : 1 ≤ p := by
  linarith [prime_pos pp]

lemma prime_rge1 {p : ℕ} (pp : Nat.Prime p) : 1 ≤ (p : ℝ) := by
  -- ℕ の 1 ≤ p から ℝ の 1 ≤ ↑p へ型を持ち上げる
  exact_mod_cast (prime_ge1 pp)

これに置き換えれば、全部１行になる✍️

仮定: {p : ℕ} [Fact p.Prime] (hp3 : p ≥ 3)

have hp_pos : 0 < (p : ℝ) := prime_rpos (Fact.out : Nat.Prime p)

公開する時には（？）きれいなコードになってしまうので今のうちに、こうして書き残しておかないと…。これらのコードは🐺賢狼が頑張って書いたコード。そこから学び、習得してからリファクタリングしないと…。

もったいない！！

2025/10/21 6:00

D.

#Lean #Lean4 #Mathlib #Mathlib4 #数学 #素数 #定理 #補題 #形式化証明

Appendix

様々だけど、これらも意味として大事である。とくに Lean の仕組みを学ぶには。いろんな書き方があるのだと知ることができる。それを、１つの記法にまとめてしまうと、学べることが減る。削ぎ落とされてしまう。残念…。

hp_pos 集

  have hp_pos : 0 < (p : ℝ) := by
    have h01 : (0 : ℕ) < (1 : ℕ) := by norm_num
    have hp_gt1 : 1 < p := lt_of_lt_of_le (by norm_num : 1 < 3) hp3
    have hnat : (0 : ℕ) < p := lt_trans h01 hp_gt1
    exact_mod_cast hnat

    have hp_pos : 0 < (p : ℝ) := by
      have hp : Nat.Prime p := Fact.out
      exact_mod_cast hp.pos

have hp_pos' : 0 < (p : ℝ) := by
  norm_cast; exact Nat.Prime.pos (Fact.out : Nat.Prime p)

have hp_pos : 0 < (p : ℝ) := by
  norm_cast; linarith [Nat.Prime.pos (by simp [P] at hp; exact (hp.2).1)]

have hpPrime : p.Prime := hp_filter.2.1
have hp_pos : 0 < (p : ℝ) := by exact_mod_cast Nat.Prime.pos hpPrime

      have hp_pos : 0 < (p : ℝ) := by
        have hp : Nat.Prime p := by
          let hf := Finset.mem_filter.1 hp
          rcases hf with ⟨_, ⟨hpPrime, _⟩⟩
          exact hpPrime
        exact_mod_cast hp.pos

      intro n hn
      simp [Finset.mem_filter, Finset.mem_Icc] at hn
      rcases hn with ⟨hnIcc, hbad⟩
      rcases hbad with ⟨p, ⟨hp_ge3, ⟨hpPr, hcond⟩⟩⟩
      have hp_pos : 0 < (p : ℝ) := by
        have hp : Nat.Prime p := hpPr
        exact_mod_cast hp.pos

これらのコードをそのままにしておくと AI に書かせた Lean コードだ！と、バレる！その界隈の人は、これらの特徴コードから判断できるっぽい。

とにかく自分で導き出さないと気がすまない。エレガントに書かなければ、気がすまない。そういう病の人には、これらのコード見ると蕁麻疹が出るらしい。可哀想…。

ビルド通れば、こんなんでも✅️OK

いつか Mathlib4 の記述仕様が変われば、これらがエラーを吐くだろう。
そんな検知器にもなる✍️