Lean4: かけ算の順序

かけ順問題…

Lean4 コーディングしていると、掛け算以外にも左右が逆で NG とか当たり前のように出くわして Lean4 って中学生未満かよ…って常に思うように…。

おバカちゃん！

$$
\large
1 \times a = a \times 1 \quad \to \quad a=a\ \to\ a
$$

これは Lean4 では、単純に同じとして認めない（笑）

こんなのが頻発するので、毎回「それはね、こうやって変換すると同じでしょ？」って教えてあげる必要がある。この例では、簡単な算術なので、

ring や simp で片付くが、結局内部では、

simp only [one_mul, mul_one, imp_self]

や

  rw [mul_one]  -- 1 * a = a
  rw [one_mul]  -- a = a

と、いちいち式を変形させて$${a=a}$$になるね。
同じだ！ Eq a a と Lean は、納得するのです。子供みたいでしょ（笑）

やってらんないわよ！！！！

ABC予想も、もう少しで（？）全体構成を繋いだ状態で内部証明も終わりそうなのだけど、この型が違う！同じじゃない！$${\N \to \R}$$ にして比べないとわからない！！とかもう…ね…。

素数 $${p}$$ だと事前に与えておいても $${p :\N \to p :\R}$$ としてしまったあと $${\uparrow p}$$ は $${p}$$ じゃないから「違う！」って言ってくる😂さっき $${\N}$$ だった $${p}$$ だよ…。

素数は自然数で実数にしても $${p = 7 → p = 7.0}$$ ってなるだけで変わらんだろ！！

疲れる…😓

もっと賢い Mathlib 作りたい…。

$ cat MathlibHello/ABC*.lean | wc -l
28094

ソースコード２万８千行超え（笑）

あとで解読のほうが大変になってきたわね…。

2025/10/20 18:44

D.

#Lean #Lean4 #Mathlib #Mathlib4
#算数 #数学 #かけ順問題