式〈項〉をギリシャ文字で書くとして α providing x:X, y:Y のような形がproviding式。これは、 within {x:X, y:Y} α assuming x:X, y:Y α と同じだが、providing, justificatin は定義義務／証明義務が発生する。providingで導入された宣言は、バックログ（…

翻訳： let → we_have := → by_using, because_of return → we_conclude, we_showed suffice let/return式 let x1: A1 := τ1 let x2: A2 := τ2 ‥‥ return α: C end別な書き方： we_have x1: A1 by_using τ1 we_have x2: A2 by_using τ2 ‥‥ we_conclude C by_…

論理記号 導入規則 除去規則 ∧ And導入 And除去左, And除去右 ∨ Or導入左, Or導入右 Or導入 ⇒ Imp導入 Imp除去 T True導入 (通常の証明) ⊥ (背理法による証明) False除去 ￢ Not導入 Not除去 1 And intro 基本証明 2 And elim left 基本証明 3 And elim righ…

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

index signature インデックス型： {[k : T] : S} の形で書ける型 いや違う、オブジェクト型やマップ型のインデックス集合の型を index signature と言っているのかな。 indexed access 型： T[K] という二項の型演算、または型演算で作られる型。特定の型や…

digraph { logic[label="形式化された\n定義／公理／定理／証明"] ts[label="TypeScript\nプログラムコード"] js[label="JavaScript\nプログラムコード\n(不要)"] logic -> ts[label=" 人手で相互翻訳", dir=both] ts -> js[label=" トランスパイラが翻訳 "]…

And_intro And intro And_left And elim left And_right And elim right Or_inl Or intro left Or_inr Or intro right fun_OR_MAKE なぜか無い 後で定義 Or elim 特殊 Imp intro MP（不要だが） Imp elim trivial True intro EFQ False elim 不要 Not intro …

アロー関数とアロー〈二重矢印記号〉を使った関数空間型の記述 declareを使った外部環境の型宣言 オンライン・プレイグラウンド 対応： TypeScript 疑似言語 function theorem const evidence declare function axiomatic theorem declare const axiomatic e…

型と値は区別する必要がある。 計算と演算を区別するのは難しい。曖昧に区別されていることもあるが、混同して使っても差し支えない。 関数と計算は一応区別するが、ヘッド部（後述）の有る無しの違いしかないので、混同して使っても差し支えない。 型と型の…

テーゼ： 十分に強力な型システム／型チェッカーを持ったプログラミング言語は、証明記述／証明検証に使える。 型 命題 型変数 命題変数 型定数 命題定数 型構成子 命題結合子 型の値 命題の証拠 計算・関数 証明・定理 計算・関数のプロファイル 証明可能性…

digraph { label="proof" subgraph cluster_not_a { label="not_a" h[shape=triangle] And_left h -> And_left[ label="￢A∧￢B"] } subgraph cluster_not_b { label="not_b" h1[shape=triangle, label="h"] And_right h1 -> And_right[ label="￢A∧￢B"] An…

全部事実上同義語。 平叙文 疑問文 型判断 型質問 シーケント 質問シーケント 関数定義 関数定義要求 定理記述 定理証明要求 クロージャ 大きいラムダ式 大きいタプル 大きいlet式

theorem half_DeMorgan premise h: ￢A∧￢B entails ￢(A∨B) proof we have not_a: ￢A by using And_left with h we have not_b: ￢B by using And_light with h we conclude ￢(A ∨ B) by using Or_tuple with not_a and not_b end 定理 ド・モルガンの半…

数学的帰納法のステップの部分。 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 …

$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\hyp}{\text{-}} \newcommand{\u}[1]{\overline{#1} } \newcommand{\Ev}{\triangleleft} \newcommand{\In}{\text{ in } } `$$`/\cat{C}/ = (|\cat{C}|, \times, \to, \u{(\hyp)}, \Ev)`$ $`(\times) : |\c…

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…

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\hyp}{ \text{-} } `$$`\mrm{K}^X_I`$ を $`I`$ 上の定数ファミリーとして、$`A`$ を任意のファミリーとする。ファミリーの射$`\quad \mrm{K}^X_I \to A \text{ on }I`$は、グロタンディーク同型により次…

() は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のキモのひとつは、名前空間／シンボル空間の構造と相互作用を理解すること。

証明項の帰結という言葉を入れてみる。 型理論 論理 計算項 証明項 計算項の型 証明項の帰結 型付け〈typing〉 帰結付け〈consequencing〉 型{付け}?判断 帰結{付け}?判断 型チェック 命題チェック? 帰結チェック? 項の検証? 証明{項}?の検証 項の型推論 証…

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 含意→ ラムダ…