次が基本概念：
- 色々なレベルのコンテキスト
- ステージ（リーズニングの状態）
- フォーカス（リーズニング中に注目している判断または問題）
- ターゲット（判断または問題の項と型）
コンテキストには：
- ライブラリ（知識ベース）のコンテキスト
- ステージのコンテキスト
- フォーカスのコンテキスト
組織化に関して、一般論とLeanでは：
| 一般 | Lean |
|---|---|
| ライブラリ | ライブラリ／パッケージ |
| ステージ | モジュール／セクション |
| フォーカス | 関数・定理定義／let文 |
表現可能と文字列化可能
#eval で値〈要素〉を表示するには、型が型クラス Repr の型インスタンスでなくてはならない。
文字列化できるためには、型が型クラス ToStrng の型インスタンスでなくてはならない。
ツールチェーンの実行可能ファイル
バージョン 3 の lean 3.23.0
- lean.exe
- leanchecker.exe
- leanpkg
- leanpkg.bat
- libgcc_s_seh-1.dll
- libgmp-10.dll
- libstdc++-6.dll
- libwinpthread-1.dll
バージョン4のクリスマスイブ版 nightly-2022-12-24
- clang.exe
- lake.exe
- ld.lld.exe
- lean.exe
- leanc.exe
- leanmake
- libLLVM-15.dll
- libc++.dll
- libclang-cpp.dll
- libleanshared.dll
- lld.exe
- llvm-ar.exe
- zlib1.dll
動画とスライドから
https://www.youtube.com/watch?v=QI-fEXSX1BA 2分30秒くらい
progress has been super-slow.
進捗は非常に遅い、と。
https://leanprover.github.io/talks/vu2019.pdf P.9 ：
Connection between modules, packages, and namespaces in Lean 3 is not very clear
だよね、不明確！
モジュール・インポートの候補としては次があったようだ。実現されなかったが。
import "init/data/set" import "mathlib/data/set"
名前空間の構造と挙動が分かりにくい。
namespace Nat def one := 1 #eval one -- 1 end Nat #eval one -- error #eval Nat.one -- 1
open Nat namespace Nat def one := 1 #eval one -- 1 end Nat #eval one -- 1 #eval Nat.one -- 1
なお、特定の名前だけを現名前空間にぶちまけるには open Except (ok error) が使える。
関数のタクティクによる定義
def f1 : Nat → Nat → Nat := by exact (fun (n m: Nat) => n + m) #check f1 def f2 (n: Nat): Nat → Nat := by intro m exact n + m #check f2 def f3 (n m: Nat): Nat := by exact n + m #check f3
モジュールパス解決とLean.findOLean
Leanサーバーは、環境変数LEAN_PATHなしでも、./lake-packages/some-package/build/lib/ の下を見ることは知っているようだ。import Foo は ./lake-packages/some-package/build/lib/Foo.olean をロードする。Lean.findOLean が役に立つ。
#eval Lean.findOLean `名前
ここ半年くらいの非互換〈破壊的〉変更
- lean_packages/ が lake-packages/ になった。
- lean_packages/manifest.json が lean-manifest.json になった。
- 属性 @[defaultTarget ...] が @[default_target ...] になった。
- lean-toolchain がなくてもよかったが、ほぼ必須になった。ない場合はたぶんデフォルト。
証明とリーズニングとLean
| 一般 抽象的 | Lean 具体的 |
|---|---|
| ライブラリコンテキスト | プレリュードとインストールしたパッケージ達 |
| ワーキングコンテキスト | モジュール／名前空間／セクションのコンテキスト |
| 質問コンテキスト | 未証明定理の前提 |
| 判断コンテキスト | 既証明定理の前提 |
続・証明とリーズニング
コンテキストの階層は、外から内に向かって：
- ライブラリコンテキスト＝知識ベース
- ワーキングコンテキスト＝ステージコンテキスト
- 判断コンテキスト または 問題コンテキスト
コンテキスト＝混合コンテキストには次のものが格納される。情報の重複がある。自動導出は、関数定義／定理定義からの導出。
| 型宇宙 | 命題宇宙 |
|---|---|
| 関数定義 | 定理定義 |
| ラベルの結果型宣言 | ラベルの結果命題宣言 |
| （上に同じ）型の要素変数宣言 | （上に同じ）命題の証拠変数宣言 |
| 関数名のプロファイル宣言（自動導出） | 定理名のシーケント宣言 |
| 計算項の結果型宣言（自動導出） | 証明項の結果命題宣言（自動導出） |
| 関数名への計算項割り当て（自動導出） | 定理名への証明項割り当て（自動導出） |
| 定義的等式 ≡（自動導出） | 定義的同値式 ≡（自動導出） |
| 関数名からボディへの書き換え規則（β変換） | 定理名からボディへの書き換え規則（β変換） |
関数定義 (f := t) : Γ |- A から次が導出される。
- f: Γ |- A 関数名のプロファイル宣言
- t : A 計算項の結果型宣言
- f := t 関数名への計算項割り当て
- f ≡ t 定義的等式
- f ~→ t, f a ~→ t[a/x] 関数名からボディへの書き換え規則（β変換）
関数名のプロファイル宣言は次のようにパッキング〈レイフィケーション〉される。
- f: Γ |- A プロファイル宣言
- f^ : |- Γ→A 右辺は依存アロー型のプロファイル宣言
- f^ : Γ→A 項の結果型宣言
パッキング〈レイフィケーション〉の結果は、コンテキスト項目〈フィールド〉になれるので、コンテキスト拡張に使える。
用語法：
- (結果＝戻り値)＠型宇宙、(結果＝結論)＠命題宇宙
注意：
カリー／ハワード／ランベック対応を使うときは、形容詞に「圏論的」「型理論的」「集合論的」「論理的」などを使うほうが安全。例：型理論的アロー型、論理的含意命題、圏論的指数対象。
構造体と名前空間とドット記法
これって、昔Catyでやろうとしていたこと（一部はやった）ことだ。
structure LatticePoint2D where
x: Int
y: Int
#check LatticePoint2D
def LatticePoint2D.moveBy (p : LatticePoint2D) (u v:Int) : LatticePoint2D :=
{
x := p.x + u
y := p.y + v
}
#check LatticePoint2D.moveBy
#check ({x:=0, y:=3} : LatticePoint2D)
#check LatticePoint2D.moveBy {x:=0, y:=3} 3 2
#eval LatticePoint2D.moveBy {x:=0, y:=3} 3 2 -- エラー：プリントできない
#check ({x:=0, y:=3} : LatticePoint2D).moveBy 2 3 -- OK
証明とリーズニング
次の3つを混同しない！
- 定理のボディ（関数定義のボディ相当）
- 証明項
- リーズニング
リーズニング：
| バックワード | フォワード |
|---|---|
| 背景知識ベース | 背景知識ベース |
| リーズニング・ステージ | リーズニング・ステージ |
| ステージ・コンテキスト | ステージ・コンテキスト |
| 問題〈ゴール〉 | 判断 |
| 問題のコンテキスト | 判断のコンテキスト |
| 問題のターゲット命題 | 判断のターゲット命題 |
| 問題の未知項 | 判断の既知項 |
| 自明問題（終状態の問題） | 自明判断（始状態の判断） |
| リーズニング・ステップ | リーズニング・ステップ |
| タクティク | コンビネータ |
| 還元、分解 | 合成、生成 |
| タクティク・スクリプト | コンビネータ・スクリプト |
ちなみに、定理のヘッドは、定理名（オプショナル）とシーケント〈プロファイル〉からなる。定理のヘッドまたはシーケント〈プロファイル〉を定理のステートメントともいう。
バックワードリーズニングは、リーズニングの開始状態のセットアップが明確かつ簡単。それに対して、フォワードリーズニングは、状態の定義が曖昧で難しくなる。フォワードリーズニングが機械に向かない事情だろう。
パッケージとビルドで確認すべきこと
- cat lean-toolchain
- elan toolchain list
- elan show だとダウンロードが始まる
- cat lakefile.lean
- cat .git/HEAD デタッチされているか？
- git branch
- git rev-parse カレントブランチ
- git tag
- git rev-parse $(git tag | tail -1)
- git log --oneline
- git rev-parse $(git log --oneline | head -1 | cut -f1 '-d ')
- git checkout コミットのハッシュ
- cat lake-manifest.json | jq -c '.packages[]|.git|[.name, .url, .rev]'
- /bin/find -name '*.c' -or -name Makefile
最近のパッケージでは次があるはず。
- lean-toolchain
- lakefile.lean
- lake-manifest.json
これだけ揃っていればビルドできる可能性が高い。
外部Cソースをコンパイルするには cc コンパイラードライバーが、標準的なCLIで使える必要がある。gccでも大丈夫かもしれないが、clangが安心だろう。
Powershellのパイプ
Powershell では、foo |& bar も foo 2>&1 | bar も効かない。標準エラー出力を tee でファイルに落とすのは現状分からない。
bashなら次が出来るが、Powershellの代替は見つからないでいる。
lake build -v |& tee $(date +%Y-%m-%d_%H-%M-%S).lake-build.log
パッケージのビルド（失敗）
次のパッケージをトップレベルパッケージ（依存パッケージではなく）git clone でインストールする。
- "leancolls" : https://github.com/jamesgallicchio/leancolls
インストールしてすぐ気がつくのは：
- ./lean_packages/ というディレクトリがある。./lake-packages/ ではない。
- ./lean_packages/manifest.json がある。./lean-manifest.json ではない。
- lean-toolcahin は leanprover/lean4:nightly-2022-10-09
- lakefile.lean 内の属性が @[defaultTarget]、@[default_target] ではない。
- lakeバージョンは、Lake version 4.0.0 (Lean version 4.0.0-nightly-2022-10-09) 。パッケージ指定のツールチェーンのバージョン。
lake -v build すると、
LeanColls > lake -v build info: > git fetch origin # in directory .\lean_packages\std error: .\lean_packages\std\lakefile.lean:9:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean:12:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean: package configuration has errors
./lean_packages/ の下に、mathlibとstdがコピーされている。
LeanColls > cat .\lean_packages\mathlib\lean-toolchain leanprover/lean4:nightly-2022-10-09 LeanColls > cat .\lean_packages\std\lean-toolchain leanprover/lean4:nightly-2023-01-10
mathlibはバージョンがあっているが、stdが新しいのでダメだ。古いlakeでは、変更された属性 @[default_target] が解釈できない。
stdのビルドを、./lean_packages/std/ で手動で行う。成功。
LeanColls/ に昇って、lake build（実際は lean-build.ps1）すると、同じ失敗。既にビルド済みなのに、自分でビルドしようとする。拉致が開かない。いや、ビルドするじゃなくて、依存グラフを作ろうと試みて失敗か。lakefile.lean の構文が変わると破綻する。
stdのバージョンは昔のものにすればいけるかも。git log で探して、git checkout ハッシュ値でデタッチトヘッドを作る。
std > git checkout 6488a2a Previous HEAD position was 5770b60 feat: support priorities in ext (#84) HEAD is now at 6488a2a chore: update nightly 09-11 (#7) std > git branch * (HEAD detached at 6488a2a) main
lakefile.lean の属性は @[defaultTarget] だ。
LeanColls/ に昇って、lake build（実際は lean-build.ps1）する。gitでリビジョンを戻されてしまった。
LeanColls > lean-build info: > git fetch origin # in directory .\lean_packages\std info: updating .\lean_packages\std to revision 5770b609aeae209cb80ac74655ee8c750c12aabd info: > git checkout --detach 5770b609aeae209cb80ac74655ee8c750c12aabd # in directory .\lean_packages\std info: stderr: Previous HEAD position was 6488a2a chore: update nightly 09-11 (#7) HEAD is now at 5770b60 feat: support priorities in ext (#84) error: .\lean_packages\std\lakefile.lean:9:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean:12:2: error: unknown attribute [default_target] error: .\lean_packages\std\lakefile.lean: package configuration has errors
std > git branch * (HEAD detached at 5770b60) main
(HEAD detached at 5770b60) は最新版のデタッチトヘッド。
もし、lean_packages/manifest.json が効いているなら、
{ "url": "https://github.com/leanprover/std4", "rev": "a7237a4a4a7dd520ba1425295306bc1b4f754577", "name": "std", "inputRev": "main" }
以下のコミットがダウンロードされるはず。
commit a7237a4a4a7dd520ba1425295306bc1b4f754577
Author: Mario Carneiro <di.gama@gmail.com>
Date: Sun Oct 9 08:14:29 2022 -0400
feat: RBMap.{filter, sdiff}
なんかおかしいが、よくわからん。
ちなみにツールチェーンは：
LeanColls > elan toolchain list leanprover-community/lean:3.23.0 leanprover-community/lean:nightly leanprover-community/lean:stable leanprover/lean4:nightly leanprover/lean4:nightly-2022-07-06 leanprover/lean4:nightly-2022-10-09 leanprover/lean4:nightly-2022-11-20 leanprover/lean4:nightly-2022-12-02 leanprover/lean4:nightly-2022-12-16 leanprover/lean4:nightly-2022-12-22 leanprover/lean4:nightly-2022-12-24 leanprover/lean4:nightly-2023-01-10 leanprover/lean4:stable (default) leanprover/lean4:v4.0.0-m5
ツールチェーンを削除しようとしたら、
LeanColls > elan toolchain uninstall leanprover/lean4:nightly-2022-10-09 info: uninstalling toolchain 'leanprover/lean4:nightly-2022-10-09' error: could not remove 'install' directory: 'C:\Users\m-hiyama\.elan\toolchains\leanprover--lean4---nightly-2022-10-09' info: caused by: アクセスが拒否されました。 (os error 5)
elan のデフォルトを最新のナイトリィビルドにして、新しく作った use-Cli-2/ で作業した。
use-cli-2 > lean-build error: dependency Cli of ﾂｫuse-cli-2ﾂｻ not in manifest, use `lake update` to update use-cli-2 > lake update cloning https://github.com/mhuisi/lean4-cli to .\lake-packages\Cli error: .\.\lake-packages\Cli\lakefile.lean:6:2: error: unknown attribute [defaultTarget] error: .\.\lake-packages\Cli\lakefile.lean: package configuration has errors
やはり、バージョンのミスマッチでビルドできない。
いろいろと小技
コマンドライン：
- lean --print-prefix
- lean --print-libdir
- lake print-paths | jq .
- jq . ./lake-manifest.json
- cat .git/HEAD
- cat ~/.elan/update-hashes/* | sort
エディタ：
- #eval Lean.findOLean `Name
- #check と #eval で InfoViewをよく見る。
- set_option （下）
set_option trace.Elab.definition true set_option pp.universes false set_option pp.notation false set_option pp.coercions true
