$`\require{color} % 緑色 \newcommand{\In}{ \text{ in }} \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } } % 使用 \newcommand{\Let}{\Keyword{Let } }% 使用 \newco…

判断シーケント＝関数定義があるとする。$`\quad a : (\Gamma \vdash t : \beta)`$これを次のようにパックする。$`\quad (a : [\Gamma \to \beta], a := t^\wedge)`$ここで、$`t^\wedge`$ は項のフルカリー化。パックした定義は、環境コンテキストに追加でき…

$`\require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\Providing}{\Keyword{Providing } }% \newcommand{\When}{\Keyword{When } }% \newcommand{\And}{\Keyword{And } }% \newcommand{\Holds}{\Keyword{Holds…

単に「コンテキスト」は混合コンテキスト 純コンテキスト＝宣言コンテキスト 混合コンテキスト＝宣言と定義のリスト 定義は、宣言（x:A）と割り当て（x:=t）のペア シーケントは三種類： 判断シーケント、事実シーケント、質問シーケント 判断シーケントは、…

ムービーはデータ構造 ムービーはフレームとトランジションからなる。 フレームはステージの構造的な集まり。 ステージはツリー構造を持つ。カレントステージが一意に決まる。 ステージは、シーケントとサブステージの集まり。 シーケントは判断シーケントか…

宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予…

名前〈ラベル〉と型項のペアを型宣言、あるいは単に宣言と呼ぶ。型項は判断のパック形式〈packed form〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。宣言＝型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名…

帰納的型の値コンストラクタ記号 帰納的型の型名は、パラメータを持つと型コンストラクタ 構造体型は、単一の値コンストラクタを持つ帰納的型だが、フィールド名をコンストラクタとも言う。 オブジェクト指向のコンストラクタは、単元集合またはパラメータ集…

依存アロー型とパイ型は同じもの。アロー型＝指数型は依存アロー型の特別なもの。Lean 4 で依存アロー型の書き方が (x:α) → β （βは型項）となったが、Agdaでは以前からこの形だったようだ。 Π(x:α), β ≡ ∀(x:α), β ≡ (x:α)→β カリー化／アンカリー化は同じ…

postulate 公準 prerequisite 要請 assumption 仮定 antecedent 前件 premise 前提〈プロミス〉 hypothesis 仮説 context 文脈 environment 環境

型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。 型を型構成子で生成する。 要素を要素〈値〉構成子で生成する。要素生成子は関数である。 型の除去規則とは、型の消費規則で、関数による要素の構成規則（「構成」で間違ってない…

テキスト ピクチャー ラベル（名前) ワイヤー頂点 型（命題含む） 色付きワイヤー 項 ストリング図 宣言 入力端頂点とワイヤー コンテキスト ワイヤーパレット シーケント ノード 公理シーケント 展開不可能ノード 割り当て 展開可能ノード ステージ パレッ…

※ 2023-01-17に書いたけど投稿忘れ。関数型言語で、デカルト閉圏の射としての関数を表すことはできない。表わされるのは、関数型〈指数型〉の要素。要素をポインター関数とみなしても、表わされるのはポインター関数に限る。2つのポインター関数に対して、ev…

※ 2023-01-17に書いたけど投稿忘れ。演算子の優先度 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続きLeanの場合、まだ調整は必要かも知れない： PrefixSuffixPrecidence 1024 = max ArgumentPrecidence 1023 = arg CompositionPrecedence 90 ($`\circ`$) Exp…

散文化は prosify。 映像作品を、通常の文章に直して伝えること。 映像作品を鑑賞することは誰でも出来るが、ノベライズ／散文化は難しい。

「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断／質問を操作する。またステージ自体もコマンドで操作する。同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。全般的な管理…

型 ←→ 命題 ←→ 対象 関数（要素含む） ←→ 定理（証拠含む） ←→ 射 関数コンビネータ ←→ 定理コネクティブ？（言及も命名もされない） ←→ オペレーター／コンビネータ リーズニング・コマンド 対応物がないゲーム・コマンド 圏論的に整理するなら もの〈シン…

B -A が before, after のオプション。-B 3 -A 3 は単に -3 でも同じ。-C は -2 つまり -B 2 -A 2 と同じ。 mathlib > git branch * master mathlib > git rev-parse master 8618f40d51539454fe06511d5c8504a77f30c598 mathlib > grep -A 3 -B 3 8618 ..\..\…

structure PreOrder where U : Type le : U → U → Prop le_refl : ∀(x : U), le x x le_trans : ∀(x y z: U), (le x y ∧ le y z) → le x z inductive ab where | a | b def ab_le (x : ab) (y : ab) : Prop := match (x, y) with | (.a, _) => True | (.b, .…

set_option pp.notation true in #print Eq.trans set_option pp.notation false in #print Eq.transset_option pp.notation false in #check 1 + 3 set_option pp.notation true in #check 1 + 3

次を区別しなくてはならない。 命題 証明〈証拠〉 判断〈主張〉シーケント 質問〈問題 | 問い合わせ〉シーケント フォワードリーズニング（推論ルール含む） バックワードリーズニング（バックワード推論ルール含む） 定理は、証拠〈証明〉を引数として証拠…

混合コンテキストが、次のレベルで提供される。 ライブラリ パッケージ モジュール 名前空間 セクション 関数・定理（のボディブロック） 入れ子ブロック（by, doなど） これらの組織化機構〈organizing mechanism / feature〉は独立ではないし、一様でもな…

コード編集中に[F5]でデバッグモードになるが、Leanの場合は、デバッガやそのVSCode拡張が存在しないので、[F5]は効かない。

例： attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_commルート名前空間は無名だが、_root_ という名前で参照できる。

まず、 $ git clone https://github.com/xubaiw/Socket.lean $ cd Socket.lean $ cat lean-toolchain leanprover/lean4:nightly-2022-06-16 去年だと、「ふるっ！」と思う。 $ git branch * main $ git rev-parse main 9fc98bc24ccdb4471b2e38e94dccd18f75d2…

コントロール＋クリック "Cli" : https://github.com/mhuisi/lean4-cli 非依存 "leancolls" : https://github.com/jamesgallicchio/leancolls mathlib依存、ビルド失敗 "advent" : https://github.com/odomontois/advent2022-lean mathlib依存、ビルド成功 "…

npmのpackage-lock.json相当が、Lakeマニフェストファイル。lean_packages/manifes.json と lake-manifest.json がある。注意すべきはマニフェストファイル自体のバージョンで、JSONファイルのトップレベルフィールドとしてバージョン番号が記入されている。…

我々は、様々なレベルのコンテキスト（ライブラリ、モジュール／セクション）を行為〈activity〉により拡張していくのだが、拡張のための行為は二種類しかない。 関数定義 （λΠ計算ベース） 帰納的型定義 （CICベース） 関数定義は def で、帰納的型定義は i…

名前付き引数〈named arguments〉と引数省略時値〈default value〉の指定 def mySub (left right :Nat) : Nat := left - right #check mySub #eval mySub (right := 3) (left := 5) --> 2 def mySub' (left :Nat) (right:Nat := 1) : Nat := left - right #c…

apply は backward apply〈deapply | reverse apply〉の意味。だいぶ困る。 複数のゴールは左〈上〉から順に攻撃する。ツリー辿りは深さ優先再帰かな。 ゴールの固有名はないが、left, right のcaseラベルは付く。並びの順番でも参照できる。 ツリーが構成さ…