2023-01-21

elanは別名を認識できない

Lean ダメ出し tips

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

対策は、lean-toolchain を手で書き換えること。

2023-01-21

lakeの再帰的なビルドと手作業でのビルド

Lean ハマリ所 tips

lakeはnpmほどには洗練されてないみたいだ。現状では完全な自動ビルドは無理な気がする。原因不明な失敗をすることがある。

ビルドの手順は、原理的には次のようなことだと思う。

./lean-toolcahin を見て、ツールチェーンがインストールされてなければ、elan toolchain install でツールチェーンをインストールする。
lakefile.lean の require を見て、依存関係〈dependency〉を知る。現パッケージが依存しているパッケージを ./lake-packages/ の直下に git clone する。原始的だが、grep require で依存しているパッケージは分かる。
クローンしたパッケージの lakefile.lean の require を見て、依存しているパッケージを ./lake-packages/ の直下にクローンする。現状、入れ子の構造は作らないようだ。./lake-packages/ の下にすべてのパッケージがフラットに並ぶ。
再帰的な検索とクローンにより、依存しているパッケージは ./lake-package/ の下を探せばある（揃っている）状態を作る。
すべてのパッケージの lakefile.lean を読んで依存関係グラフを作る。サイクルがあったらどうする？
依存関係グラフの末端から順にパッケージ単位でビルドする。
ビルド時に、既にビルド済みのパッケージのディレクトリ ./lake-packages/pkg/build/, ./lake-packages/pkg/build/lib/ などを、ツールに指定して、依存関係を解決してあげる。
各パッケージごとに必要とするツールチェーンもlakeバージョンも違うので、各パッケージごとにOSのプロセスとして別なlakeを起動する必要がある。

lakeの実行

コマンドラインで：

> lake build -v | tee "$(date +%Y-%m-%d_%H-%M-%S)_build.log"

これは、Git BashでもPowershellでもOK。Powershellのteeは Tee-Object の別名だが特に問題ない。

Gig Bash：

alias 名前
alias 名前=文字列
unalias 名前
alias lean-build="lake build -v | tee \$(date +%Y-%m-%d_%H-%M-%S).lake-build.log"

Powershell：

alias 名前または get-alias 名前
set-alias 名前文字列
remove-item alias:名前
下のスクリプトファイル

# lean-build.ps1
lake build -v | tee "$(date +%Y-%m-%d_%H-%M-%S).lake-build.log"

Powershellでは、lakeからの出力がないとルグファイルが作られないが、Git Bashではサイズ0のファイルが作られる。

パッケージバージョンの確認

信用できるのは、gitコミットのハッシュ値だけ。./laka-manifest.json に正確なバージョン（ハッシュ値）が書いてある。

{"git":
  {"url": "https://github.com/mhuisi/lean4-cli",
    "subDir?": null,
    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
    "name": "Cli",
    "inputRev?": "nightly"
  }
}

この例で：

url: gitリポジトリのURLは "https://github.com/mhuisi/lean4-cli"
subDir?: サブディレクトリ指定はなし。リポジトリ全体（コミットのルートから下全部）がパッケージの内容物となる。
rev: パッケージのgitコミットのハッシュ値
name: パッケージ名、この名前でサブディレクトリが作られる。コンフリクトする可能性あり。
inputRev?: パッケージのブランチやリリースの名前

git cloneしたコミットのハッシュ値は次のようにして求める。

$ git branch
* master

$ git rev-parse master
ecad15071973627f08ce7af018100fdbee566654

lakeがダウンロードして ./lake-packages/ の下にいれたパッケージでは、HEADがデタッチされている。

$ git branch
* (HEAD detached at 5a858c3)
  main

$ cat .git/HEAD
5a858c32963b6b19be0d477a30a1f4b6c120be7e

HEADが指しているコミットは、たいてはタグが付いている。最後〈最新〉のタグがパッケージのリリースバージョンになっていることが多いが、いつでもそうとは限らない。タグよりハッシュ値ベースで確認する。

