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

スキーマ、タプル空間、タプルインスタンス、フィールド関数、テーブル 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この定義のリカーサー〈帰…

順不同・断片的な記述となる。ネタ元は： https://leanprover.github.io/theorem_proving_in_lean4/tactics.html https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#basic-tactics で出てくるタクティクを列挙。 apply Iff.itro ： 論理…

過去記事： タクティク解説、等式の種類も タクティクのためのゲンツェン法則 「Leanタクティク」は、実際のLeanのタクティクを話題にする。参考URL： https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_C/Part_C.html ケビン…

ステージデザインとシナリオスクリプトで指定すること。 ストーリー〈コース〉の開始ステージ（入り口）と終了（出口）の指定。 各ステージのコンテキスト（予備知識）とスキル（コマンドセット） ステージクリア条件 クリアした後の進行先の選択肢、条件付…

論理的体系のマクロな構造とその学習は、リーズニングゲームで行う。リーズニングゲームは、背景知識／背景スキル〈コマンドセット〉を提供するグリモワ〈仏: grimoire | 魔導書〉と、ゲーム・ストーリーからなる。ゲームストーリーはパッケージとして流通単…

eviは証拠〈evidence〉の略記だとする。命題と証明の圏 $`{\bf Ded}`$ から集合圏への関手が定義できる。 $`P\in |{\bf Ded}| \mapsto \mathrm{evi}(P) := {\bf Ded}(\top, P)`$ $`(f:P \to Q) \text{ in }{\bf Ded} \mapsto \mathrm{evi}(f) := {\bf Ded}(\…

依存型に一般化したカリー同型：$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{ \text{ in } } `$$`\quad \cat{C} \in |{\bf Cat}|\\ \quad A:I \to |\cat{C}|_0 \In {\bf Set}\\ \quad \prod_{i\in I} \ca…

次の同型が成立する。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$$`\prod_{i \in I} {\bf Set}[X, A[i] ] \cong {\bf Bun}[I](X \times I, \sum_I A[\bullet]) \\ \cong {\bf Fam}[I](\mrm{K}^X_I, A[\bullet]) `$名前だ…

まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$ コンテナ インスティ…