33 lines
1.2 KiB
Text
33 lines
1.2 KiB
Text
/-
|
|
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Author: Leonardo de Moura
|
|
-/
|
|
import data.nat
|
|
open nat
|
|
|
|
definition partial_sum : nat → nat
|
|
| 0 := 0
|
|
| (succ n) := succ n + partial_sum n
|
|
|
|
example : partial_sum 5 = 15 :=
|
|
rfl
|
|
|
|
example : partial_sum 6 = 21 :=
|
|
rfl
|
|
|
|
lemma two_mul_partial_sum_eq : ∀ n, 2 * partial_sum n = (succ n) * n
|
|
| 0 := by reflexivity
|
|
| (succ n) := calc
|
|
2 * (succ n + partial_sum n) = 2 * succ n + 2 * partial_sum n : by rewrite left_distrib
|
|
... = 2 * succ n + succ n * n : by rewrite two_mul_partial_sum_eq
|
|
... = 2 * succ n + n * succ n : by rewrite (mul.comm n (succ n))
|
|
... = (2 + n) * succ n : by rewrite right_distrib
|
|
... = (n + 2) * succ n : by rewrite add.comm
|
|
... = (succ (succ n)) * succ n : rfl
|
|
|
|
theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) / 2 :=
|
|
take n,
|
|
have h₁ : (2 * partial_sum n) / 2 = ((succ n) * n) / 2, by rewrite two_mul_partial_sum_eq,
|
|
have h₂ : (2:nat) > 0, from dec_trivial,
|
|
by rewrite [nat.mul_div_cancel_left _ h₂ at h₁]; exact h₁
|