数学的帰納法のステップの部分。
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 0 = arith 0 := by simp -- theorem arith_suc' (m : Nat) : theorem unfold_succ (m : Nat) : Nat.succ m = m + 1 := by simp theorem arith_suc (m : Nat) : arith m + Nat.succ m = arith (Nat.succ m) := by rw [arith] -- m * (m + 1) / 2 + Nat.succ m = arith (Nat.succ m) rw [arith] -- m * (m + 1) / 2 + Nat.succ m = Nat.succ m * (Nat.succ m + 1) / 2 rw [unfold_succ] -- m * (m + 1) / 2 + (m + 1) = (m + 1) * (m + 1 + 1) / 2 /- m * (m + 1) / 2 + (m + 1) = (m^2 + m)/2 + (2m + 2)/2 = (m^2 * 3m + 2)/2 (m + 1) * (m + 1 + 1) / 2 = (m + 1) * (m + 2) / 2 = (m^2 + 2m + m + 2) / 2 -/ sorry theorem case_succ (m : Nat) : sumto m = arith m → (sumto m) + Nat.succ m = arith (Nat.succ m) := by intro h rw [h] -- arith m + Nat.succ m = arith (Nat.succ m) -- sorry exact arith_suc m theorem target : ∀(n : Nat), (sumto n) = (arith n) := by intro n cases n with | zero => -- sorry -- case_zero exact case_zero | succ m => apply case_succ m -- 失敗 -- sorry -- case_succ -- sumto (Nat.succ m) = arith (Nat.succ m) #print target end NatInd