$ git tag | tail -1
v2.1.0-lnightly-2022-11-20

$ git rev-parse $(git tag | tail -1)
5a858c32963b6b19be0d477a30a1f4b6c120be7e

2023-01-20

elan show でダウンロードをはじめる

Lean ハマリ所

プロジェクトディレクトリ内で elan show すると、そのプロジェクトのツールチェーンがダウンロードしてないと即座にダウンロードをはじめる。困ったもんだ。

elan toolchain list を使うべし！

lake build しても必要ならダウンロードして、elanツールチェーンリストに追加する。

VSCodeも、Leanプロジェクトの.leanファイルを開いた時点で、elanによるツールチェーンのインストールとlakeによるビルドを始める。が、ビルドはなかなかうまくいかない。

2023-01-19

全称記号の使い方と内部変形

Lean 具体例

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 : α, F x × G x) : (∀ y : α, F y) :=
 fun y : α => (h y).fst

variableの包摂〈取り込み〉すると：

def f'' (α : Type) (F G : α → Type) (h : ∀ x : α, F x × G x) : (∀ y : α, F y) :=
 fun y : α => (h y).fst

圏論的プロファイル形式を書くと：

f'' :
 (α : Type), (F G : α → Type), (h : ∀ x : α, F x × G x) 
 |- (∀ y : α, F y)

内部的に次のように変形される。

f'' :
 (α : Type), (F G : α → Type), (h : (x : α) → F x × G x) 
 |- (y : α) → F y

2023-01-19

constantがなくなった

Lean ハマリ所 tips

Lean 4ではキーワードを整理したらしく。

constantが廃止されて、axiomのみを使うようになった。
Πが廃止されて、∀のみを使うようになった。
assumeが廃止されて、funまたはλのみを使うようになった。
variables は廃止。variable が使える。
parameter, parameters って使えたっけ？ともかく廃止（使えない）。

2023-01-19

要素＝ポインター、一般化要素＝セクション

Lean ハマリ所 tips

Leanマニュアルでは "object" も使っているが、混乱のもとなので「要素〈element〉」を使う。「インスタンス」も混乱のもとなので使わない。「型の要素」を使う。

型の要素が命題の証拠〈witness〉に対応する。次はセクションの定義：

variable (F : Type → Type)
variable (s : ∀(X : Type), F X)
#check s Nat

セクション s は、パイ型のセクション。このパイ型は型族（型引数を持つ型）の総称型／多相型と言っていい。セクションは総称型〈多相型〉の一般化要素になる。

(要素：型 ) の一般化が (一般化要素 : パイ型)

要素はポインターで、一般化要素はセクション。

命題の型宇宙では：

(証拠：命題) の一般化が (一般化証拠 : 全称命題)

命題〈型〉と証拠〈ポインター〉、あるいは証明〈関数〉を区別する。命題には命題演算〈コネクティブ〉があり、証明〈定理〉には証明のコネクティブがある。

証明〈計算〉から証明〈計算〉を作る手続き〈メタ計算〉を重視する構成的論理で考える。証明〈計算〉に関するメタ計算がリーズニング。

2023-01-18

格納形式と表示形式

Lean ハマリ所

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
#check f4
#eval f1 3 4
#eval f2 3 4
#eval f3 3 4
#eval f4 3 4

check による表示では：

f1 (n m : Nat) : Nat
f2 (n _a : Nat) : Nat
f3 (_a _a1 : Nat) : Nat
f4 (_a _a1 : Nat) : Nat

ここで、アンダースコア始まり変数は、もとラムダ変数。シーケント記法だと：

f1 : (n m : Nat) |- Nat
f2 : (n _a : Nat) |- Nat
f3 : (_a _a1 : Nat) |- Nat
f4 : (_a _a1 : Nat) |- Nat

