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