git init 直後HEADの内容： ref: refs/heads/mainmainという名前はここで決定されて、その後も使われる。初期化しただけでは ./.git/refs/heads/ は空で、HEADの参照先である ./.git/refs/heads/main は存在しない。git add README.md しても見た目上の「リ…

The formal proof on the other side was a big and unreadable 'proof term' 出典： 不明、現在はインターネット上にないようだ。

証明図から証明項に引き写すのは手作業。支援系とかいいながら、ソフトウェアは何も支援してくれない。 /-! example_1.lean -/ namespace Imp def elim_right {A B: Prop} (f:A → B) (a:A) : B := f a def elim_left {A B: Prop} (a:A) (f:A → B) : B := f a…

証明図〈横棒図〉やストリング図を扱うこと、解釈すること。 順行リーズニング 柔軟な参照（固有名、固有ラベル以外の参照方法） 直示 位置による参照 曖昧参照 リーズニングの中断保留（未完成のままに保存） 順行リーズニングと逆行リーズニングを混ぜたリ…

命題の真偽判定： 白黒つける、決着をつける。どうやって？ 証明項の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行 証明項の生成工程〈リーズニングプロセス〉の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行 証明…

問題は、絵図で自明なことをどうやってテキストエンコードするか？ 論理絵図＝横棒図〈バー図〉 圏論絵図＝ストリング図 テキスト 論理絵図 圏論絵図 命題 命題 ワイヤー・ラベル 証拠ラベル バー・ラベル ノード・ラベル 証明項 横棒図 ストリング図 公理 …

次が基本概念： 色々なレベルのコンテキスト ステージ（リーズニングの状態） フォーカス（リーズニング中に注目している判断または問題） ターゲット（判断または問題の項と型） コンテキストには： ライブラリ（知識ベース）のコンテキスト ステージのコン…

#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…

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 c…

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サーバーは、環境変数LEAN_PATHなしでも、./lake-packages/some-package/build/lib/ の下を見ることは知っているようだ。import Foo は ./lake-packages/some-package/build/lib/Foo.olean をロードする。Lean.findOLean が役に立つ。 #eval Lean.findOL…

lean_packages/ が lake-packages/ になった。 lean_packages/manifest.json が lean-manifest.json になった。 属性 @[defaultTarget ...] が @[default_target ...] になった。 lean-toolchain がなくてもよかったが、ほぼ必須になった。ない場合はたぶん…

一般 抽象的 Lean 具体的 ライブラリコンテキスト プレリュードとインストールしたパッケージ達 ワーキングコンテキスト モジュール／名前空間／セクションのコンテキスト 質問コンテキスト 未証明定理の前提 判断コンテキスト 既証明定理の前提

コンテキストの階層は、外から内に向かって： ライブラリコンテキスト＝知識ベース ワーキングコンテキスト＝ステージコンテキスト 判断コンテキスト または 問題コンテキスト コンテキスト＝混合コンテキストには次のものが格納される。情報の重複がある。…

これって、昔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 } #c…

次の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…

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-…

コマンドライン： 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_o…

leanprover/lean4:stable と leanprover/lean4:v4.0.0-m5 という名前のツールチェーンは同じもので、名前だけが違う。どちらも、https://github.com/leanprover/lean4/releases/expanded_assets/v4.0.0-m5 からダウンロードされる。が、elanはそれに気付かず…

lakeはnpmほどには洗練されてないみたいだ。現状では完全な自動ビルドは無理な気がする。原因不明な失敗をすることがある。ビルドの手順は、原理的には次のようなことだと思う。 ./lean-toolcahin を見て、ツールチェーンがインストールされてなければ、elan…

プロジェクトディレクトリ内で elan show すると、そのプロジェクトのツールチェーンがダウンロードしてないと即座にダウンロードをはじめる。困ったもんだ。elan toolchain list を使うべし！lake build しても必要ならダウンロードして、elanツールチェー…

variable (α : Type) variable (F G : α → Type) def f : (∀ x : α, F x × G x) → (∀ y : α, F y) := fun h : ∀ x : α, F x × G x => fun y : α => (h y).fst関数ヘッドを変形すると： variable (α : Type) variable (F G : α → Type) def f' (h : ∀ x : α, …

Lean 4ではキーワードを整理したらしく。 constantが廃止されて、axiomのみを使うようになった。 Πが廃止されて、∀のみを使うようになった。 assumeが廃止されて、funまたはλのみを使うようになった。 variables は廃止。variable が使える。 parameter, par…

Leanマニュアルでは "object" も使っているが、混乱のもとなので「要素〈element〉」を使う。「インスタンス」も混乱のもとなので使わない。「型の要素」を使う。型の要素が命題の証拠〈witness〉に対応する。次はセクションの定義： variable (F : Type → T…

def f1 (n:Nat) (m:Nat) : Nat := n + m def f2 (n:Nat) : Nat → Nat := fun (m:Nat) => n + m def f3 : Nat → Nat → Nat := fun (n :Nat) => fun(m:Nat) => n + m def f4 : Nat → Nat → Nat := fun (n m:Nat) => n + m #check f1 #check f2 #check f3 #chec…

problem Γ ok? （コンテキスト Γ は正しいか？） judgement Γ ok （コンテキスト Γ は正しい） problem Γ |- t ok? （項 t は、コンテキスト Γ で解釈できるか？） judgementm Γ |- t ok （項 t は、コンテキスト Γ で解釈できる） problem Γ |- ?t : A （型…

wt.exe が2箇所にあった。 C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt.exe C:\Program Files\WindowsApps\Microsoft.WindowsTerminal_1.15.3466.0_x64__8wekyb3d8bbwe\wt.exe が、C:\Users\m-hiyama\AppData\Local\Microsoft\WindowsApps\wt…