31:T60f,md`As you hopefully saw earlier by experimenting, the number of bees in each "column" of the family tree is a Fibonacci number. Let's prove this: **Theorem**: The number of ancestors of a drone ${tex`n`} generations back is equal to ${tex`F_{n+1}.`} *Proof*: This holds for the ${tex`n=0,1`} cases, and the remaining case is a consequence of this: **Lemma**: Let ${tex`A_j`} be the list of ${tex`j`}th ancestors of a drone read from top to bottom in the diagram above. Then for all ${tex`n \in \mathbb{N}`}, ${tex.block`A_{n+2} = A_{n+1} + A_n,`} where ${tex`+`} denotes concatenation of lists. *Proof of lemma*: Note that ${tex`A_n`} is just \`drone.ancestors n\`, which is defined recursively as the concatenation of the parents of each of the elements of ${tex`A_{n-1}`} (with ${tex`A_0`} defined to be "D"). Let's write this as ${tex`A_n = P(A_{n-1})`}, where ${tex`P`} denotes the "get parents, then concatenate" function. Then an informal proof by induction goes as follows: - When ${tex`n=0`}, we can check that ${tex`A_2=[Q,D], A_1=[Q], A_0=[D]`}, so the desired identity holds. - Assuming ${tex`A_{m+2} = A_{m+1} + A_m`} holds for all ${tex`m\leq n`}, we have: ${tex.block`\begin{aligned} A_{(n+1)+2}&=P(A_{n+2})&\text{by definition of $A_{m}$}\\ &= P(A_{n+1} + A_n)&\text{by the inductive hypothesis}\\ &= P(A_{n+1}) + P(A_n)&\text{since we can either concatenate}\\ & &\text{before or after getting the parents}\\ &= A_{n+2} + A_{n+1}, &\text{by definition of $A_m$} \end{aligned}`} which concludes the proof. ${tex`\square`}`32:T582,md`This proof pattern-matches on three arguments, a nat \`n\`, a \`list\` of \`car\`s \`cs\`, and a proof \`h\` that \`cs ∈ packings n\`. The final ${tex`n+2`} case of the induction uses a few new ingredients: - the \`at\` syntax for \`simp\`, which applies \`simp\` to a named hypothesis in the tactic, rather than to the goal, - the \`rcases\` tactic, which lets us destructure a hypothesis into named parts, and - the \`all_goals\` tactic, which applies the tactic(s) inside its curly braces to all goals. Here's what happens in the \`rcases\`, \`all_goals\` steps. Initially, we have:

65:23: goal

packings_size : ∀ {n : ℕ} {cs : list car},
  cs ∈ packings n → sum_size cs = n,
n : ℕ,
cs : list car,
h :
  (∃ (a : list car), a ∈ packings (succ n) ∧ rabbit :: a = cs) ∨
    ∃ (a : list car), a ∈ packings n ∧ cadillac :: a = cs
⊢ sum_size cs = n + 2

In words, \`h\` states that: > **Either** there exists a list \`a ∈ packings (n+1)\` such that \`cs = rabbit :: a\`, **or** there exists a list \`a ∈ packings n\` such that \`cs = cadillac :: a\`. To use a hypothesis of this sort, we have to show that the goal holds "either way". Thus we anticipate splitting the goal state into two, one for each branch of this hypothesis. ` 33:T61a,md` When we apply \`rcases h with ⟨cs', h₁, h₂⟩ | ⟨cs', h₁, h₂⟩\`, the expression that comes after \`with\` represents a pattern that is matched against \`h\`: - First, the pipe \`|\` matches with the "or", splitting both the pattern and \`h\`. - Then, the first angle-bracketed expression \`⟨cs', h₁, h₂⟩\` is matched to \`\`\` (∃ (a : list car), a ∈ packings (succ n) ∧ rabbit :: a = cs). \`\`\` Note that this expression decomposes into 3 parts so that: - \`cs'\` matches \`(a : list car)\`, - \`h₁\` matches \`a ∈ packings (succ n)\`, and - \`h₂\` matches \`rabbit :: a = cs\`. - The second expression \`⟨cs', h₁, h₂⟩\` is matched to \`\`\` ∃ (a : list car), a ∈ packings n ∧ cadillac :: a = cs. \`\`\` with: - \`cs'\` matching \`(a : list car)\`, - \`h₁\` matching \`a ∈ packings n\`, and - \`h₂\` matching \`cadillac :: a = cs\`. As anticipated, this results in **two** goals, one for each case of the or-expression:

66:46: goal

2 goals
packings_size : ∀ {n : ℕ} {cs : list car},
  cs ∈ packings n → sum_size cs = n,
n : ℕ,
cs cs' : list car,
h₁ : cs' ∈ packings (succ n),
h₂ : rabbit :: cs' = cs
⊢ sum_size cs = n + 2

packings_size : ∀ {n : ℕ} {cs : list car},
  cs ∈ packings n → sum_size cs = n,
n : ℕ,
cs cs' : list car,
h₁ : cs' ∈ packings n,
h₂ : cadillac :: cs' = cs
⊢ sum_size cs = n + 2

` 34:T413,md`Next we turn to the "if" direction: any configuration of Rabbits and Cadillacs with total car length \`n\` is an element of \`packings n\`. *Proof*: The \`n=0, 1\` cases can be proved by direct enumeration of the possibilities. Now assume that any configuration of length \`m\` at most \`n+1\` is in \`packings m\`. Given a list \`cs\` representing a configuration of cars with total car length \`n+2\`, consider its first element: - If the first element of \`cs\` is a Rabbit, then the remainder is a configuration of with total car length \`n+1\`, and the inductive hypothesis tells us that it is an element of \`packings (n+1)\`. But then \`cs\` is a member of \`packings (n+2)\`, by examining the definition. - Otherwise, the first element of \`cs\` is a Cadillac, and a very similar argument shows that \`cs\` is a member of \`packings (n+2)\` in this case as well. Formalizing this is more of a pain (though maybe that's because of my poor Lean skills). Here's a proof that the only configuration with length zero is the empty one:`35:T52d,md`The proofs here use several other new tactics. In the proof of \`car_size_ne_zero\`, \`cases\` is a less powerful version of \`rcases\`: here it splits the goal into a case where \`c = rabbit\` and one where \`c = cadillac\`. The semicolon \`;\` is similar to \`all_goals\`; it applies the following tactic to both goals. The \`contradiction\` tactic is useful for finishing off proofs that something cannot occur: in this proof the two goals are \`size rabbit = 1 ≠ 0\` and \`size cadillac = 2 ≠ 0\`. In \`sum_size_zero\`, we pattern-match on the \`list\` \`cs\`: - it can either be the empty list \`[]\` (in which case the proof is \`rfl\`), or - it can take the form \`c::cs\` (with \`c : car\` the head of the list and \`cs : list car\` the tail). [Recall that when pattern-matching, the old \`cs\` gets shadowed by the \`cs\` in the pattern.] - This case is impossible, so we first use the \`exfalso\` tactic to change the goal to \`false\`. - The rest of the proof extracts a contradiction from \`size c = 0\` and the just-proved \`car_size_ne_zero\`. The \`exact\` tactic closes a goal by providing an explicit term of the type required; in this case, \`car_size_ne_zero c h.2\` has type \`false\`. Next is the formal proof that the only configuration with length 1 is the singleton list \`[rabbit]\`:`36:T582,fibBees = String.raw`import data.list.range @[reducible] def fibonacci : ℕ → ℕ | 0 := 0 | 1 := 1 | (n+2) := fibonacci n + fibonacci (n+1) --- inductive bee : Type | queen : bee | worker : bee | drone : bee open bee list instance : has_repr bee := ⟨λ s, match s with | queen := "Q" | worker := "W" | drone := "D" end⟩ --- namespace bee def parents : bee → list bee | queen := [queen, drone] | worker := [queen, drone] | drone := [queen] def ancestors (b : bee) : ℕ → list bee | 0 := [b] | (n+1) := ((ancestors n).map parents).join --- def tree_json : bee → ℕ → string | b 0 := "{\"name\":\"" ++ repr b ++ "\"}" | b (n+1) := "{\"name\":\"" ++ repr b ++ "\",\"children\":[" ++ string.intercalate "," (b.parents.map (λ p, p.tree_json n)) ++ "]}" --- lemma drone_ancestors_concat : ∀ (n : ℕ), drone.ancestors (n+2) = drone.ancestors (n+1) ++ drone.ancestors n | 0 := rfl | (n+1) := begin change ((ancestors _ (n+2)).map _).join = _, conv { to_lhs, rw [drone_ancestors_concat n, map_append, join_append], }, refl, end --- theorem drone_ancestors_length_eq_fib_succ : ∀ (n : ℕ), (drone.ancestors n).length = fibonacci (n+1) | 0 := rfl | 1 := rfl | (n+2) := begin rw [drone_ancestors_concat, length_append, drone_ancestors_length_eq_fib_succ n, drone_ancestors_length_eq_fib_succ (n+1), add_comm], refl, end end bee`.split('\n---\n')37:Ta2b,fibCars = String.raw`import data.list.range @[reducible] def fibonacci : ℕ → ℕ | 0 := 0 | 1 := 1 | (n+2) := fibonacci n + fibonacci (n+1) --- inductive car : Type | rabbit : car | cadillac : car open car list nat instance : has_repr car := ⟨λ s, match s with | rabbit := "R" | cadillac := "C" end⟩ --- namespace car @[reducible] def size : car → ℕ | rabbit := 1 | cadillac := 2 @[reducible] def sum_size (cs : list car) : ℕ := (cs.map size).sum lemma sum_size_cons (c : car) (cs : list car) : sum_size (c :: cs) = sum_size cs + c.size := by simp only [sum_size, sum_cons, map, add_comm] --- @[reducible] def packings : ℕ → list (list car) | 0 := [[]] | 1 := [[rabbit]] | (n+2) := (packings (n+1)).map (cons rabbit) ++ (packings n).map (cons cadillac) --- theorem num_packings_eq_fib : ∀ (n : ℕ), (packings n).length = fibonacci (n+1) | 0 := rfl | 1 := rfl | (n+2) := begin simp [packings, fibonacci, add_left_comm, add_comm], rw [num_packings_eq_fib n, num_packings_eq_fib (n+1), add_left_comm, add_right_inj, fibonacci], end --- theorem packings_size : ∀ {n : ℕ} {cs : list car} (h : cs ∈ packings n), sum_size cs = n | 0 cs h := begin rw mem_singleton.1 h, refl, end | 1 cs h := begin rw mem_singleton.1 h, refl, end | (n+2) cs h := begin simp [packings] at h, rcases h with ⟨cs', h₁, h₂⟩ | ⟨cs', h₁, h₂⟩, all_goals { rw [←h₂, sum_size_cons, size, packings_size h₁], }, end --- lemma car_size_ne_zero (c : car) : size c ≠ 0 := by cases c; contradiction lemma sum_size_zero : ∀ {cs : list car} (h : sum_size cs = 0), cs = [] | [] _ := rfl | (c::cs) h := begin exfalso, rw [sum_size_cons, add_eq_zero_iff] at h, exact car_size_ne_zero c h.2, end --- lemma sum_size_one : ∀ {cs : list car} (h : sum_size cs = 1), cs = [rabbit] | [] h := by contradiction | (rabbit::cs) h := begin rw [sum_size_cons] at h, simp, exact sum_size_zero (succ.inj h), end | (cadillac::cs) h := begin rw [sum_size_cons] at h, have : sum_size cs + 1 = 0 := succ.inj h, contradiction, end --- theorem all_packings : ∀ {n : ℕ} {cs : list car} (h : sum_size cs = n), cs ∈ packings n | 0 cs h := by simp [packings, sum_size_zero h] | 1 cs h := by simp [packings, sum_size_one h] | (n+2) [] h := by contradiction | (n+2) (rabbit::cs) h := begin rw [sum_size_cons, add_left_inj 1] at h, simp [packings, all_packings, h], end | (n+2) (cadillac::cs) h := begin rw [sum_size_cons, add_left_inj 2] at h, simp [packings, all_packings, h], end end car`.split('\n---\n')38:[] 2f:{"title":"Fibonacci formalized 2: bees and cars","cells":[{"id":0,"value":"md`# Fibonacci formalized 2: bees and cars\n\nIn this notebook we formalize two applications of the Fibonacci numbers in counting problems in the Lean theorem prover. See [Part 1](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums) for an introduction and more context.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1616,"value":"contents = md`## Contents\n\n[Part 1](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums):\n- [Fibonacci numbers](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums#sectionStart)\n- [Formulas 🧮](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums#sectionFormulas)\n\n**Part 2**:\n- [Bees 🐝](#sectionBees)\n- [Cars 🚗](#sectionCars)\n- [Implementation notes for Part 2](#sectionImplementation)\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":434,"value":"sectionBees = md`## Bees 🐝\n\nMore than 900 years ago, Leonardo of Pisa [wrote about Fibonacci numbers](https://www.math.utah.edu/~beebe/software/java/fibonacci/liber-abaci.html) in the book **Liber Abaci**. He asked a question about the number of pairs of rabbits in a rather silly model of population growth and gave the answer, which happened to be the 13th Fibonacci number. Fibonacci numbers have since appeared in other applications to biology (notably, in [phyllotaxis](https://en.wikipedia.org/wiki/Phyllotaxis#Repeating_spiral)). In this section, I'll formalize a model for the family trees of bees in which Fibonacci numbers also make an appearance.\n\nFirst, our model of bees in Lean will be [an enum type](https://en.wikipedia.org/wiki/Enumerated_type). Bees are either *queens*, *workers* or *drones*:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":287,"value":"viewof fB1 = fibBeesEditor(1, invalidation, { height: '250px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1202,"value":"md`The \\`has_repr\\` instance tells Lean to print a term of type \\`bee\\` as \\`Q\\`, \\`W\\` or \\`D\\`. \n\nNow we sketch our model of [honeybee biology](https://en.wikipedia.org/wiki/Honey_bee#Sexes_and_castes):\n- The queen is the mother of all the bees in her hive: workers and virgin queens (which are female), and drones (which are male). \n- Female bees are hatched from eggs that the queen has fertilized with sperm from drones of other hives, whereas drones are hatched from unfertilized eggs. \n- Thus, female bees have two parents, a queen and a drone, and drones have only one parent, a queen.\n\nWe encode this in the definitions of a \\`parents\\` function which returns lists of the parent types for a given bee and an \\`ancestors\\` function which returns a list of bees in the \\`n\\`th generation of ancestors for a given bee.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":292,"value":"viewof fB2 = fibBeesEditor(2, invalidation, { height: '200px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":503,"value":"viewof fBeeEval = leanEditor({\n docArray: [\n `import fib\nopen bee list nat`,\n `#eval drone.parents.map parents\n\n#eval (range 5).map drone.ancestors\n\n#eval (drone.ancestors 7).length\n#eval fibonacci 8`,\n ],\n docIndex: 1,\n fileName: 'fib_bees_eval.lean',\n displayMode: 1,\n lineNumbers: false,\n height: '200px',\n header: html`Test out the above functions here:`,\n}, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1227,"value":"md`Play around with the numbers above until you've convinced yourself that the number of ancestors of a drone at the \\`n\\`th generation is equal to \\`fibonacci (n+1)\\`.\n\nWe now take a quick diversion to show off how we can visualize this data using JavaScript in Observable. As above, we can parse the messages from a given Lean editor (though here we need a little string pre-processing):`","pinned":false,"hidden":false,"mode":"ojs"},{"id":667,"value":"parseLeanMsgs(fBeeEval.msgs, msg => msg.replace(/[A-Z]/g,'\"$&\"'))","pinned":true,"hidden":false,"mode":"ojs"},{"id":1230,"value":"md`Now let's draw the family tree of a drone!\n\nFirst, we get Lean to output a string encoding a nested JS Object in JSON format:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":608,"value":"viewof fB3 = fibBeesEditor(3, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":612,"value":"viewof fBeeEvalTree = leanEditor(\n {\n docArray: [\n `import fib\nopen bee list nat`,\n `#eval drone.tree_json 8`\n ],\n docIndex: 1,\n fileName: 'fib_bees_eval_tree.lean',\n displayMode: 1,\n lineNumbers: false,\n height: '200',\n header: html``\n },\n invalidation\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":1247,"value":"md`Try clicking on the inspector cell below to expand the parsed output object, \\`treeData\\`:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":644,"value":"// if first message is undefined, return empty object\ntreeData = {\n const parsedMsgs = parseLeanMsgs(fBeeEvalTree.msgs.filter(({caption}) => caption === 'eval result'))\n .filter((msg) => typeof msg === 'object');\n return parsedMsgs[0] || {};\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1234,"value":"md`We can create a graphic of the family tree with [d3's tree layout](https://github.com/d3/d3-hierarchy/blob/master/README.md#tree) using a cell imported from the [\"Tidy Tree\"](https://observablehq.com/@d3/tidy-tree) notebook:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":647,"value":"treeChart","pinned":false,"hidden":false,"mode":"ojs"},{"id":1275,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"id":295,"value":"viewof fB4 = fibBeesEditor(4, invalidation, { height: '225px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1295,"value":"md`The Lean code follows the same familiar strategy: we use pattern matching on \\`n\\` to prove the equality inductively:\n- Case 0 is \\`rfl\\`, as you might expect. \n- For the \\`(n+1)\\` case, \n - We first \\`change\\` the goal to something equivalent (essentially expanding out the definition of \\`ancestors\\`). Note the use of underscores in \\`change\\` for bits that we don't care to write out – Lean can fill in those bits automatically!\n - Then we use the powerful [\\`conv\\`](https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md) (conversion mode) tactic to apply rewrites only to the left-hand side of the goal.\n - We finish with the \\`refl\\` tactic, which tells Lean to try to recognize the LHS and RHS as the same (basically it tries a few tricks before attempting to finish with a \\`rfl\\` term).\n\nThe formal proof of the theorem that a drone has ${tex`F_{n+1}`} ${tex`n`}th ancestors is then relatively straightforward:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":298,"value":"viewof fB5 = fibBeesEditor(5, invalidation, { height: '275px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":436,"value":"sectionCars = md`## Cars 🚗\n\n*This section is based on Problem 12.2 / Solution 12.20 in **\"Mathematical Thinking: Problem-solving and Proofs\"** (2nd edition) by John P. D'Angelo and Douglas B. West. I bought this book in high school and learned a ton from it!*\n\nSuppose a parked Volkswagen Rabbit

takes up one unit of space and a parked Cadillac limousine

takes up two units of space.\n\nHow many ways are there to fill a curb of length ${tex`n`} with parked Rabbits and Cadillacs? Equivalently, how many lists consisting of 1's and 2's sum up to ${tex`n`}? \n\nYou can probably guess – Fibonacci numbers are involved.\n\nLet's start the formalization by defining our \\`car\\` type and telling Lean how to print its elements:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":323,"value":"viewof fC1 = fibCarsEditor(1, invalidation, { height: '225px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1359,"value":"md`Now we formalize:\n- the car length function (called \\`size\\`),\n- a function \\`sum_size\\` that computes the total size of a list of cars, and\n- prove a simple result that will be useful later\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":336,"value":"viewof fC2 = fibCarsEditor(2, invalidation, { height: '275px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1446,"value":"md`Note our naming convention (commonly seen in other functional programming languages): \\`c\\` for a single \\`car\\`, \\`cs\\` for a \\`list\\` of \\`car\\`s.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1364,"value":"md`Now we define a recursive function which returns a list of parking configurations. When the curb has length 0 or 1, there's only one way to fill the curb, with no cars or with a single Rabbit, respectively. For longer curbs, we can get a packing of length ${tex`n+2`} by either:\n- parking a Rabbit in the first space and then filling the remaining curb with any packing of length ${tex`n+1`}, or\n- parking a Cadillac in the first space and then filling the remaining curb with any packing of length ${tex`n`}.\n\nWe'll refer to this list as ${tex`\\mathcal{P}(n)`} (and as \\`packings n\\` in Lean, since we're \"packing\" a curb of fixed length with Rabbits and Cadillacs). Below, [\\`cons\\`](https://en.wikipedia.org/wiki/Cons) is the function of type \\`car → list car → list car\\` that appends an element to the beginning of a list (later we'll see the notation \\`x::xs\\` for \\`cons x xs\\`):`","pinned":false,"hidden":false,"mode":"ojs"},{"id":342,"value":"viewof fC3 = fibCarsEditor(3, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":821,"value":"viewof fCarsEval = leanEditor({\n docArray: [\n `import fib\nopen car list nat`,\n `#eval packings 8\n\n#eval size cadillac + size rabbit\n\n#eval sum_size [cadillac, rabbit, cadillac]\n\n#eval ((range 10).map packings).map length\n#eval (range 11).map fibonacci`,\n ],\n docIndex: 1,\n fileName: 'fib_cars_eval.lean',\n displayMode: 1,\n lineNumbers: false,\n height: '200px',\n header: html`Experiment with size, sum_size, and packings here:`,\n}, invalidation)","pinned":false,"hidden":false,"mode":"ojs"},{"id":825,"value":"parsedCars = parseLeanMsgs(fCarsEval.msgs.filter(({caption}) => caption === 'eval result'),\n msg => msg.replace(/[A-Z]/g,'\"$&\"'))","pinned":false,"hidden":false,"mode":"ojs"},{"id":1376,"value":"md`After importing the output of \\`packings\\` into Observable, we can draw the generated parking configurations!`","pinned":false,"hidden":false,"mode":"ojs"},{"id":833,"value":"configurations = {\n if (!parsedCars[0] || !Array.isArray(parsedCars[0])) return md`Enter \\`#eval packings N\\` for some \\`N\\` (less than 15 or so if you don't want to run out of memory) at the start of the above Lean editor to see a graphic showing up to 100 of the packings of Rabbits and Cadillacs that fill up \\`N\\` parking spaces.`\n return md`### ${parsedCars[0].length} configurations of length ${parsedCars[0][0].length}:

${parsedCars[0]\n .map(packing => packing.slice(0,100).map(s => `

`).join(''))\n .join('
')}

\n\n${parsedCars[0].length > 100 ? `${parsedCars[0].length-100} packings omitted.` : ''}`\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1393,"value":"md`Now we can prove the following:\n\n**Theorem**: ${tex`\\mathcal{P}(n)`} has length ${tex`F_{n+1}`}.\n\n*Proof*: Let ${tex`|\\mathcal{P}(m)|`} denote the length of the list ${tex`\\mathcal{P}(m)`}. Note that ${tex`\\mathcal{P}(n+2)`} is the concatenation of a list of length ${tex`\\mathcal{P}(n)`} (since putting a Rabbit at the beginning of each element of ${tex`\\mathcal{P}(n)`} does not change the number of such packings) and a list of length ${tex`\\mathcal{P}(n+1)`}. Now compare the facts ${tex`|\\mathcal{P}(0)| = 1, |\\mathcal{P}(1)| = 1,`} and ${tex`|\\mathcal{P}(n+2)| = |\\mathcal{P}(n)| + |\\mathcal{P}(n+1)|`} with the definition of ${tex`F_{n}`}. ${tex`\\square`}\n\nThe Lean proof is straightforward (modulo figuring out what lemmas need to go in \\`simp\\` vs. \\`rw\\`):\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":352,"value":"viewof fC4 = fibCarsEditor(4, invalidation, { height: '250px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1383,"value":"md`However, we're not done yet. What if \\`packings\\` missed some configurations of Rabbits and Cadillacs? And how do we know that it doesn't return some incorrect configurations? Luckily, we can prove:\n\n**Theorem**: A configuration of Rabbits and Cadillacs is in \\`packings n\\` if and only if the total length of the cars is \\`n\\`.\n\nWe first prove the \"only if\" direction: every configuration in \\`packings n\\` has total car length equal to \\`n\\`:\n\n*Proof*: We first check that this is true when \\`n=0, 1\\`. Then assuming this holds for all \\`m\\` up to \\`n+1\\`, note that each configuration in \\`packings (n+2)\\` consists of either:\n- a Rabbit (which has length 1) plus a configuration in \\`packings (n+1)\\` (which has length \\`n+1\\`, by induction), or\n- a Cadillac (which has length 2) plus a configuration in \\`packings n\\` (which has length \\`n\\`, by induction).\n\nIn both cases, the total length of the cars is \\`n+2\\`, as desired. ${tex`\\square`}\n\nIn Lean:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":344,"value":"viewof fC5 = fibCarsEditor(5, invalidation, { height: '375px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1677,"value":"$32","pinned":false,"hidden":false,"mode":"ojs"},{"id":1437,"value":"$33","pinned":false,"hidden":false,"mode":"ojs"},{"id":1680,"value":"md`The two goals are nearly the same, so we try applying a tactic to both goals at the same time, using:\n\\`\\`\\`\nall_goals { rw [←h₂,\n sum_size_cons,\n size,\n packings_size h₁], },\n\\`\\`\\`\n\nEven though the \\`h₁\\` and \\`h₂\\` in the \\`rw\\` string are different in the two goals, the same sequence of rewrites suffices in both cases.\n\nSadly, we can only inspect the changes to the first goal when we click around in \\`all_goals\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":1547,"value":"$34","pinned":false,"hidden":false,"mode":"ojs"},{"id":346,"value":"viewof fC6 = fibCarsEditor(6, invalidation, { height: '250px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1556,"value":"$35","pinned":false,"hidden":false,"mode":"ojs"},{"id":348,"value":"viewof fC7 = fibCarsEditor(7, invalidation, { height: '275px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1563,"value":"md`We pattern-match on the list \\`cs\\`, but this time we split into *three* cases: \n- the empty list \\`[]\\`, \n- lists \\`(rabbit::cs)\\` that begin with \\`rabbit\\`, and \n- lists \\`(cadillac::cs)\\` that begin with \\`cadillac\\`. \n\nAs in the previous lemma, much of this proof is ruling out the invalid cases.\n\nThe final formalization pulls all of this together:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":350,"value":"viewof fC8 = fibCarsEditor(8, invalidation, { height: '350px' })","pinned":false,"hidden":false,"mode":"ojs"},{"id":1661,"value":"md`The proof is divided into 5 cases using pattern-matching:\n\n- \\`n = 0\\` (essentially \\`sum_size_zero\\`),\n- \\`n = 1\\` (\\`sum_size_one\\`),\n- \\`n\\` matches \\`(n+2)\\` has 3 subcases:\n - \\`cs = []\\` (impossible),\n - \\`cs\\` matches \\`(rabbit::cs)\\`, and\n - \\`cs\\` matches \\`(cadillac::cs)\\`.\n\nAs in our informal proof, the last two cases are proved nearly the same way, with just a slight difference in arithmetic.\n\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":145,"value":"sectionImplementation = md`## Implementation notes\n\nMuch of the following is the same as in part 1, so [here's a link to the implementation notes there](https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums#sectionImplementation). I'll only explain the parts which are related to the two main graphics above.`","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":1572,"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":1742,"value":"// leanControl","pinned":true,"hidden":false,"mode":"ojs"},{"id":1749,"value":"md`For the family tree of a honeybee drone, I import a chart from [the \\`tidy-tree\\` notebook](https://observablehq.com/@d3/tidy-tree).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":642,"value":"import {chart as treeChart} with {treeData as data, treeWidth as width} from '@d3/tidy-tree'","pinned":true,"hidden":false,"mode":"ojs"},{"id":1752,"value":"md`I override two of the cells in that notebook. First and foremost, I override the main data cell with the output of a Lean editor above so that the D3 code builds the desired tree. Second, I override the \\`width\\` built-in variable so that the tree doesn't take up quite as much space:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":655,"value":"treeWidth = 0.8*width","pinned":false,"hidden":false,"mode":"ojs"},{"id":1756,"value":"md`Here are the arrays of strings containing the theorems proved in this notebook and the editor factories that use them. As in Part 1, these are generated by splitting a Lean file in [the \\`lean-fibonacci\\` repo](https://github.com/bryangingechen/lean-fibonacci). Note the use of [\\`String.raw\\`](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/String/raw) to save writing some escape sequences.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":283,"value":"$36","pinned":false,"hidden":false,"mode":"ojs"},{"id":281,"value":"fibBeesEditor = leanEditorFrom({\n docArray: fibBees,\n fileName: 'fib_bees.lean',\n readOnly: true,\n height: 150,\n lineNumbers: false,\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":326,"value":"$37","pinned":false,"hidden":false,"mode":"ojs"},{"id":329,"value":"fibCarsEditor = leanEditorFrom({\n docArray: fibCars,\n fileName: 'fib_cars.lean',\n readOnly: true,\n height: 150,\n lineNumbers: false,\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":1763,"value":"md`The [\\`configurations\\`](#configurations) graphics cell is generated from the output of the Lean function \\`packings\\` with the following snippet:\n\n\\`\\`\\`js\nparsedCars[0]\n .map(packing => packing.slice(0,100)\n .map(s => \\`

\\`).join(''))\n .join('
')\n\\`\\`\\`\n\nWhat this does is create an HTML string with \\`\\` elements replacing the \\`R\\` and \\`C\\` characters. The SVG images (which I \"drew\") are below:\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":886,"value":"md`

This VW Rabbit is based on the flickr photo [\"1975 Volkswagen Rabbit\" by Curtis Perry](https://flic.kr/p/d6GHjJ).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":843,"value":"svgRabbit = svgDataURL``","pinned":false,"hidden":false,"mode":"ojs"},{"id":875,"value":"md`

This Cadillac limo is based on the flickr photo [\"72fltwd75\" by John W.](https://flic.kr/p/dDiKz4) of a 1972 Cadillac Fleetwood 75.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":845,"value":"svgCadillac = svgDataURL``","pinned":false,"hidden":false,"mode":"ojs"},{"id":851,"value":"function svgDataURL(svg) {\n return `data:image/svg+xml;utf8,${encodeURIComponent(`\n${svg}`)}`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":1803,"value":"md`## Version history:\n- [2019/07/28](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars@1786): first publish\n- [2019/08/15](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars@1807): 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-2-bees-and-cars@1810): update for Lean 3.6.1c\n- [2020/04/19](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars@1813): update for Lean 3.9.0c\n- [2020/05/22](https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars@1815): update for Lean 3.14.0c\n- 2020/07/04: update \\`sum_size_one\\` (\\`nat.succ_inj\\` was renamed to \\`nat.succ.inj\\`)\n`","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W38","stdlib":"1","titling":"auto"}