quiz: course-of-values recursion

Stream: maths

[Bulhwi Cha]

Quiz: define the following function in Lean, evaluate the values of the first ten arguments of that function, and find another way of defining it.

$$f \left( 0 \right) = 1 \wedge f \left(n + 1 \right) = f \left( n \right) + f \left( n - 1 \right) + \cdots + f \left( 0 \right)$$

Solution

-- this code is written in Lean 4
import Std.Data.Nat.Lemmas

open List

namespace sumOfAllPrevSums

def loop (n : Nat) : List Nat :=
  match n with
  | 0     => [1]
  | m + 1 => loop m ++ [Nat.sum (loop m)]

#reduce loop 0 -- [1]
#reduce loop 1 -- [1, 1]
#reduce loop 2 -- [1, 1, 2]
#reduce loop 3 -- [1, 1, 2, 4]
#reduce loop 4 -- [1, 1, 2, 4, 8]
#reduce loop 5 -- [1, 1, 2, 4, 8, 16]
#reduce loop 6 -- [1, 1, 2, 4, 8, 16, 32]
#reduce loop 7 -- [1, 1, 2, 4, 8, 16, 32, 64]
#reduce loop 8 -- [1, 1, 2, 4, 8, 16, 32, 64, 128]
#reduce loop 9 -- [1, 1, 2, 4, 8, 16, 32, 64, 128, 256]

theorem loop_lt (n : Nat) : (loop n).length - 1 < (loop n).length := by
  apply Nat.sub_lt_self
  case h₀ => show 0 < 1; decide
  case h₁ =>
    show 1 ≤ (loop n).length
    induction n with
    | zero =>
      apply Nat.le_of_eq
      show 1 = (loop 0).length
      calc
        1 = [1].length      := rfl
        _ = (loop 0).length := rfl
    | succ m ih =>
      apply Nat.le_trans ih
      show (loop m).length ≤ (loop (m + 1)).length
      calc
        (loop m).length
      ≤ (loop m).length + 1                   := by apply Nat.le_add_right
    _ = (loop m).length + [Nat.sum (loop m)].length := rfl
    _ = (loop m ++ [Nat.sum (loop m)]).length := by rw [length_append]
    _ = (loop (m + 1)).length                 := rfl

end sumOfAllPrevSums

-- sum of all previous sums
def sumOfAllPrevSums (n : Nat) : Nat :=
  let loop    := sumOfAllPrevSums.loop
  let loop_lt := sumOfAllPrevSums.loop_lt
  (loop n).get ⟨(loop n).length - 1, loop_lt n⟩

#reduce sumOfAllPrevSums 0 -- 1
#reduce sumOfAllPrevSums 1 -- 1
#reduce sumOfAllPrevSums 2 -- 2
#reduce sumOfAllPrevSums 3 -- 4
#reduce sumOfAllPrevSums 4 -- 8
#reduce sumOfAllPrevSums 5 -- 16
#reduce sumOfAllPrevSums 6 -- 32
#reduce sumOfAllPrevSums 7 -- 64
#reduce sumOfAllPrevSums 8 -- 128
#reduce sumOfAllPrevSums 9 -- 256

namespace sumOfAllPrevSums

theorem loop_lemma (n : Nat) : Nat.sum (loop n) = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ m ih =>
    show Nat.sum (loop (m + 1)) = 2 ^ (m + 1)
    calc
      Nat.sum (loop (m + 1))
    = Nat.sum (loop m ++ [Nat.sum (loop m)])        := rfl
  _ = Nat.sum (loop m) + Nat.sum [Nat.sum (loop m)] := by rw [Nat.sum_append]
  _ = Nat.sum (loop m) + Nat.sum (loop m)           := rfl
  _ = 2 * Nat.sum (loop m)                          := by rw [Nat.two_mul]
  _ = 2 * 2 ^ m                                     := by rw [ih]
  _ = 2 ^ (m + 1)                                   := by rw [Nat.pow_succ']

theorem general_term_lemma (n : Nat)
      : length (loop n) = length (loop (n + 1)) - 1 := by
  apply Eq.symm
  show length (loop (n + 1)) - 1 = length (loop n)
  calc
    length (loop (n + 1)) - 1
  = length (loop n ++ [Nat.sum (loop n)]) - 1 := rfl
_ = length (loop n) + length ([Nat.sum (loop n)]) - 1
                                 := by rw [length_append]
_ = length (loop n) + 1 - 1 := rfl
_ = length (loop n)         := rfl

theorem general_term (n : Nat)
      : sumOfAllPrevSums n = if n = 0 then 1 else 2 ^ (n - 1) := by
  induction n with
  | zero => rfl
  | succ m ihm =>
    simp
    show sumOfAllPrevSums (m + 1) = 2 ^ m
    induction m with
    | zero => simp
    | succ k ihk =>
      simp [*] at *
      show sumOfAllPrevSums (k + 2) = 2 ^ (k + 1)
      calc
        sumOfAllPrevSums (k + 2)
      = (loop (k + 2)).get (Fin.mk ((loop (k + 2)).length - 1)
          (loop_lt (k + 2)))   := rfl
    _ = Nat.sum (loop (k + 1)) :=
          by apply get_last;     apply Nat.not_lt_of_le
             apply Nat.le_of_eq; apply general_term_lemma
    _ = 2 ^ (k + 1)            := by rw [loop_lemma]

end sumOfAllPrevSums

By theorem sumOfAllPrevSums.general_term,

$$f \left( 0 \right) = 1 \wedge f \left( n + 1 \right) = 2 ^ n$$

Reference

CWoo. “course-of-values recursion.” PlanetMath. Last modified Mar 22, 2013. https://planetmath.org/courseofvaluesrecursion.

[Bulhwi Cha]

While trying to solve Exercise 3 from Chapter 8 of #tpil4, I came up with the quiz above.

[Patrick Johnson]

Can you define f without using lists and without proving any theorem before the definition of f?

Simpler definition

noncomputable def f : Nat → Nat :=
Classical.epsilon $ λ f => f 0 = 1 ∧ ∀ n,
f (n + 1) = (n + 1).rec 0 (λ k a => a + f (n - k))

The final proof may be harder using this definition though.

[Bulhwi Cha]

Right. Maybe I can also use Finset to define f; I'd like it to be computable.