つまり、フル・アンカリー化して表示する。だが、内部的にはフルカリー化している。

f1 : |- Nat → Nat → Nat
f2 : |- Nat → Nat → Nat
f3 : |- Nat → Nat → Nat
f4 : |- Nat → Nat → Nat

よって、内部的はすべての関数は同じ形式になっていて区别が付かない（名前が異なるだけ）。呼び出し形式も戻り値も同じになる。次の点が分かりにくい。

表示はフル・アンカリー化する。
内部的な格納形式はフル・カリー化する。
呼び出しは、フル・カリー化関数を呼び出す。

def s1 (n: Nat) : Nat := n + 1
def s2 : Nat → Nat := fun (n:Nat) => n + 1

#check s1
#check s2

def valAtZero (f:Nat → Nat) : Nat := f 0
def valAtZero2 : (Nat → Nat) → Nat := fun (f:Nat → Nat) => f 0
#check valAtZero
#check valAtZero2

#eval valAtZero s1
#eval valAtZero s2
#eval valAtZero2 s1
#eval valAtZero2 s2

↑で、定義形式に関わらずフルカリー化関数が格納されて呼び出されることが分かる。表示においては定義形式の影響を受けるが、内部に格納されている関数自体は定義形式の影響を受けない。

そもそも、インラインで関数を書くときは、フルカリー化する以外の方法がない。

2023-01-18

判断と問題

Lean 半形式証明スクリプト本編ネタ

problem Γ ok? （コンテキスト Γ は正しいか？）
judgement Γ ok （コンテキスト Γ は正しい）
problem Γ |- t ok? （項 t は、コンテキスト Γ で解釈できるか？）
judgementm Γ |- t ok （項 t は、コンテキスト Γ で解釈できる）
problem Γ |- ?t : A （型 A である項 ?t を求めよ）
judgement Γ |- t : A （項 t は型 A である）
problem Γ |- t : ?A （項 t の型を求めよ）
judgement Γ |- t : A （再度：項 t は型 A である）
problem Γ |- t : A ok? （項 t は型 A であるか？）
judgement Γ |- t : A （三度目：項 t は型 A である）
problem Γ |- A ok? （型 A である項が存在するか？）
judgement Γ |- A ok （型 A である項が存在する）
existential judgement Γ |- A （型 A である項が存在する）

代表的かつ重要な問題：

型検証問題： problem Γ |- t : A ok? （項 t は型 A であるか？）
型推論問題： problem Γ |- t : ?A （項 t の型を求めよ）
項構成問題： problem Γ |- ?t : A （型 A である項 ?t を求めよ）

ソルバーソフトウェア：

型検証問題 → 証明検証系
型推論問題 → 結論抽出系
項構成問題 → 自動証明系

2023-01-18

Windowsのコンソールとショートカットキー問題

記録ハマリ所

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.exe は0バイトでダミーだった。

二番目のwt.exeは実体がある。他に、WindowsTerminal.exeもあるが何故か実行できない。わからん。

それとショートカットキー問題。Alt+Ctrl+B をMSYS2のBashターミナルに割り当てたが、firefoxにフォーカスのときに Alt+B でMSYS2のBashターミナルが起動される。わからん。

wt.exe（ダミー）へのリンクをデスクトップに作って、ALT+Ctrl+Tで起動するようにしたが、あいかわらず毎回プロセス起動になる。

2023-01-18

言霊による誤解・違和感・抵抗感

半形式証明スクリプト本編ネタ

命題は型である。← そんなわけないだろ。
命題は型の一種である。
[間違い] 命題はデータ型の一種である。
命題とデータ型は違う。が、命題は型の一種である。
命題は広義の型の一種である。
命題は広義の型の一種であり、データ型も広義の型の一種である。
命題は命題の型宇宙に居て、データ型はレベル0の型宇宙に居る。

2023-01-18

不明瞭なところ色々

Lean 半形式証明スクリプト本編ネタ

