doc(library/data/nat/examples): add examples

library/data/nat/examples/fib.lean

@@ -0,0 +1,52 @@
+/-
+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 fib : nat → nat
+| 0     := 1
+| 1     := 1
+| (n+2) := fib (n+1) + fib n
+
+private definition fib_fast_aux : nat → (nat × nat)
+| 0     := (0, 1)
+| 1     := (1, 1)
+| (n+2) :=
+  match fib_fast_aux (n+1) with
+  | (fn, fn1) := (fn1, fn1 + fn)
+  end
+
+open prod.ops -- Get .1 .2 notation for pairs
+
+definition fib_fast (n : nat) := (fib_fast_aux n).2
+
+-- We now prove that fib_fast and fib are equal
+
+lemma fib_fast_aux_succ_succ : ∀ n, fib_fast_aux (succ (succ n)) = match fib_fast_aux (succ n) with | (fn, fn1) := (fn1, fn1 + fn) end :=
+λ n, rfl
+
+lemma fib_fast_aux_lemma : ∀ n, (fib_fast_aux (succ n)).1 = (fib_fast_aux n).2
+| 0               := rfl
+| 1               := rfl
+| (succ (succ n)) :=
+  begin
+    rewrite [fib_fast_aux_succ_succ],
+    rewrite [-prod.eta (fib_fast_aux (succ (succ n)))],
+  end
+
+theorem fib_eq_fib_fast : ∀ n, fib n = fib_fast n
+| 0     := rfl
+| 1     := rfl
+| (n+2) :=
+  begin
+    have feq  : fib n = fib_fast n,               from fib_eq_fib_fast n,
+    have f1eq : fib (succ n) = fib_fast (succ n), from fib_eq_fib_fast (succ n),
+    unfold [fib, fib_fast, fib_fast_aux],
+    rewrite [-prod.eta (fib_fast_aux (succ n))], esimp,
+    fold fib_fast (succ n), rewrite -f1eq,
+    rewrite fib_fast_aux_lemma,
+    fold fib_fast n, rewrite -feq,
+  end

library/data/nat/examples/partial_sum.lean

@@ -0,0 +1,33 @@
+/-
+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  : mul.left_distrib
+                   ...   = 2 * succ n + succ n * n  : two_mul_partial_sum_eq
+                   ...   = 2 * succ n + n * succ n  : mul.comm
+                   ...   = (2 + n) * succ n         : mul.right_distrib
+                   ...   = (n + 2) * succ n         : add.comm
+                   ...   = (succ (succ n)) * succ n : rfl
+
+theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) div 2 :=
+take n,
+assert h₁ : (2 * partial_sum n) div 2 = ((succ n) * n) div 2, by rewrite two_mul_partial_sum_eq,
+assert h₂ : 2 > 0, from dec_trivial,
+by rewrite [mul_div_cancel_left _ h₂ at h₁]; exact h₁