31:T13f5,md`I like math. I like thinking about it and talking about it with like-minded friends. But I had to take a bunch of courses, do a lot of challenging reading and writing, and most importantly, learn from many good teachers before I was ready to appreciate the style of math that appears in most papers and books. Here's a crude analogy: written definitions, theorems and proofs are kind of like a very high-level source code for math, and it takes time and care to train one's brain to efficiently interpret this code. Correct proofs should in principle "compile" to a sequence of individually justifiable logical deductions, but in practice, many steps are left implicit per the writer's taste, and a reader needs confidence and experience to successfully fill these in. Furthermore, proofs frequently rely on definitions and results given elsewhere, so trying to understand an argument without sufficient prerequisites is like reading code for a program when you don't have access to the library functions being called. Given these difficulties, wouldn't it be nice to have a computer help out, just as we have fancy editors and IDEs assist us with other sorts of code? As it happens, programming languages for formal proofs already exist. [Proof assistants](https://en.wikipedia.org/wiki/Proof_assistant) (also known as "interactive theorem provers") are computer programs that enable their users to write mathematical definitions, theorems, and proofs as code. This code is simultaneously checked for correctness, so that only theorems that have been formally verified are ultimately accepted into the system. Proof assistants frequently feature interfaces to text editors that assist in the writing of this code, including e.g. facilities for searching and applying previously proved results as well as tools for inspecting proofs, such as a "goal" display which displays the progress made in proving a statement. Admittedly, these programs are still rather difficult to use – after all, you have to learn a new programming language to use a proof assistant (and sometimes more than one)! On the other hand, in addition to checking correctness and assisting searches and all that, they also enable you to interact with proofs in new and wonderful ways. Formalized proofs are in essence gigantic syntax trees which can be analyzed and visualized; see e.g. the picture produced by the [Lean perfectoid project](https://leanprover-community.github.io/lean-perfectoid-spaces/). Plus, there's a certain fun factor: poking my way towards a formal proof while the computer validates moves and returns the state really does feel a lot like playing a puzzle game (cf. [these comments by Mike Shulman on Coq](https://golem.ph.utexas.edu/category/2012/06/the_gamification_of_higher_cat.html) cited in Katherine Ye's slides linked below). While I don't believe that informal written math can or should be replaced by code, I do think that (some) future mathematical expositions might be integrated with interactive formalizations to the benefit of readers and authors alike. I'm not sure if those will be implemented using anything like currently extant proof assistants. However, it might still be interesting to experiment with integrating today's proof assistants into mathematical text. If nothing else, such an effort may make these programs more accessible and easier to teach and learn. In this spirit, I've written up some simple mathematical proofs in a pair of Observable notebooks with their formalizations displayed in an integrated proof assistant ([Lean](http://leanprover.github.io/), using the editor from [this notebook](https://observablehq.com/@bryangingechen/hello-lean-prover)). Specifically, in Part 1 (this notebook), I prove three [Fibonacci number](https://en.wikipedia.org/wiki/Fibonacci_number) sum identities and (in [Part 2](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars)), I prove that certain objects are counted by Fibonacci numbers and make simple graphics from the Lean output. If by chance you're already familiar with Lean and are just curious about how I wrote this document (and how you can too!), check out [the last section of this notebook](#sectionImplementation). *Thanks to the denizens of the [Lean prover Zulip chat](https://leanprover.zulipchat.com/) for answering lots of questions and helping out with proofs when I was getting started! Hop in if you're interested in all in Lean, questions at all levels are welcomed.* **Some inspiring links**: - Jeremy Avigad, [The Mechanization of Mathematics (pdf)](http://dx.doi.org/10.1090/noti1688), [[talk slides] (pdf)](https://www.andrew.cmu.edu/user/avigad/Talks/mechanization_talk.pdf), - Kevin Buzzard, [Formalising mathematics – a mathematician's viewpoint](https://xenaproject.wordpress.com/2018/09/22/formalising-mathematics-a-mathematicians-personal-viewpoint/) (and there are many other good posts on the Xena project blog), - Katherine Ye, [Proof assistants as a tool for thought [talk slides] (pdf)](http://www.cs.cmu.edu/~kqy/resources/coq_tools_for_thought.pdf). `32:Tce2,leanResources = md`The above text box is read-only, but you can still click around or hover over code to inspect it. The main things you will see when hovering around here are the [types](https://en.wikipedia.org/wiki/Type_theory) of certain expressions. Unfortunately, I won't give an actual tutorial for Lean in this notebook, only some hints about what the code you're reading means. I recommend looking at the books [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/introduction.html) and [Logic & Proof](http://avigad.github.io/logic_and_proof/introduction.html) if you're interested in learning more about Lean! The former is a bit more like an actual tutorial but also a bit more advanced in terms of the background knowledge in logic required. The latter is actually a book on introductory mathematical logic and proofs in mathematics, but it has several nice chapters on Lean. The first line tells Lean to import [a library file](https://github.com/leanprover-community/mathlib/blob/master/src/data/list/basic.lean) containing basic facts about lists. You can ignore the "\`@[reducible]\`" for now – suffice it to say that it's an "attribute" which tells Lean to unfold this definition wherever possible. The colon in: ${leanHL`def fibonacci : ℕ → ℕ`} is Lean syntax for a type annotation. This particular line declares a new function \`fibonacci\` of type \`ℕ → ℕ\`, i.e. a function from the nats (natural numbers) to the nats. The remainder of the definition uses Lean's [pattern-matching syntax](https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#pattern-matching) (which you can think of as kind of like a \`switch ... case\` statement) to complete the definition by providing a function of that type. Explicitly, when \`fibonacci\` is applied to a nat, Lean looks to match it to one of 3 cases (exactly as in the recursive formula above): - Case \`0\`: ${leanHL`| 0 := 0`} (Read as: \`fibonacci 0\` is defined to be (\`:=\`) \`0\`.) - Case \`1\`: ${leanHL`| 1 := 1`} - Case \`(n+2)\`: ${leanHL`| (n+2) := fibonacci n + fibonacci (n+1)`} Note that Lean's equation compiler is smart enough to recognize that: - every nat is covered by the above cases, and - even though \`fibonacci\` references itself in the \`(n+2)\` case, the function arguments strictly decrease, so that the recursion will eventually terminate. (If you try to define a function on the natural numbers which breaks these rules, Lean will throw an error.) The final line of the box above, \`open nat list\`, lets us write abbreviations like \`add_comm\` and \`map\` for \`nat.add_comm\` and \`list.map\`. In this notebook, the main way in which we'll be running Lean code is using the \`#eval\` command. Roughly speaking, when the Lean server encounters \`#eval\`, it attempts to evaluate the following expression (see [this chapter of TPiL](https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html) for more details) and then returns the result as an \`info\` message. Below are some \`#eval\` statements using \`fibonacci\` – the following editor is not read-only, so feel free to experiment by changing the numbers or making other edits (the Reset button will bring you back to the initial state):`33:T64a,md`Note that function application doesn't require parentheses; the expression \`fibonacci 5\` evaluates the function \`fibonacci\` at 5, similarly, \`range 10\` evaluates the \`range\` function at 10. In general, given a function \`f\` of type \`A → B\` and an expression \`a\` of type \`A\`, \`f a\` is of type \`B\`. The second \`#eval\` statement deserves a little bit of explanation. Try hovering over \`range\` and you'll see that it has type \`ℕ → list ℕ\`. This means that it's a function from nats to lists of nats. In particular, \`range 10\` evaluates to a list containing the numbers from 0 to 9. Finally, the expression \`(range 10).map fibonacci\` uses a certain shorthand which we'll see much more of below. The function \`list.map\` is under the \`list\` namespace and has type \`(α → β) → list α → list β\` (in words, it takes a function of type \`α → β\`, a list whose elements are of type \`α\` and returns a list of elements of type \`β\`). If \`xs\` has type \`list α\` and \`f\` has type \`α → β\`, then \`xs.map f\` is short for \`list.map xs f\`. Thus \`(range 10).map fibonacci\` is really \`map fibonacci (range 10)\`, which is an application of the \`fibonacci\` function to each of the elements of the list \`range 10\`. In general, given a function of type \`foo.bar\` with a parameter of type \`foo\` and a term \`t : foo\`, we can write \`t.bar\` and Lean will interpret this as \`foo.bar\` with \`t\` passed as an argument in the appropriate place. As an aside, note that we can parse the messages from Lean and use them in Observable cells:`34:T5d1,sectionFormulas = md`## Formulas 🧮 I think I first learned about Fibonacci numbers in middle school. Middle school algebra was all about cool formulas, and I remember having a blast proving cool sum formulas (likely due in no small part to the joy of scrawling ${tex`\Sigma`}'s and other mysterious symbols in my homework). In this section, let's see if we can teach Lean some sums. Specifically, these three: ${tex.block`\begin{aligned} F_0+F_1+F_2+\cdots+F_n &= F_{n+2} - 1,\\ F_1 + F_3 + F_5 + \cdots + F_{2n-1} &= F_{2n},\\ F_0 + F_2 + F_4 + \cdots + F_{2n} &= F_{2n+1} - 1. \end{aligned}`} It turns out to be convenient later to work with sums that go to ${tex`n-1`} (because \`range n\` only contains numbers from \`0\` to \`n-1\`); with this choice, the sum identities above can be written in more compact notation: ${tex.block`\begin{aligned} 1+\sum_{m=0}^{n-1}F_m&= F_{n+1},\\ \sum_{m=0}^{n-1}F_{2m+1} &= F_{2n},\\ 1+\sum_{m=0}^{n-1}F_{2m}&= F_{2n-1}. \end{aligned}`} We take the convention that sums from 0 to -1 (which appear when ${tex`n=0`}) are zero (since they are sums over an empty set). We'll prove the first two identities for all ${tex`n\in\mathbb{N}`} and the last one for nats ${tex`n>0`} (since we haven't defined ${tex`F_{-1}`}). The next code block contains the following definitions in Lean: - \`fib_sum n\` := ${tex`\sum_{m=0}^{n-1}F_m,`} - \`fib_odd_sum n\` := ${tex`\sum_{m=0}^{n-1}F_{2m+1},`} - \`fib_even_sum n\` := ${tex`\sum_{m=0}^{n-1}F_{2m}.`} `35:T75f,md`Before we look at the formal proofs, let's quickly prove one of these "informally". The basic idea in all cases is to proceed by [the principle of induction](https://en.wikipedia.org/wiki/Mathematical_induction). To prove any proposition ${tex`P`} for all natural numbers ${tex`n`}, we: - first prove that ${tex`P`} holds when ${tex`n=0`}, - show that if ${tex`P`} holds for ${tex`n`}, it also holds for ${tex`n+1`}. For example, consider the identity for the sum of odd Fibonacci numbers: **Theorem**: For all ${tex`n \in \mathbb{N}`}, ${tex.block`\sum_{m=0}^{n-1}F_{2m+1} = F_{2n}.`} *Proof*: By the principle of induction, we consider two cases: - When ${tex`n=0`}, the empty sum on the left hand side is zero, per our convention. The right hand side is ${tex`F_{0}=0`}, so the identity holds in this case. - Now suppose the identity holds for ${tex`n`}. We want to prove the ${tex`n+1`} case of the identity: ${tex.block`\sum_{m=0}^{n}F_{2m+1} = F_{2(n+1)}.`} To do so, we manipulate the sum on the left hand side until it becomes the right hand side: ${tex.block`\begin{aligned} \sum_{m=0}^nF_{2m+1} =& \sum_{m=0}^{n-1}F_{2m+1} + F_{2n+1}&\text{by extracting the last summand}\\ =& F_{2n} + F_{2n+1}&\text{by the inductive hypothesis}\\ =& F_{2n+2}&\text{by the definition of $F_{m}$}\\ =& F_{2(n+1).} \end{aligned}`} That concludes the proof! ${tex`\square`} The text box below shows a formalization of this proof in Lean. By default, Lean is silent when given a correct proof ("if it compiles, it's correct"). [Writing proofs in Lean is thus often a matter of eliminating "squiggly lines", which indicate errors.] As with the definitions shown above, Lean will provide info when you hover or click around. You'll see that Lean provides "goal" info in certain parts of the proof. Click the prev and next buttons below to navigate through an explanation of the code:`36:T9bd,md`The type of \`fib_even_sum_eq\` is a little more complicated due to the condition \`n > 0\`: ${leanHL`∀ {n : ℕ} (h : n > 0), fib_even_sum n + 1 = fibonacci (2*n - 1)`} In words: "For all nats \`n\`, and all proofs \`h\` that \`n > 0\`, we have the equality \`fib_even_sum n + 1 = fibonacci (2*n - 1)\`." Pattern-matching happens on both \`n\` and \`h\`, hence we have 2 parameters in each case: - Case 0: ${leanHL`| 0 h := (gt_irrefl 0 h).elim`} In Lean, we have to give an argument to rule out the \`n = 0\` case. This is a little silly so feel free to skip to the next case. Here, the hypothesis \`h\` would have to be a proof that \`0 > 0\`. This, of course, is impossible and leads to a contradiction (\`gt_irrefl 0 h : false\`), so Lean lets us close the goal with \`.elim\` (short for \`false.elim\` which is [the principle of explosion](https://en.wikipedia.org/wiki/Principle_of_explosion)). - Case 1: ${leanHL`| 1 _ := rfl`} Just as in the base case of the previous theorem, Lean is able to recognize that the LHS and RHS are equal, so \`rfl\` suffices. I've used an underscore for the proof of \`1 > 0\` as a way of indicating that it's unused. (Outside of pattern-matching, an underscore is a special keyword which tells Lean to try to infer some expression to replace it.) - Case \`n+2\`: ${leanHL`| (n+2) _ :=`} The \`have\` syntax tells Lean that we want to prove a side result first and add it to the context for this proof. While we won't see it much in these pages, this is a good way of storing intermediate results in a long proof: ${leanHL`have H : fib_even_sum (n+1) + 1 = fibonacci (2*(n+1) - 1) := `} This line says that \`H\` is a proof of the equality \`fib_even_sum (n+1) + 1 = fibonacci (2*(n+1) - 1)\`. It's defined to be an application of the inductive hypothesis (named \`fib_even_sum_eq\`) to a proof that \`n+1\` is positive (\`succ_pos n\`): ${leanHL` fib_even_sum_eq (succ_pos n),`} The \`begin ... end\` block also tells Lean to enter tactic mode. (The difference with \`by\` is that we can put multiple commands between \`begin\` and \`end\`.) The tactics used are \`rw\`, \`change\` and \`rw\` again. I leave it to you to inspect the rewrites, which are mostly straightforward (remember that you can check the type of the rewrite lemma by hovering over it). The \`change\` tactic lets us replace the goal with something definitionally equivalent; in this case, I used it to avoid doing some silly arithmetic with 1's and 2's. `37:T7ae,sectionImplementation = md`## Implementation notes *This section is primarily written for Lean users who aren't familiar with Observable notebooks. If you're more interested in Lean, see [the resources linked above](#leanResources).* This document is an [Observable notebook](https://observablehq.com/@observablehq/five-minute-introduction) (see also: the ["User manual"](https://observablehq.com/@observablehq/user-manual)). You can publish notebooks just like this one if you sign in with your Github, Twitter or Google account! While these notebooks resemble Jupyter or Mathematica notebooks in that they are made up of "cells", they actually [run more like spreadsheets](https://observablehq.com/@observablehq/how-observable-runs), since cells are **automatically re-evaluated** when they are edited or when any of their dependencies change. This is in contrast to other notebook systems where cells are either evaluated manually, or are made to run once from top to bottom. A great feature of Observable notebooks is that all the code is easily available: **click to the left of any "unpinned" cell to display its source**. While everything is actually written in JavaScript ([kind of](https://observablehq.com/@observablehq/observables-not-javascript)), most of the content, including this cell, is actually markdown text, wrapped in an \`md\` "tag function". The equations above are written in LaTeX and included in the markdown using the \`tex\` tag function. See ["Introduction to HTML"](https://observablehq.com/@observablehq/introduction-to-html) for details. Finally, notebooks aren't restricted to the \`observablehq.com\` platform – they can be easily downloaded and embedded on other sites: see [this tutorial](https://observablehq.com/@observablehq/downloading-and-embedding-notebooks). The code cells in the rest of this section are dependencies of the Lean editor cells above. I've included some explanation in the surrounding text below.`38:T910,md`Now, a word on how I prepared the Lean code used in this notebook. I first wrote a version of the Lean proofs in VS Code using the [\`vscode-lean\`](https://github.com/leanprover/vscode-lean) extension. Then I copied it into a cell in this notebook and modified it as I wrote the surrounding text. By default, the Lean editor notebook loads a ZIP bundle containing only the core Lean library. However, this means that you can't immediately work with Lean files that build off of the Lean community standard library [mathlib](https://github.com/leanprover-community/mathlib). For this reason, when I first started experimenting with my Lean code in this notebook, I used the following to import a Lean editor that loads a ZIP bundle containing all files in \`mathlib\`: \`\`\`js import {leanEditor, leanEditorFrom, leanControl, leanHL, parseLeanMsgs} with {leanLibName} from '@bryangingechen/hello-lean-prover' \`\`\` The \`with {leanLibName}\` syntax refers to another cell that I had in this notebook: \`\`\`js leanLibName = 'library' \`\`\` which replaces [a certain cell](https://observablehq.com/@bryangingechen/hello-lean-prover#leanLibName) that is used in generating the URL to the Lean server's ZIP bundle. While this was a fine solution for personal use, the ZIP bundle with all of mathlib is ~19 MB, which is way too large to ask a casual reader to download. Fortunately, it's possible to use a much smaller ZIP file, at the cost of doing a bit more preparation. So after I finalized the Lean code in this notebook, I copied it back to my computer and used \`leanpkg\` to make a new Lean package (see [\`lean-fibonacci\`](https://github.com/bryangingechen/lean-fibonacci)). I then used the \`mk_library.py\` script from my fork of the [\`lean-web-editor\`](https://github.com/bryangingechen/lean-web-editor) project (see the instructions in the README there) to prepare the much smaller (~3 MB) \`libfib.zip\`, which contains only the files needed for my code to work. Finally, I hosted \`libfib.zip\` in my personal \`github.io\` repository and then changed the import statement to the one currently used above. The "\`with {transportOpts}\`" syntax replaces the [\`transportOpts\` cell in the Lean editor notebook](https://observablehq.com/@bryangingechen/hello-lean-prover#transportOpts) with this:`39:T54e,fibFormulas = String.raw`import data.list.range @[reducible] def fibonacci : ℕ → ℕ | 0 := 0 | 1 := 1 | (n+2) := fibonacci n + fibonacci (n+1) open nat list --- @[reducible] def fib_sum (n : ℕ) : ℕ := ((range n).map fibonacci).sum @[reducible] def fib_odd_sum (n : ℕ) : ℕ := ((range n).map (λ m, fibonacci (2*m + 1))).sum @[reducible] def fib_even_sum (n : ℕ) : ℕ := ((range n).map (λ m, fibonacci (2*m))).sum --- theorem fib_odd_sum_eq : ∀ (n : ℕ), fib_odd_sum n = fibonacci (2*n) | 0 := rfl | (n+1) := by rw [fib_odd_sum, sum_range_succ, ←fib_odd_sum, fib_odd_sum_eq, mul_add, mul_one, fibonacci] --- theorem fib_even_sum_eq : ∀ {n : ℕ} (h : n > 0), fib_even_sum n + 1 = fibonacci (2*n - 1) | 0 h := (gt_irrefl 0 h).elim | 1 _ := rfl | (n+2) _ := have H : fib_even_sum (n+1) + 1 = fibonacci (2*(n+1) - 1) := fib_even_sum_eq (succ_pos n), begin rw [fib_even_sum, sum_range_succ, ←fib_even_sum, add_right_comm, H, mul_add, mul_one, mul_add], change fibonacci (2*n + 1) + fibonacci (2*n + 1 + 1) = fibonacci (2*n + 1 + 2), rw [←fibonacci], end --- theorem fib_sum_eq : ∀ (n : ℕ), fib_sum n + 1 = fibonacci (n+1) | 0 := rfl | (n+1) := begin rw [fibonacci, ←fib_sum_eq n], simp [range_succ, fib_sum, add_left_comm, add_comm], end`.split('\n---\n')3a:T1be5,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}}], } ]3b:T673,md`The editable (non-read-only) editors required a little bit of planning to set up. I wanted them to have access to definitions from the \`fib_formulas.lean\` editors without having to display them again. I also wanted their content to be independent from those editors, since if they shared a \`docArray\`, user input in one editor could screw up the parsing of later editors. Since the Lean server does not allow us to import from one open Lean file to another, I had to either copy all of the definitions that I wished to reuse into the \`docArray\` of every editable editor, or import from a file in the ZIP bundle. As I had already decided to make a custom ZIP bundle, I went for the latter. The editable editor cells thus use arrays consisting of 2 strings. The first string contains \`import fib\`, so that all of my definitions are available, and then I also include an \`open\` statement for convenience. The second string contains the Lean code that the user has access to and can edit. I use \`docIndex: 1\` in the options so that only the second string is displayed. For instance, here's the source code for [the first editable editor](#fEval): \`\`\`js viewof fEval = leanEditor({ docArray: [ \`import fib open nat list\`, \`#eval fibonacci 5 #eval (range 10).map fibonacci\` ], docIndex: 1, fileName: 'fib_formula_eval.lean', displayMode: 1, lineNumbers: false, height: '200px', header: html\`\`, }, invalidation) \`\`\` The \`header\` option is used just to hide the default filename display. Note that the value of this cell \`fEval\` is used in the last cell before [this section](#sectionFormulas).`3c:[] 2f:{"title":"Fibonacci formalized 1: some sums","cells":[{"id":0,"value":"md`# Fibonacci formalized 1: some sums`","pinned":false,"hidden":false,"mode":"ojs"},{"id":519,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"id":1254,"value":"contents = md`## Contents\n\n**Part 1**:\n- [Fibonacci numbers](#sectionStart)\n- [Formulas 🧮](#sectionFormulas)\n - [Sum of odd Fibonacci numbers](#sectionSumOdd)\n - [Sum of even Fibonacci numbers](#sectionSumEven)\n - [Sum of all Fibonacci numbers](#sectionSumAll)\n- [Implementation notes for Part 1](#sectionImplementation)\n\n[Part 2](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars):\n- [Bees 🐝](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars#sectionBees)\n- [Cars 🚗](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars#sectionCars)\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":518,"value":"sectionStart = md`## Fibonacci numbers\n\nLet's start the math with a definition of the Fibonacci numbers. The first two are 0 and 1 and then each number afterwards is defined to be the sum of the two preceding it in the sequence. Thus the Fibonacci sequence begins: \n\n${tex.block`0,1,1,2,3,5,8,13,21,34,55,89,\\dots`} \n\nIf ${tex`F_n`} denotes the ${tex`n`}th Fibonacci number, then we have the following recursive definition:\n\n${tex.block`F_n = \\begin{cases}\n0 & n=0,\\\\\n1 & n=1,\\\\\nF_{n-2} + F_{n-1} & n>1.\n\\end{cases}`}\n\nHere it is formalized in Lean:\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":29,"value":"viewof f0 = fibFormulasEditor(0, invalidation, { height: '175px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":695,"value":"$32","pinned":false,"hidden":false,"mode":"ojs"},{"id":81,"value":"viewof fEval = leanEditor({\n docArray: [ \n `import fib\nopen nat list`,\n `#eval fibonacci 5\n#eval (range 10).map fibonacci`\n ],\n docIndex: 1,\n fileName: 'fib_formula_eval.lean',\n displayMode: 1,\n lineNumbers: false,\n height: '200px',\n header: html``,\n}, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":706,"value":"$33","pinned":false,"hidden":false,"mode":"ojs"},{"id":438,"value":"parseLeanMsgs(fEval.msgs)","pinned":true,"hidden":false,"mode":"ojs"},{"id":431,"value":"$34","pinned":false,"hidden":false,"mode":"ojs"},{"id":381,"value":"viewof f1 = fibFormulasEditor(1, invalidation, { height: '225px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":733,"value":"md`The \\`.sum\\` notations make use of the shorthand described above for \\`list.sum\\` (note that the parenthesized expressions that \\`.sum\\` is applied to are all of type \\`list\\`).\n\nIn the second and third definitions above, the \\`λ\\`'s are used to define [anonymous functions](https://en.wikipedia.org/wiki/Anonymous_function) which are then passed to the \\`list.map\\` function.\n\nGiven these definitions, we can now check the formulas above in a few cases:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":565,"value":"viewof fSumEval = leanEditor({\n docArray: [\n`import fib\nopen nat list`,\n `#eval (range 10).map fib_sum\n#eval (range 10).map (λ m, fibonacci (m+1) - 1)\n\n#eval (range 10).map fib_odd_sum\n#eval (range 10).map (λ m, fibonacci (2*m))\n\n#eval (range 10).map fib_even_sum\n#eval (range 10).map (λ m, fibonacci (2*m-1) - 1)`\n ],\n docIndex: 1,\n fileName: 'fib_formula_sum_eval1.lean',\n displayMode: 1,\n lineNumbers: false,\n height: '275px',\n header: html``,\n}, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1672,"value":"md`🤔 You might have noticed something strange about the last \\`#eval\\` statement. When ${tex`m=0`}, what should the expression \\`fibonacci (2*m-1) - 1\\` evaluate to? Try typing \\`#eval 0-1\\` above and you might be surprised. The explanation is that subtraction on Lean's nats is a [\"total function\"](https://softwareengineering.stackexchange.com/questions/334874/in-the-context-of-functional-programming-what-are-total-functions-and-partia) and so it *must* return another nat. Thus when \\`a < b\\`, \\`a - b\\` is defined to be \\`0\\`. In any case, as mentioned above, we will only be proving things about this function when \\`m > 0\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1674,"value":"sectionSumOdd = md`### Sum of odd Fibonacci numbers`","pinned":false,"hidden":false,"mode":"ojs"},{"id":966,"value":"$35","pinned":false,"hidden":false,"mode":"ojs"},{"id":224,"value":"viewof f2 = fibFormulasEditor(2, invalidation, { height: '225px', footer: stepEditor(steps) })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1680,"value":"sectionSumEven = md`### Sum of even Fibonacci numbers:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1057,"value":"md`The next identity is for the sum of even Fibonacci numbers:\n\n**Theorem**: For all positive natural numbers ${tex`n`}:\n\n${tex.block`1 + \\sum_{m=0}^{n-1}F_{2m} = F_{2n-1}.`}\n\n*Proof*: The basic idea is still to extract the largest term of the sum and then use the induction hypothesis + definition of Fibonacci numbers. The only wrinkle is that our induction starts at 1 instead of 0 (since we only want to prove this for ${tex`n>0`}):\n- ${tex`n=1`}: the LHS is ${tex`1 + F_0 = 1`} and the RHS is ${tex`F_{2\\times1-1} = F_1 = 1`}.\n- Assuming the identity holds for ${tex`n`}, we show ${tex`1 + \\sum_{m=0}^{n}F_{2m} = F_{2n+1},`} by manipulating the LHS:\n${tex.block`\\begin{aligned}\n1 + \\sum_{m=0}^{n}F_{2m} &= 1 + \\sum_{m=0}^{n-1}F_{2m} + F_{2n}\\\\\n&= F_{2n-1} + F_{2n}\\\\\n&= F_{2n+1}.\n\\end{aligned}`}\n${tex`\\square`}\n\nThe Lean proof looks like this:\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":226,"value":"viewof f3 = fibFormulasEditor(3, invalidation, { height: '375px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1090,"value":"$36","pinned":false,"hidden":false,"mode":"ojs"},{"id":1683,"value":"sectionSumAll = md`### Sum of Fibonacci numbers:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1215,"value":"md`Here's the final Fibonacci sum identity. I will omit the informal proof, but it goes almost exactly as the ones above (use induction, split the sum, apply the definition of Fibonacci, etc.). [We could also prove it from the two above identities, but that turns out to require more manipulation.]`","pinned":false,"hidden":false,"mode":"ojs"},{"id":228,"value":"viewof f4 = fibFormulasEditor(4, invalidation, { height: '200px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1218,"value":"md`The above Lean proof makes use of the \\`simp\\` tactic. Roughly speaking, it attempts to simplify the goal by repeatedly rewriting it using its library of known facts (anything in the imported libraries which are tagged with the \\`simp\\` attribute as well as anything included in the list that follows). In this case, it saves us from writing explicitly a long list of lemmas in a \\`rw\\` statement.\n\nProofs using more powerful tactics tend to be more concise and hence more opaque (though Lean does have capabilities for \"tracing\" the behavior of tactics). \n\n### *See [Part 2](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars) for formalizations of certain objects counted by Fibonacci numbers (including some graphics driven by Lean code)*.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":145,"value":"$37","pinned":false,"hidden":false,"mode":"ojs"},{"id":1760,"value":"md`The Lean editor cells above are created by the functions \\`leanEditor\\` and \\`leanEditorFrom\\` from [another notebook](https://observablehq.com/@bryangingechen/hello-lean-prover#docArrayDoc). To use them here, we have to \"\\`import\\`\" them into this notebook with the following command (which also imports several other useful functions). We override the \\`transportOpts\\` so that we can load a custom ZIP bundle of Lean files (described below).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4,"value":"import {leanEditor, leanEditorFrom, leanControl, leanHL, parseLeanMsgs} with {transportOpts} from '@bryangingechen/hello-lean-prover'","pinned":true,"hidden":false,"mode":"ojs"},{"id":1784,"value":"md`Uncomment the following cell for a form that lets you reset the Lean server (useful for debugging):`","pinned":false,"hidden":false,"mode":"ojs"},{"id":125,"value":"// leanControl","pinned":false,"hidden":false,"mode":"ojs"},{"id":1800,"value":"$38","pinned":false,"hidden":false,"mode":"ojs"},{"id":1767,"value":"transportOpts = {\n const prefix = 'https://bryangingechen.github.io/lean/lean-web-editor/';\n return {\n javascript: prefix+'lean_js_js.js', // Lean server compiled to asm.js with Emscripten (won't be downloaded or used unless your browser doesn't support WASM)\n webassemblyJs: prefix+'lean_js_wasm.js', // JS code generated by Emscripten to call...\n webassemblyWasm: prefix+'lean_js_wasm.wasm', // Lean server compiled to WASM by Emscripten\n libraryZip: prefix+'libfib.zip', // bundle of .olean files\n };\n}","pinned":true,"hidden":false,"mode":"ojs"},{"id":1792,"value":"md`There are two types of Lean editors in this notebook, read-only editors, which are labeled with \"\\`fib_formulas.lean\\` (X/5)\" and non-read-only editors, which let the reader experiment with \\`#eval\\` statements.\n\nThe read-only editors contain parts of the following array, which is generated by [splitting](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/split) a string containing the first part of the Lean code in the \\`lean-fibonacci\\` repository:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":73,"value":"$39","pinned":false,"hidden":false,"mode":"ojs"},{"id":1805,"value":"md`I use this array to create the following \"editor factory\" function by passing an options object to \\`leanEditorFrom\\` with \\`fibFormulas\\` as the \\`docArray\\` field.\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":97,"value":"fibFormulasEditor = leanEditorFrom({\n docArray: fibFormulas,\n fileName: 'fib_formulas.lean',\n readOnly: true,\n lineNumbers: false,\n height: 150,\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":1838,"value":"md`As an example, here's the source of [the read-only cell that shows part 4/5](#f3):\n\\`\\`\\`js\nviewof f3 = fibFormulasEditor(3, invalidation, { height: 375 })\n\\`\\`\\`\n\nHere and elsewhere, you'll see [\\`invalidation\\`](https://observablehq.com/@mbostock/disposing-content) as an argument to various functions that create editors. This is a special [\"Promise\" object](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Using_promises) that is defined by Observable's runtime which resolves when a cell is re-run. If you're not familiar with promises, you can just think of this as something that helps ensure that the editor cleans up resources when it's destroyed.\n\nThe \\`viewof f3\\` part just names the cell and its output. While the value \"\\`f3\\`\" of this particular editor is not actually used elsewhere in the notebook, naming cells also creates anchors that we can then link to, as I did just above.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":2026,"value":"md`[One of the read-only editors](#f2) has a special footer element with buttons that step forwards / backwards through a multi-step explanation. This is implemented using the \\`stepEditor\\` function from [this notebook](https://observablehq.com/@bryangingechen/stepping-through-currying-in-lean).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1930,"value":"import {stepEditor} from '@bryangingechen/stepping-through-currying-in-lean'","pinned":false,"hidden":false,"mode":"ojs"},{"id":2033,"value":"md`For convenience, here's what the source of that editor cell looks like:\n\\`\\`\\`js\nviewof f2 = fibFormulasEditor(2, invalidation, { height: 225, footer: stepEditor(steps) })\n\\`\\`\\`\nThe input to \\`stepEditor\\` is the following array \\`steps\\` whose entries are objects describing the state of the footer and the highlighting in the editor in each \"step\". Here I only use two fields of each state object:\n- \\`desc\\` contains an HTML element to be displayed in the footer (using the \\`md\\` function), and \n- \\`marks\\` contains an array of CodeMirror ranges to highlight. \n\nSee the [\\`stepEditor\\` notebook](https://observablehq.com/@bryangingechen/stepping-through-currying-in-lean) for full documentation:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1937,"value":"$3a","pinned":false,"hidden":false,"mode":"ojs"},{"id":1813,"value":"$3b","pinned":false,"hidden":false,"mode":"ojs"},{"id":2123,"value":"md`## Version history:\n- [2019/07/28](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums@2106): first publish\n- [2019/08/15](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums@2128): Compatibility with [2019/08/15 update to \"Hello, Lean prover!\"](https://observablehq.com/@bryangingechen/hello-lean-prover@5203).\n- [2020/03/06](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums@2130): update for Lean 3.6.1c\n- [2020/04/19](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums@2133): update for Lean 3.9.0c\n- [2020/05/22](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums@2135): update for Lean 3.14.0c\n- 2021/01/28: update for Lean 3.26.0c\n`","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W3c","stdlib":"1","titling":"auto"}