steps = [ { desc: md`Let's go over this proof carefully. First, we have the declaration of the theorem: ${leanHL`theorem fib_odd_sum_eq : ∀ (n : ℕ), fib_odd_sum n = fibonacci (2*n)`} The \`theorem\` declaration is like the function declaration \`def\`, except that it's intended for propositions (which can't be \`#eval\`'d). We'll see \`lemma\` later, which does exactly the same thing. The name of the theorem is \`fib_odd_sum_eq\` and as before, the stuff after the colon tells us the type of the theorem. In words, it says "For all nats \`n\`, \`fib_odd_sum n = fibonacci (2*n)\`". Here we could digress into a very interesting discussion on dependent type theory and the [Curry-Howard / propositions-as-types correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). For our purposes, the following points are most relevant: just as a function is passed arguments of a particular data type and returns a value of some other data type, a theorem can be viewed as a function from its hypotheses (in this case, we're given a nat \`n\`) to its conclusion (\`fib_odd_sum n = fibonacci (2*n)\`). Thus in Lean, giving a valid proof of a theorem is like supplying a definition of a function that is consistent with its declared type.`, marks: [{from: {line:0, ch:0}, to: {line:1, ch:33}}], }, { desc: md`As we saw above, we can define functions of the natural numbers in Lean via pattern matching. We can also use this syntax to prove theorems about the natural numbers. Thus the proof is structured around pattern matching on \`n\`; note how the two cases \`0\` and \`(n+1)\` resemble the cases in the induction in our informal proof.`, marks: [{from: {line:2, ch:0}, to: {line:2, ch:3}}, {from: {line:3, ch:0}, to: {line:3, ch:7}},] }, { desc: md`Case 0: ${leanHL`| 0 := rfl`} The proof in this case is \`rfl\` (which stands for "reflexivity"). It proves a goal of the form \`a = a\`. The fact that this succeeds means that Lean has confirmed that the two sides of the equality become identical after substituting \`n = 0\` and unfolding all definitions (in this case, \`fib_odd_sum 0 = 0 = fibonacci (2 * 0)\`).`, marks: [{from: {line:2, ch:0}, to: {line:2, ch:10}}], }, { desc: md`Case \`n+1\`: ${leanHL`| (n+1) := by rw [...]`} ⚠️ First, an important point about Lean's pattern-matching syntax: the \`n\` in \`(n+1)\` is **different** from the \`n\` in the theorem's type. You can think of the pattern \`(n+1)\` as introducing a new variable \`n\` that [**mask**](https://en.wikipedia.org/wiki/Variable_shadowing) the matched variable \`n\` in the theorem's type. It's probably best practice to give these variables different names to avoid confusion, but you'll see here and below that I didn't bother... This case is proved by going into ["tactic mode"](https://leanprover.github.io/theorem_proving_in_lean/tactics.html) (with \`by\`) and then using the \`rw\` ("rewrite") tactic with a list (enclosed in square brackets) of rewriting lemmas. `, marks: [{from: {line:3, ch:0}, to: {line:3, ch:17}}], }, { desc: md`You can inspect the "tactic state" for code within tactic blocks by placing the cursor somewhere or hovering the mouse pointer. Start out by placing your cursor or mouse pointer after the \`by\` and before the end of the first item in the list. You will see something like this in the infoview or a popup: ${html`

24:15: goal

fib_odd_sum_eq : ∀ (n : ℕ), fib_odd_sum n = fibonacci (2 * n),
n : ℕ
⊢ fib_odd_sum (n + 1) = fibonacci (2 * (n + 1))

`} This is a display of the current context where a list of hypotheses is shown before the ["turnstile"](https://en.wikipedia.org/wiki/Turnstile_(symbol) ⊢ and the desired goal is shown after it. Here the hypotheses are: - the inductive hypothesis \`fib_odd_sum_eq : ∀ (n : ℕ), fib_odd_sum n = fibonacci (2 * n)\`, and - \`n\` is a nat. And the goal is: - \`⊢ fib_odd_sum (n + 1) = fibonacci (2 * (n + 1))\`. While the inductive hypothesis looks like it proves this already (it says \`∀ (n : ℕ)\`, after all), if you try to use \`fib_odd_sum_eq (n+1)\`, Lean will notice that you're trying to cheat and spit out an error like "failed to prove recursive application is decreasing". Try placing your cursor before and after each of the elements of the rewrite list to see how the goal gets rewritten. [In this notebook, I've placed each rewrite on a separate line for ease of inspection.] I'll go through the first three rewrites in the next few steps.`, marks: [{from: {line:3, ch:13}, to: {line:3, ch:28}}], }, { desc: md`The first rewrite uses the definition of \`fib_odd_sum\` to transform the original goal: ${leanHL`⊢ fib_odd_sum (n + 1) = fibonacci (2 * (n + 1))`} to the goal: ${leanHL`⊢ sum (map (λ (m : ℕ), fibonacci (2 * m + 1)) (range (n + 1))) = fibonacci (2 * (n + 1))`} Reminder: you can move the cursor back and forth between the last two letters of the rewrite lemma to see the goal change back and forth.`, marks: [{from: {line:3, ch:18}, to: {line:3, ch:29}}], }, { desc: md`The second rewrite lemma \`sum_range_succ\` has type \`\`\` ∀ {α : Type} [_inst_1 : add_monoid α] (f : ℕ → α) (n : ℕ), sum (map f (range (succ n))) = sum (map f (range n)) + f n. \`\`\` This looks hairy, but just pay attention to the last bit: \`sum (map f (range (succ n))) = sum (map f (range n)) + f n\`. Note that \`succ\` stands for "successor", i.e. the "+1" function. In words, this says that the sum of a function \`f\` over \`range (n+1)\` is equal to the sum over \`range n\` plus \`f n\`. If we take \`f = (λ (m : ℕ), fibonacci (2 * m + 1))\`, then this is precisely the "extracting the last summand" step above. The goal becomes: ${leanHL`⊢ sum (map (λ (m : ℕ), fibonacci (2 * m + 1)) (range n)) + fibonacci (2 * n + 1) = fibonacci (2 * (n + 1))`}`, marks: [{from: {line:4, ch:2}, to: {line:4, ch:16}}], }, { desc: md`The third rewrite uses the definition of \`fib_odd_sum\` in reverse (hence the left arrow symbol \`←\`), which results in: ${leanHL`⊢ fib_odd_sum n + fibonacci (2 * n + 1) = fibonacci (2 * (n + 1))`}`, marks: [{from: {line:5, ch:2}, to: {line:5, ch:14}}], }, { desc: md`There are a few more rewrites included in the Lean code which direct Lean to do some arithmetic. At the end though (try putting your cursor at the end of the highlighted region, right before the closing square bracket "\`]\`"), we have something that Lean recognizes is trivial and so it declares success with an uplifting "\`no goals\`" message in place of the tactic state!`, marks: [{from: {line:6, ch:2}, to: {line:9, ch:11}}], } ]