矢印の奪い合い問題

含意を表す
指数型〈関数型 | アロー型〉を表す
射のプロファイルの区切り記号
シーケントの区切り記号（前提と結論）

暫定的解決

含意と指数はカリー／ハワード対応により同一視して → を使う。
射のプロファイルの区切り記号にターンスタイル $`\vdash`$（\vdash）を使う。
射はバンチ複圏〈bunched multicategory〉の複射でもよい。バンチとして依存レコード〈テレスコープ〉を考えることが多い。
射のプロファイルとシーケントは同義語として、シーケントの区切り記号もターンスタイル〈turnstile〉を使う。

定義による効果：コンテキストの拡張・増大

定義によって何が生成されるか？これも曖昧。

define function x:A := t

に対して、次の6つのモノが混合コンテキストに追加される。

declared name x : A
confiermed typing t:A
assigned body x := t
registered equation x ≡ t
registered conversion x ~~> t

これらの追加〈append〉のためには、validityが必要。

名前が構文的に正しい名前である。
型項が構文的に正しい型項である。
値項が構文的に正しい項である。
型付け〈タイピング〉が正しい。

これらの検証〈チェック〉作業が終わると、コンテキストに追加されて、結果的にコンテキストが膨らむ。次の作業は、膨らんだコンテキストに基づいてなされる。

等号の奪い合い問題

定義的等号〈definitional equality symbol〉
命題的等号〈propositional equality symbol〉
述語記号〈predicate symbol〉
n-圏のn-射

次のようにする。

定義的等号： ≡
命題的等号： =
述語記号： eq
n-圏のn-射： ⇒ などの次元付き矢印記号と id-アノテーション

他に、一般的同値関係は～で表す。

判断、問題、解の区别

区別してない。

型つけ判断： judgement Γ |- t:A
型つけ問題： problem Γ |- t:?A
項構成問題： problem Γ |- ?t:A
存在判断： existential judgement Γ |- A
問題の解： solution of problem Γ |- t:?A
問題の解： solution of problem Γ |- ?t:A
問題の解： solution t of problem Γ |- t:A
問題の解： solution A of problem Γ |- t:A
相対判断： providing Γ judgement Δ |- t:A
相対問題： providing Γ problem Δ |- ?t:A
相対問題の解： providing Γ solution of problem Δ |- ?t:A

項構成問題に対して、順行ソルバーと逆行ソルバーがあり、ソルバーをプログラムとして作ることをソルバー・プログラミングと呼ぶ。特に、項が証明項のときの逆行ソルバーのプログラミングはタクティク・プログラミング。

事実と予告

宣言文が環境としての事実の宣言と、今後やることの予告の宣言がある。

declare defined succ: Nat |- Nat
declare defining add: Nat, Nat |- Nat

自然言語風に書くと：

it's already defined succ: Nat |- Nat
we will define add: Nat, Nat |- Nat

引数渡しとカリー化後の適用演算

f: A |- B と f': |- (A → B) があるとき、a: |- A に対して、

a;f = a▷f = f◁a = f' a （ベータ等式）

f |→ f' というカリー化はコアージョンとして組み込まれている。その結果、カリー化したモノの名前はオーバーロードされる。

コロンの奪い合い問題

圏論： f: プロファイルでプロファイル宣言
型理論： a: 型で型つけ宣言〈タイピング宣言〉
(型理論 a:型) ⇔ (圏論 a: 1 |- 型)
圏論のプロファイル宣言は、フルカリー化して型理論のタイピング宣言にする。ここで齟齬が生まれる。

2023-01-18

Windowsショートカットキー

記録 tips

「CTRL+ALT+P」で Powershell だったのだが、この設定は：

[Win]+[Q] から Powershell を探す。
[ファイルの場所を開く] でディレクトリを見る。
"Windows Powershell" がリンクになっているので、プロパティを見る。
プロパティのショートカットキー項目に「CTRL+ALT+P」が指定されている。

