Lean4: 学習: 内部コードのコアと機械語

Lean を少しずつ理解しようと進めてはいます。

同時に、宇宙式の証明などを並行しつつ…。書けた証明があっているか？
自己検証ができないので「まだ理解できてない」というのが証明された…

（以下は別記してリンクする✍️）

Ｃ言語なら機械語アセンブラ翻訳機

プログラミング言語は Lean 含めすべて CPU が直接理解できる機械語という１６進数コード＝数値の羅列に翻訳されます。これを人間が理解しやすいようにニーモニック命令と値を紐づけて、読みやすくしたアセンブリ言語が、あります。

例: hello.c

#include <stdio.h>

int main()
{
    fputs("Hello, World!\n", stdout);
    return 0;
}

VS Code 画面

コンパイル

clang hello.c

a.out という実行ファイルが出来上がる。

実行

$ ./a.out 
Hello, World!

動きましたね。

機械語（マシン語）

これをコンピュータ (CPU) は、数値の羅列を解読して処理してます。

実行ファイルダンプ

適当にピックアップ
文字コード部分は、なんとなく解る。数値は慣れれば…読める…。
（Z80ならかろうじて覚えているかな…😅笑）

$ od -A x -t x4z -v a.out 
000000 464c457f 00010102 00000000 00000000  >.ELF............<
000010 003e0003 00000001 00001050 00000000  >..>.....P.......<
000020 00000040 00000000 000036f8 00000000  >@........6......<
000030 00000000 00380040 0040000d 001e001f  >....@.8...@.....<
000040 00000006 00000004 00000040 00000000  >........@.......<
000050 00000040 00000000 00000040 00000000  >@.......@.......<
...
001140 e5894855 10ec8348 00fc45c7 48000000  >UH..H....E.....H<
001150 2e72058b 8b480000 3d8d4830 00000ea4  >..r...H.0H.=....<
001160 fffecbe8 48c031ff 5d10c483 000000c3  >.....1.H...]....<
001170 fa1e0ff3 08ec8348 08c48348 000000c3  >....H...H.......<
...
002000 00020001 6c6c6548 57202c6f 646c726f  >....Hello, World<
002010 00000a21 3b031b01 00000028 00000004  >!......;(.......<
002020 fffff00c 0000005c fffff02c 00000084  >....\...,.......<
002030 fffff03c 00000044 fffff12c 0000009c  ><...D...,.......<

アセンブリコード

a.out`main:
->  0x555555555140 <+0>:  pushq  %rbp
    0x555555555141 <+1>:  movq   %rsp, %rbp
    0x555555555144 <+4>:  subq   $0x10, %rsp
    0x555555555148 <+8>:  movl   $0x0, -0x4(%rbp)
    0x55555555514f <+15>: movq   0x2e72(%rip), %rax
    0x555555555156 <+22>: movq   (%rax), %rsi
    0x555555555159 <+25>: leaq   0xea4(%rip), %rdi
    0x555555555160 <+32>: callq  0x555555555030 ; symbol stub for: fputs
    0x555555555165 <+37>: xorl   %eax, %eax
    0x555555555167 <+39>: addq   $0x10, %rsp
    0x55555555516b <+43>: popq   %rbp
    0x55555555516c <+44>: retq

lldb 画面上

これは、ダンプコードにあった文字列データ

6c6c6548 57202c6f 646c726f -> Hello, World

のある場所（アドレス）をセットして、画面に表示するライブラリ fputs を呼び出し、OSに渡して画面（コンソール）に出力する。を、

0x555555555160 <+32>: callq  0x555555555030 ; symbol stub for: fputs

この１行のコールで後はOS側のライブラリがやってくれます。

というコンピュータの内部構造の雰囲気を、まだコンピュータ内部事象を、知らない人に感じて知ってもらって…。以下の話が解るようになる？🤔

私も解ってないので、そういう所でもないか。純粋な数学知識も必要かなｗ

Lean4 コードはどうなっている？

Lean は、たしか LLVM ベースなので、ざっくり

という長い旅を経てソースコードは機械語に翻訳されています。
（今のコンピュータでは時間的には一瞬なんだけどね！）

Lean 自体は何で書かれている？

一番最初は Ｃ言語 系なのでしょうが、自身の言語が成熟すると、自分自身で機械語へと自立します。が、現代はもう LLVM というアセンブリ言語手前の共通言語がある時代なので、そこまでか、その手前の Clang に任せます。

そして現在は Lean 自体、ほぼ自身の言語 Lean で書かれているようですね。

Lean のアセンブリ言語までは読まない

流石に、アセンブリ言語を読んで Lean が何やっているかは調べません（笑）
じゃあ、何でアセンブリ言語を紹介した？😅

すべての言語の行き着くところは、アセンブリ言語→機械語 CPU 命令です。

Lean も同じなのでそこまで行けば、どんな動きしてるのかは追えます。
Lean を理解するのと、lldb でコードを追うのは意味が全く違います。

Ｃ言語の例では、短いプログラムがアセンブリコードと、ほぼ対ついになっているので、なんとなく解ります。その感覚を知ってもらうための一例

しかし、Lean は、

$$
\text{
Lean → Clang → LLVM → … → 機械語（CPU 命令数列）
}
$$

らしいので。

Clang → LLVM → 機械語では、さらにCPU毎の最適化が行われます。
つまり、省略されている部分が多くなり、一対一では、読めません。

よって、ここを読んでも仕方ないのです。読むなら、一段下の底レイヤーを読む必要があります。ここは、まだ純粋に、対になっている可能性があるので読みやすいはず…。

Lean の内部式 term

本題へやっと進みます。 term とは式で expr 結果ではないです。
つまり、評価前の構造、評価後の結果。という解釈です。

term 突入前に…

自作自然数を作って Lean で証明してみる

例に、自然数の定義と証明（例題・補題）を取り上げます。

自然数とはペアノの公理では、０ゼロを基点に後続する自身（単位など）が繰り返される構造です。

$$
\N = [0, 1, 2, 3, 4, 5, …]\\
これを\\
\N = \text{… (succ (succ (succ (succ (succ (zero))))))}\\
こう表現します。少々ややこしいですね。
$$

$${n = 123}$$ を、表現するのに zero から、次の次の次の次の…と１２３回も次々と後続を数えていって１２３で止める。正直言ってアホだよね🤣実際このネスト構造では大きな数でスタックオーバーフローを起こして目的の数を求められません。なので概念的なもので実用性はまったくゼロです。

Lean で自然数の型を定義して再現する

それを Lean で自作じさく自然数の型を定義するには、こう書きます。

inductive MyNat where
| zero : MyNat
| succ : MyNat → MyNat

• zero は、そのまま返す。※zero コンストラクタは Lean 側で既に定義されてるので 0, zero にマッチする。

• 後続 succ (succsessor) は、MyNat の後継を MyNat で返す。

これで自然数の数列を表現できるようになりました。しかし、このままでは数値としての意味はなく、MyNat というものが zero を基点に始まり、succ で続いて表現される。

$$
\text{
MyNat.succ(MyNat.succ(MyNat.succ(MyNat.succ(MyNat.zero))))
}
$$

と、返ってきます。
計算も出来ますが、数字では返ってこないです。これで返ってきます。

def add (m n : MyNat) : MyNat :=
  match m, n with
  | MyNat.zero, _ => n
  | _, MyNat.zero => m
  | MyNat.succ m', MyNat.succ n' => MyNat.succ (add m' n')

#eval add MyNat.zero MyNat.zero
  -- MyNat.zero -- 0 + 0 = 0 の意味
#eval add MyNat.zero (MyNat.succ MyNat.zero)
  -- MyNat.succ MyNat.zero -- 0 + 1 = 1 の意味
#eval add (MyNat.succ MyNat.zero) MyNat.zero
  -- MyNat.succ MyNat.zero -- 1 + 0 = 1 の意味
#eval add (MyNat.succ MyNat.zero) (MyNat.succ MyNat.zero)
  -- MyNat.succ (MyNat.succ MyNat.zero) -- 1 + 1 = 2 の意味
#eval add (MyNat.succ (MyNat.succ MyNat.zero)) (MyNat.succ MyNat.zero)
  -- MyNat.succ (MyNat.succ (MyNat.succ MyNat.zero))
#eval add (MyNat.succ (MyNat.succ MyNat.zero)) (MyNat.succ (MyNat.succ MyNat.zero))
  -- MyNat.succ (MyNat.succ (MyNat.succ (MyNat.succ MyNat.zero)))

結局、人間がゼロから数えることになる表記。

この Nat 演算が Lean の核となっている…。わけじゃない。一応、Lean 実装の Nat 定義もこう言う実装で証明されながら表面的に実装されている。

実際の計算は Nat 定義コメントに、こう書かれていて、

GMP: https://gmplib.org/ というライブラリが使われている。
Nat の数値計算処理は、このライブラリで行われ結果を Nat で返している。

内部では、実用的な実績あるライブラリで構築されている。Lean が証明支援系の特殊言語であるために便宜上（？）表面的にちゃんと立証しながら動作しているよ！という、ポリシー設計なのでしょう。

自作自然数も再現して、通るし、動くので証明支援系言語としてはちゃんと機能しているし、ちゃんとした言語なのです。ちゃんとしすぎて扱いづらい
（笑）

ゼロは自然数と定義する

/-- 1. 0は自然数 -/
def zero_is_natural : MyNat := zero

ここでは、自然数に０を含めるという意味で明確化しているだけです。
（０を含めない自然数 $${\N^+}$$ という定義集合もあります。）

例題で確かめる

例題：定義 zero_is_natural = zero と等しい。

example : zero_is_natural = zero := by rfl

by ～ によって証明する。
rfl とは、reflexivity のことで反射関係（＝自明）である。という略記です。

Lean が、それを確かめて、合ってます。となれば、この例題は成立する。

ようやく term の話につながる

by rfl で、何を証明したのか？正直、わかりません。
（この例は、非常に単純なので自明なのですが）

$$
\begin{array}{l}
\text{MyNat に zero の定義があり、MyNat.zero とそのまま返している。}\\
\text{zero は、MyNat.zero として存在している。}\\
\text{どちらも、比べたら同じである。}\\
\end{array}
$$

これを、具体的にどうやっているのかを見る方法があります。

by? ～ / show_term by ～

by? ～ とするか show_term by ～ とすると、rfl を、どのように展開して、立証しているのか教えてくれます。解らないと難問デバッグが大変です！

どの様になってたか？

具体的にはこのように展開されている事がわかりました。

example : zero_is_natural = zero := Eq.refl zero_is_natural

$$
\text{
Eq.refl zero\_is\_natural
}
$$

Eq.refl という処理に渡されてますね。
ちなみに rfl は、マクロ（？）で、色んな tactic（戦略）に繋がっています。

-- But, mostly for backward compatibility,
-- we try `eq_refl` too (reduces more aggressively)
macro_rules | `(tactic| rfl) => `(tactic| eq_refl)

今回はこれにマッチ？ eq_refl というのに流れていきます。
それが、たぶんこれですね。Eq.refl が出てきました。

/--
`rfl : a = a` is the unique constructor of the equality type. This is the
same as `Eq.refl` except that it takes `a` implicitly instead of explicitly.

This is a more powerful theorem than it may appear at first, because although
the statement of the theorem is `a = a`, Lean will allow anything that is
definitionally equal to that type. So, for instance, `2 + 2 = 4` is proven in
Lean by `rfl`, because both sides are the same up to definitional equality.
-/
@[match_pattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a

今度は、それは Eq a a つまり Eq zero_is_natural zero_is_natural として
Eq へ渡されている。
（※Lean ではカッコが省略されて、パラメータは空白区切りです。）

/--
The equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
-/
inductive Eq : α → α → Prop where
  /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the
  equality type. See also `rfl`, which is usually used instead. -/
  | refl (a : α) : Eq a a

一番下の

inductive Eq : α → α → Prop where
　| refl (a : α) : Eq a a

ここで評価されてますね。

反射的にどちらも同じ。数学では、P=N としても、P → N ∧ N → P が両方、言えないと同じと言わない。（P なら N = True かつ N なら P ＝True）is True

$$
(P \to N\ \land\ N \to P) \quad\Rightarrow\quad P \iff N
$$

やっと動きの流れが見えてきた…

show term のお陰で Lean の処理の流れを追いかける事が出来るようになりました。私のスタンスと言うか、この note で書いてる数学などの記事を、読み返せば解りますが、原理構造がどうなってそうなっているのか？
を調べていく内容が多く、完全解明まではしない（←お～い！）

とにかく、具体的な仕組みがわからないのが気持ちが悪いので、壊れた家電などバラして仕組みを学び取ってます（原因が解れば直しちゃう！）

１行プログラミング

なんか昔、楽しんだ呪文プログラム遊びは CODE GOLF という究極の遊びに発展しているようですね。元々は、少ないメモリのコンピュータに、どれだけ多くの要素を含んだコードが書けるか？という実用的な圧縮技術だったのですが。

たった数行で書けるのは、素晴らしい言語です。手数が少なくて済みます。
こうして自分や誰かのために説明を書くのが、異常に長くなるだけで（笑）

こっからが本題です！！

あれ？本題。今、終わったんじゃ…？

例に、宇宙式の証明をします！証明のコードは、ほぼ書き終えてる感じで。正しいのかどうかが自己判断で解らないんです（笑）コンパイル通っていても、数学的な厳密表現で示せていない。とか、いろいろボロが出ます。

宇宙式での代数的素数無限性の証明等に関しては、反射性の検証が怪しく、片方だけ成立していて、片方は成立してないっぽいです。素数が生まれると自然数が増えて、自然数が増えると新しい素数が必要になって、新しい素数が…と、交互に数を生むので、両者が無限になる。自然数だけが無限保証されていない。という原理構造が宇宙式にはあります。

単位宇宙式零
UnitCosmicFormulaZero

この関数は、どんな値も、どんな単位世界でも、素数と自然数の関係を意味を持って保ち、演算をちゃんと行って結果として、常に０を返す。という、数宇宙のバランスを示す関数式です。定数ではありません。結果としてゼロというパランス点を常に示した結果の定数です。これも、圏論レベルで最後まで証明しましたが…。この話とは別で、書きますね。

$$
0 = P(x;u) - N(x;u) - u^2
$$

これを展開して、

$$
f(x;u) = (x+u)^2 - x(x+2u) - u^2
$$

という関数にします。（詳細は別記の既存記事をリンク✍️）

それを Lean で以下のように定義しておきます。
（この時点ではゼロを返すかどうか解りません。演算した結果判明します。）

import Mathlib.RingTheory.Coalgebra.Basic

/-- 単位宇宙式ゼロ定数関数（任意の単位系においても常にゼロとなる関数）-/
def UnitCosmicFormulaZero (x u : Int) : Int :=
  (x + u)^2 - x * (x + 2 * u) - (u^2)

#eval という対話コマンドで、その場でわかります。
結果はコメントに書いておきます。

#eval UnitCosmicFormulaZero 0 0  -- → 0
#eval UnitCosmicFormulaZero 1 0  -- → 0
#eval UnitCosmicFormulaZero 2 0  -- → 0
#eval UnitCosmicFormulaZero 3 0  -- → 0
#eval UnitCosmicFormulaZero 0 3  -- → 0
#eval UnitCosmicFormulaZero 1 2  -- → 0
#eval UnitCosmicFormulaZero 2 1  -- → 0
#eval UnitCosmicFormulaZero 3 0  -- → 0

試したい人は、以下の Lean 4 Web にて。

右側に→ 0 が出力されると思います。

定理として証明する

/- 宇宙式ゼロ定数関数が常にゼロであることを示す定理 -/
theorem UnitCosmicFormulaZero_eq_zero (x u : Int) :
  UnitCosmicFormulaZero x u = 0 :=
  by
  unfold UnitCosmicFormulaZero
  ring

定理: UnitCosmicFormulaZero_eq_zero
UnitCosmicFormulaZero は x, u 整数を受け取り、結果として常にゼロと等しい関数である。

$$
\text{UnitCosmicFormulaZero}(x, u) = 0
$$

by ～ で、式を展開したりして、証明をしてます。

unfold （展開）が、色々やってくれます。

unfold の実装内容（さっぱり読めない！）

/-- "unfold " ident+ (location)? -/
@[builtin_tactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do
  let loc := expandOptLocation stx[2]
  for declNameId in stx[1].getArgs do
    go declNameId loc
where
  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext <| withRef declNameId do
    let e ← withoutRecover <| elabTermForApply declNameId (mayPostpone := false)
    match e with
    | .const declName _ =>
      withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
    | .fvar declFVarId =>
      unless ← declFVarId.isLetVar do
        throwError "tactic 'unfold' failed, local variable '{Expr.fvar declFVarId}' has no definition"
      withLocation loc (zetaDeltaLocalDecl declFVarId) (zetaDeltaTarget declFVarId) (throwTacticEx `unfold · m!"did not unfold '{e}'")
    | _ => throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"

