/-- 自然数に関する帰納原理 -/ 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 NatIndPrinciple' (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n := by intro n cases n with -- cases/with 文、 複数形のsを忘れがち | zero => -- 何故か名前空間修飾は要らない、が、名前の綴は合ってないとダメ exact hz -- goal is p 0 | succ k => -- 変数名は何でもよい apply hs -- goal is a : ℕ ⊢ p (succ a) /-- casesを使って関数定義 -/ def f8 (n : Nat) : Nat := by cases n; exact 3; -- 自然数のベースケース exact 7 -- 自然数のステップケース #print f8 #eval f8 0 #eval f8 1 open Nat in -- 次の定義だけに適用 /-- 普通の定義-/ def fact (n : Nat) : Nat := match n with | zero => 1 -- openしてないと名前空間修飾必要 | succ m => (fact m) * (m + 1) /-- casesによる定義 -/ def fact' (n : Nat ) : Nat := by cases n with | zero => exact 1 -- 名前空間修飾不要、理由不明 | succ m => exact (fact' m) * (m + 1) def bang (n : Nat ) : Nat := by cases n · exact 1 · exact 0 #print bang def bang' (n : Nat) : Nat := match n with | Nat.zero => 1 | Nat.succ _m => 0 #print bang' def toNum (b : Bool) : Nat := by cases b with | true => exact 1 | false => exact 0 #print toNum #print Bool.casesOn
match/witと似たcases/withが使える。exactと共に通常の関数の定義にも使える。だが、#printしてみると、関数の中身がぜんぜん違う。
