Lean #02 - 2025/09/14
https://lambda-kansai.connpass.com/event/368673/
方針変更
読み上げを paragraph 単位から section 単位に変更してみる
第2章 Lean による初めての証明
https://github.com/leanprover/elan
Elan はフランス語の普通名詞(一般名詞)に由来する
フランス語の発音わからん takezaki.icon ebi_chan.icon
zulipのスレを立ててもらった: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/pronunciation.20of.20.22elan.22/with/539403684
kakkun61.icon ディレクトリーの名前はプロジェクトの名前と同じことが必須なんだろうか
lakefile見るとファイル名を設定しているところがなくて、namespace名を指定しているように見える
自然数を自分で定義する
みんな論理式読めてるんですか?僕はLean始めたてのころ全然読めなかったんですがebi_chan.icon
私は記号論理の本を一冊読んで慣れました takezaki.icon
古いけど読みやすい。自然演繹を扱う。 https://www.nippyo.co.jp/shop/book/2703.html
kakkun61.icon TAPL で慣れた感じ
帰納法の原理は自然数の定義に含まれる
この定義は自然か?
自然数を定義しようとしているのに、「zero と succ を何度か適用したものにhogehogeが成り立つ」みたいなことを言うと曖昧だし循環論法になる
集合論を使う場合は「zero と succ で作れる最小の集合」みたいな定義ができる(?)
MyNatの定義だけ見ると、公理の1と2だけしか書いてないように見える。残りは?
A. あとで出てくる
spoiler: 現状の MyNat の定義で、ペアノの公理が満たされるような自然数が手に入っている
このように自然数を定義するのは計算的には非常に効率が悪いのですが、Lean では証明に使う定義と計算に使う定義を分けることができて、この問題を回避できます。
kakkun61.icon ほえー そのふたつの定義が一致するかどうかは人間の責任なんだろうなあ
そこをいじってる場合、証明時(型チェック時)は保証するけど実行時にどうなるかは知らん、というスタンスですねebi_chan.icon
code:lean
#check MyNat.succ
-- -> MyNat.succ (n : MyNat) : MyNat
#check @MyNat.succ
-- -> MyNat.succ : MyNat → MyNat
豆知識話したくて喋っちゃったけどいらんこと言ったかもしれない…ebi_chan.icon
ええんやで takezaki.icon
kakkun61.icon := を ≔ にするのはダメなんだ
x = y という記法は他で使ってるのでパーサの混乱を避けるためにそうしてると思います
ちなみにx = yはEq x yという表記のマクロになってます。気にしなくていいけど
kakkun61.icon あ、いや ≔ U+2254 っていう Unicode 文字もあるけど、そこは対応(?)してないんだなと
ほんとだ。ちゃんと見てなかったです。すいません。確かにそうですね。なんでなんだろう
これ 👇 でもいいらしい .zero → zero
code:lean
def MyNat.add (m n : MyNat) : MyNat :=
match n with
| zero => m
| succ n => succ (add m n)
なんならこっち 👇 でもいいらしい
code:lean
| .succ n => .succ (.add m n)
こう 👇 書いちゃうと zer 変数を束縛することになるのでタイポに弱い
コンストラクターだよって示すために .zero って書いておくといい
code:lean
| zer => m
なるほど takezaki.icon
#errata フィールド記法になっている p.20
#check コマンドの出力(上記ではボックスで表示しています)を見ると、等式「MyNat.one.add MyNat.one = MyNat.two」の型が Prop と表示されています。これは Lean における命題を表す型です。
証明行の左ガーターにダブルチェックが付くと証明ができてる
https://scrapbox.io/files/68c6c8958c6fa90c180a6d43.png
2.2.6
本書では 👇 だけど
code:lakefile.lean
lean_lib "LeanBook" where
kakkun61.iconが生成したときは
code:lakefile.lean
lean_lib «LeanBook» where
だった
ほんとですねebi_chan.icon
kakkun61.icon フランス流🤔
takezaki.icon そうなんだ
« » の記号は識別子に日本語とかの任意のUnicode文字列を使いたいに使う記号ですebi_chan.icon
" " で囲ってても問題は起きない気がするので、テンプレートがなぜこうなったかは分からない(調べなきゃ)
kakkun61.icon なあるほど
2.2.7
kakkun61.icon sorry おもろ
kakkun61.icon (n : MyNat) のところカーソルホバーすると説明出てきた
Explicit binder, like (x y : A) or (x y). Default values can be specified using (x : A := v) syntax, and tactics using (x : A := by tac).
デフォルト引数使えるんか... takezaki.icon
Leanの文法、バリエーションがくそ多いのでホバーで出てくる説明読むのは地味に大事ですね…ebi_chan.icon
code:lean
#reduce MyNat.add (n := .one) .one
↑みたいに、名前付き引数(関数定義で : の内側に書かれた引数)を使って関数に値を渡してやることもできます
次回 Lean #03 - 2025/09/21
2.2.7 の回答から
2025/09/21