そのあと
ring で、証明してるんですかね？
（こういうところちゃんと説明できてないので、私はまだ理解できてない。と証明されている）

ring の具体的処理内容（さっぱり読めない！）

/--
Tactic for evaluating expressions in *commutative* (semi)rings, allowing for variables in the
exponent. If the goal is not appropriate for `ring` (e.g. not an equality) `ring_nf` will be
suggested.

* `ring!` will use a more aggressive reducibility setting to determine equality of atoms.
* `ring1` fails if the target is not an equality.

For example:
```
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf
```
-/
macro (name := ring) "ring" : tactic =>
  `(tactic| first | ring1 | try_this ring_nf
  "\n\nThe `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
  \nNote that `ring` works primarily in *commutative* rings. \
  If you have a noncommutative ring, abelian group or module, consider using \
  `noncomm_ring`, `abel` or `module` instead.")
@[inherit_doc ring] macro "ring!" : tactic =>
  `(tactic| first | ring1! | try_this ring_nf!
  "\n\nThe `ring!` tactic failed to close the goal. Use `ring_nf!` to obtain a normal form.
  \nNote that `ring!` works primarily in *commutative* rings. \
  If you have a noncommutative ring, abelian group or module, consider using \
  `noncomm_ring`, `abel` or `module` instead.")

/--
The tactic `ring` evaluates expressions in *commutative* (semi)rings.
This is the conv tactic version, which rewrites a target which is a ring equality to `True`.

See also the `ring` tactic.
-/
macro (name := ringConv) "ring" : conv =>
  `(conv| first | discharge => ring1 | try_this ring_nf
  "\n\nThe `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
  \nNote that `ring` works primarily in *commutative* rings. \
  If you have a noncommutative ring, abelian group or module, consider using \
  `noncomm_ring`, `abel` or `module` instead.")
@[inherit_doc ringConv] macro "ring!" : conv =>
  `(conv| first | discharge => ring1! | try_this ring_nf!
  "\n\nThe `ring!` tactic failed to close the goal. Use `ring_nf!` to obtain a normal form.
  \nNote that `ring!` works primarily in *commutative* rings. \
  If you have a noncommutative ring, abelian group or module, consider using \
  `noncomm_ring`, `abel` or `module` instead.")

で、結果的には？

by ～ のあと、２行で済みました！👏

真実なので、証明できて当然ですが。

この２行の証明は具体的にどのようになっているのでしょうか…。

by → by? とすると term 展開されて見ることが出来ます。

❗️❓️

展開後のコード

展開後のコードを並べました！

なんと２００行を超えた巨大な関数になっている！

びっくりですね…。とても読めません。

そうです。これが、
（一部の戦術では、出力される用語は人間が判読できない場合があります。）

これは、Lean のアセンブリ言語と言ってもよいでしょう。構造ツリーです。
この構造が一致しているかを、証明でマッチさせて、立証しているのです。

この長い式 term でエラーが出て無ければ、これが合ってるという事です。
この命題より、次の話へ、証明へと展開していけます。

これが Lean の世界です。✍️

あとがき

ああ。そうか！これとマッチさせなければならないとなると…。
そりゃ、あの定理は書ききれてない。となるわけか。苦手な AI もこれを前提に、これに関する証明を書くことになる。先に教えなければいけないのか。

（一部の戦術では、出力される用語は人間が判読できない場合があります。）
AI ならば判読可能なのかなあ…。

これ全部見せて聞いてみたら、余裕で読めると返ってきた！
これをベースに戦略的証明式を展開できる可能性が大幅に上がると！（？）

これはLeanのアセンブリ言語だよ！とも言ってきて、この記事の紹介方法であってたかな（笑）

書きながら、少しは理解度が高まった。

2025/08/05  0:55

D.