全称変数は、型宣言された変数で、その型の任意のモノを表す。任意変数と言ってもいい。$`\require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} } \newcommand{\for}{\Keyword{for } } \newcommand{\assume}{\Keyword{assume } } \newco…

曖昧表現は： 名前・記号の借用 例： G = (G, *, 1) 省略 例： G = (G, *) 名前・記号の多義的使用〈オーバーロード〉 曖昧表現の解決は、データベース検索。検索条件はパターンマッチ問題〈ユニフィケーション問題〉となる。パターンマッチ問題を解いて曖昧…

次の計算系がある。 計算対象物 CC圏 CC複圏 CC多圏 （広義）射 ◯ ◯ ◯ コンビネータ △ ◯ ◯ アレンジメント △ ◯ ◯ CCは Cartesian Closed ◯：うまく定式化できる。 △：ある程度は定式化できる。 演算： 射に対して： 結合、直積、カリー化、評価 コンビネータ…

ミクシン指標の導入と削除には、extends ではなくて、次を使う。 employs 宣言 ： 雇用する、採用する include ディレクティブ ： ミクシン（スニペット）を実際に挿入展開する dismisses 宣言 ： 解雇する、免責する。

/-! ファミリーと多項式 -/ /- →《《《《《《《《《《《《《《《《《《《《 → -/ namespace My /- 型コンストラクタ Fam -/ def Fam (X : Type) := X → Type abbrev FamOver := Fam variable (I : Type) (i j : I) variable (F G : FamOver I) def Sigm {X: …

一応できた。sectionは要らないみたい。 /-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a …

/- 用語： スタブ： from https://e-words.jp/w/%E3%82%B9%E3%82%BF%E3%83%96.html スタブとは、切り株、半券、（何かが減ったり短くなった）残り、などの意味を持つ英単語。ITの分野では、本物が用意できないときに動作に支障が無いようにとりあえず置いて…

/-! 写像と関係 -/ namespace My /- >>>>>>>>>>>>>>>>>>>>>>>>>>>>>> -/ section Logic def MP {A B: Prop} (p:A → B) (a: A) : B := p a def Inst {X: Type} {P: X → Prop} (w: ∀(x: X), P x) (a : X) : P a := w a def Cut {A B C : Prop} (p: A → B) (q: …

最後の行がエラー。 /-- 記法クラス -/ class LE (X : Type) where le : X → X → Prop scoped infix:50 "≦" => LE.le #check LE section LE_Test variable -- セミローカルコンテキストの導入 (A: Type) [LE A] (a b:A) #check a≦b end LE_Test /-- 全順序集…

区別するなら ◯、しないなら／出来ないなら ☓、無意味なら - 。プログラミング言語に関しては、定義時と呼び出し時で二つ。△はやる気になればやれるが、普通はやらない、ほぼ☓。 集合圏 デカルト閉圏 TypeScript Lean 4 関数と関数データ ◯ - ◯, ☓ ◯, ☓ 関数…

関数・定理の定義・記述 Γ |- ψ : A 型推論問題の質問 Γ |-? ψ : ? 項推論問題の質問 Γ |-? ? : A プロファイル宣言 Γ |- _ : A （アンダースコアは不定の意味） 単なる省略 Γ |- ψ : _ （不定だが、型推論で確定可能） ホムセット {f | f: Γ |- _ : A} 毎回…

判断・主張と質問・問題の区別ができること。 命題と事実と証拠と証明の区別が出来ること。 証明とリーズニングの区別が出来ること。 ローカル前提とグローバル・コンテストの区別が出来ること。 公理や前提と先送りの区別ができること。 コンテスト環境とバ…

ライブラリとバックログは双対的な存在。ライブラリ／パッケージ管理と同程度にバックログ管理機能が必要。現状、何もしてくれない。Idrisのholeがある程度はバックログ管理。

def FooRetType (b:Bool) : Type := match b with | false => Nat | true => String def foo (b: Bool) : FooRetType b := match b with | false => (1 : Nat) | true => "hello" #eval foo true #eval foo false

数学的帰納法のステップの部分。 section NatInd def sumto (n : Nat) : Nat := match n with | Nat.zero => 0 | Nat.succ m => (sumto m) + (Nat.succ m) def arith (n : Nat) : Nat := (n * (n + 1))/2 -- theorem target 跡地 theorem case_zero : sumto …

purely functional code ＝ pure code ＝ 純コード imperative code ＝ impure code ＝ 不純コード transpile to pure code ＝ purify ＝ 浄化 impure block ＝ Kleisli block impure function ＝ command impure program ＝ script impure program fragment…

def f5 (n : Nat) : Nat := by cases n exact 3 -- zero case exact 7 -- succ case #eval f5 0 --> 3 #eval f5 1 --> 7 example : f5 0 = 3 := rfl -- by も要らない！？ example : f5 5 = 7 := rfl example : f5 2 = 7 := by exact Eq.refl 7

inductive Eq : α → α → Prop where /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the equality type. See also `rfl`, which is usually used instead. -/ | refl (a : α) : Eq a a /- recursor Eq.rec.{u, u_1} : {α : Sort u_1} →…

def toNum (b : Bool) : Nat := by cases b with | true => exact 1 | false => exact 0 #print toNum #print Bool.casesOn #eval toNum true --> 1 def toNum' (b : Bool) : Nat := by cases b exact 1 exact 0 #eval toNum' true --> 0 def toNum'' (b : B…

rflは exact Eq.refl 項 の略記。適切な項は見つけてくれる。 theorem t1 (y : Nat) : (fun x : Nat => 0) y = 0 := by rfl theorem t2 (y : Nat) : (fun x : Nat => 0) y = 0 := by exact Eq.refl 0A = A の形でないとターゲットに適用できない。カーネルに…

/-- 自然数に関する帰納原理 -/ theorem NatIndPrinciple (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n := by intro n cases n · exact hz · apply hs /-- 自然数に関する帰納原理を with付きで書いてみる -/ theorem NatIndPrincipl…

() はUnit型の唯一の要素。 (3) は 3 のこと。型 Nat (3, 4) はペア型 Nat×Nat (3, 4, 5) は Nat×Nat×Nat (3, 4, 5) = (3, (4, 5)) 右結合的な二項演算子 .1 は .fst、.2 は .snd ⟨カンマ区切り項目並び⟩ は構造体リテラルの略記。フィールド名を省略できる…

関数適用は必ず空白が必要。空白類が適用演算子の記号だから。一方、x.2 や x[3] のようなタプル／リスト／配列へのアクセスは、空白を入れてはダメ。空白が適用演算子なので、適用として解釈されてエラーになる。だいぶハマる。

シンボル上にマウスホバーでツールチップが出る。 シンボル上でホバーから[ctrl+click]で定義元にジャンプ。 必要なら[shift+ctrl+enter]でインフォビューをON/OFF とりあえず[F12]だが、トンチンカンな所に飛ぶことがある。 [alt+←]で戻る。 [alt+F12]でpee…

inductiveな型と同名の名前空間を定義して、そのなかにstuffを入れる。以下は実例： structure Parser.Category namespace Parser.Category /- ... ... -/ end Parser.CategoryLeanのキモのひとつは、名前空間／シンボル空間の構造と相互作用を理解すること。

def Obj := Type def Enricher := Type def Hom (α β : Obj) : Enricher := (α → β) structure EndoFunctor where obj : Obj → Obj -- 台型構成子＝対象パート hom : {α β : Obj} → (Hom α β) → (Hom (obj α) (obj β)) -- ホムパート #check @EndoFunctor.ho…

mathlib と Std.logic も必要。 論理記号 導入規則 除去規則 連言∧ And.intro And.left, And.right 選言∨ Or.intro_left, Or.intro_right Or.elim 否定￢ Not.intro Not.elim〈absurd〉 真T True.intro 通常の証明 偽⊥ 背理法の証明 False.elim 含意→ ラムダ…

スキーマ、タプル空間、タプルインスタンス、フィールド関数、テーブル structure Schema where fields : Type typeAssig : fields → Type def TupleSpace (S : Schema) := ((f : S.fields) → S.typeAssig f) inductive NameAge where | name : NameAge | ag…

Eq〈イコール〉の定義： inductive Eq : α → α → Prop where /-- `Eq.refl a : a = a` is reflexivity, the unique constructor of the equality type. See also `rfl`, which is usually used instead. -/ | refl (a : α) : Eq a aこの定義のリカーサー〈帰…