デスクトップにある Gi Bash へのリンクには、「CTRL+ALT+S Shell」が定義されていて有効ではある。

以前、「CTRL+ALT+P」に Bash を指定していたが今は何も設定されてない。MSYS2の"MSYS2 MSYS" に「CTRL+ALT+B Bash」を指定してみた。が、これも毎回プロセス起動で、フォーカスだけチェンジが出来ない。Windowsの仕様が変わったようだ。

アプリケーション側で、フォーカスチェンジに反応しないと新プロセス起動となるのかも知れない。

2023-01-18

MSYS2

その他ソフトウェア tips

久しぶりで色々忘れている。

MSYS2のルート / は C:\msys64\
MSYS2の /c/ は C:\
したがって、/c/msys64/ は /
/ucrt64/, /mingw64/, /clang64/ と、それらの32ビット版があるが、当初はダミーで空っぽ
clang32.exe, clangarm64.exe, mingw64.exe, ucrt64.exe, clang64.exe, mingw32.exe がある。それぞれの開発環境ごとのシェルということらしい。
プレーンなシェルとして、msys2.exe がある。
clang64.exe と msys2.exe で作業したい。
今は空っぽなので、現物を入れるには pacman を使うようだ。
/bin/mintty.exe と /bin/bash.exe が主要なインターフェース。
/msys2_shell.cmd をジックリ読むと何か分かるかも。

2023-01-17

演算子の優先度

Lean tips

src/Init/Notation.lean からの情報。

構文範疇precは項の優先度を表す値（の表現）のことで：

項の優先度： max = 1024, arg = 1023, lead = 1022, min = 10
パイプ記号 <|, |> は優先度は min = 10
=, ∈ が50
足し算は65、
規表現風接尾辞の *,+,? は arg = 1023

Swiftの演算子がよく整理されている。Leanの値は後で埋める。

演算子	説明	結合律	優先順位	Lean
<<	左ビットシフト	無結合	160
>>	右ビットシフト	無結合	160
*	乗算	左結合	160
/	除算	左結合	160
%	剰余	左結合	160
&	ビットAND	左結合	160
+	加算	左結合	140	65
-	減算	左結合	140
縦棒	ビットOR	左結合	140
^	ビットXOR	左結合	140
<	未満	無結合	130
<=	以下	無結合	130
>	より上	無結合	130
>=	以上	無結合	130
==	イコール	無結合	130	50
!=	ノットイコール	無結合	130
~=	パターンマッチ	無結合	130
&&	論理AND	左結合	120
二本縦棒	論理OR	左結合	110
?:	三項条件	右結合	100
=	代入	右結合	90
=	乗算と代入	右結合	90
+=	加算と代入	右結合	90
&:&=	論理ANDと代入	右結合	90

優先度のグループ分けは：

BitwiseShiftPrecedence << など 160
MultiplicationPrecedence * など 160
AdditionPrecedence + など 140
RangeFormationPrecedence ... など 135
CastingPrecedence is など 132
NilCoalescingPrecedence ?? など 131
ComparisonPrecedence = など 130
LogicalConjunctionPrecedence && など 130
LogicalDisjunctionPrecedence || など 120
TernaryPrecedence ?: など 100
AssignmentPrecedence = など 90

130代が混みすぎ。

2023-01-17

binOpの自然数版

Lean 具体例

演算子優先度〈prec〉は適切かどうかわからない。

infix:70 "←" => Nat.pow

#eval 5 ← 2 -- 25

def sqPow (n:Nat) : Nat := n ← (n * n)
#eval sqPow 2 -- 16

lakeの実行

パッケージバージョンの確認

矢印の奪い合い問題

定義による効果： コンテキストの拡張・増大

等号の奪い合い問題

判断、問題、解の区别

事実と予告

引数渡しとカリー化後の適用演算

コロンの奪い合い問題

定義による効果：コンテキストの拡張・増大