diff --git a/content/blog/00_aoc_coq.md b/content/blog/00_aoc_coq.md index 7554993..2bba71d 100644 --- a/content/blog/00_aoc_coq.md +++ b/content/blog/00_aoc_coq.md @@ -1,8 +1,7 @@ --- title: "Advent of Code in Coq - Day 1" -date: 2020-12-01T21:50:28-08:00 +date: 2020-12-02T18:44:56-08:00 tags: ["Advent of Code", "Coq"] -draft: true --- The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite @@ -21,19 +20,19 @@ problem statement: With this in mind, we can move on to writing some Coq! ### Defining the Functions -The first step to proving our code correct is to actually write the code! As a first -step, let's write a helper function that, given a number `x`, tries to find another number -`y` such that `x + y = 2020`. The code is quite simple: +The first step to proving our code correct is to actually write the code! To start with, +let's write a helper function that, given a number `x`, tries to find another number +`y` such that `x + y = 2020`. In fact, rather than hardcoding the desired +sum to `2020`, let's just use another argument called `total`. The code is quite simple: {{< codelines "Coq" "aoc-coq/day1.v" 7 14 >}} -Here, `is` is the list of numbers that we want to search, and `total` is the number -we want to add up to (`2020` in our particular case), and `x` is the same as it was in -the previous paragraph. We proceed by case analysis: if the list is empty, we can't +Here, `is` is the list of numbers that we want to search. +We proceed by case analysis: if the list is empty, we can't find a match, so we return `None` (the Coq equivalent of Haskell's `Nothing`). -On the other hand, if the list has at least one element, `y`, we see if it adds -up to `total`, and return `y` if it does. If it doesn't, we continue our search -into the rest of the list. +On the other hand, if the list has at least one element `y`, we see if it adds +up to `total`, and return `Some y` (equivalent to `Just y` in Haskell) if it does. +If it doesn't, we continue our search into the rest of the list. It's somewhat unusual, in my experience, to put the list argument first when writing functions in a language with [currying](https://wiki.haskell.org/Currying). However, @@ -92,7 +91,7 @@ hold for the empty list, which is the simplest possible list. In our case, this means `find_matching` searching an empty list. * The __inductive case__. Assuming that a property holds for any list `[b, c, ...]`, we want to show that the property also holds for -the list `[a, b, ...]`. That is, the property must remain true if we +the list `[a, b, c, ...]`. That is, the property must remain true if we prepend an element to a list for which this property holds. These two things combined give us a proof for _all_ lists, which is exactly @@ -105,7 +104,8 @@ an element to the list, this time a `3`, and conclude that `P [3,4]`. Repeating this twice more, we arrive at our desired fact: `P [1,2,3,4]`. When we write `induction is`, Coq will generate two proof goals for us, -one for the base case, and one for the inductive case. Since we have +one for the base case, and one for the inductive case. We will have to prove +each of them separately. Since we have not yet introduced the variables `k`, `x`, and `y`, they remain inside a `forall` quantifier at that time. To be able to refer to them, we want to use `intros`. We want to do this in both the @@ -147,14 +147,14 @@ Hev : None = Some y ``` Well, this doesn't make any sense. How can something be equal to nothing? -We ask Coq this question using `inversion Hev`. Effectively, `inversion` asks -the question: what are the possible ways we could have acquired `Hev`? +We ask Coq this question using `inversion Hev`. Effectively, the question +that `inversion` asks is: what are the possible ways we could have acquired `Hev`? Coq generates a proof goal for each of these possible ways. Alas, there are no ways to arrive at this contradictory assumption: the number of proof sub-goals is zero. This means we're done with the base case! The inductive case is the meat of this proof. Here's the corresponding part -of the proof: +of the Coq source file: {{< codelines "Coq" "aoc-coq/day1.v" 32 36 >}} @@ -175,7 +175,7 @@ x + y = k Following the footsteps of our informal description of the inductive case, Coq has us prove our property for `(a :: is)`, or the list `is` to which `a` is being prepended. Like before, we assume that our property holds for `is`. -This is represented in the __induction hypothesis__ `IHis`. It states that if we +This is represented in the __induction hypothesis__ `IHis`. It states that if `find_matching` finds a `y` in `is`, it must add up to `k`. However, `IHis` doesn't tell us anything about `a :: is`: that's our job. We also still have `Hev`, which is our assumption that `find_matching` finds a `y` in `(a :: is)`. @@ -186,13 +186,16 @@ Hev : (if x + a =? k then Some a else find_matching is k x) = Some y ``` The result of `find_matching` now depends on whether or not the new element `a` -adds up to `k`. We're not sure if this is the case. Fortunately, we don't need to be! +adds up to `k`. If it does, then `find_matching` will return `a`, which means +that `y` is the same as `a`. If not, it must be that `find_matching` finds +the `y` in the rest of the list, `is`. We're not sure which of the possibilities +is the case. Fortunately, we don't need to be! If we can prove that the `y` that `find_matching` finds is correct regardless of whether `a` adds up to `k` or not, we're good to go! To do this, we perform case analysis using `destruct`. -Our particular use of `destruct` says: check any possible value for `Nat.eqb (x+a) k`, -and create an equation `Heq` that tells us what that value is. `Nat.eqb` returns a boolean +Our particular use of `destruct` says: check any possible value for `x + a ?= k`, +and create an equation `Heq` that tells us what that value is. `?=` returns a boolean value, and so `destruct` generates two new goals: one where the function returns `true`, and one where it returns `false`. We start with the former. Here's the proof state: @@ -210,11 +213,11 @@ x + y = k ``` There is a new hypothesis: `Heq`. It tells us that we're currently -considering the case where `Nat.eqb` evaluates to `true`. Also, +considering the case where `?=` evaluates to `true`. Also, `Hev` has been considerably simplified: now that we know the condition of the `if` expression, we can just replace it with the `then` branch. -Looking at `Hev`, we can see that `a` is equal to `y`. After all, +Looking at `Hev`, we can see that our prediction was right: `a` is equal to `y`. After all, if they weren't, `Some a` wouldn't equal to `Some y`. To make Coq take this information into account, we use `injection`. This will create a new hypothesis, `a = y`. But if one is equal to the other, why don't we @@ -236,11 +239,11 @@ x + y = k We're close, but there's one more detail to keep in mind. Our goal, `x + y = k`, is the __proposition__ that `x + y` is equal to `k`. However, `Heq` tells us -that the __function__ `eqb` evaluates to `true`. These are fundamentally different. -One talks about mathematical equality, while the other about some function `eqb` +that the __function__ `?=` evaluates to `true`. These are fundamentally different. +One talks about mathematical equality, while the other about some function `?=` defined somewhere in Coq's standard library. Who knows - maybe there's a bug in -Coq's implementation! Fortunately, Coq comes with a proof that if two things -are equal according to `eqb`, they are mathematically equal. This proof is +Coq's implementation! Fortunately, Coq comes with a proof that if two numbers +are equal according to `?=`, they are mathematically equal. This proof is called `eqb_nat_eq`. We tell Coq to use this with `apply`. Our proof goal changes to: ``` @@ -248,9 +251,9 @@ true = (x + y =? k) ``` This is _almost_ like `Heq`, but flipped. Instead of manually flipping it and using `apply` -with `Heq`, I let Coq figure the rest of the work out using `auto`. +with `Heq`, I let Coq do the rest of the work using `auto`. -Phew! All this for the `true` case of `eqb`. Next, what happens if `x + a` does not equal `k`? +Phew! All this for the `true` case of `?=`. Next, what happens if `x + a` does not equal `k`? Here's the proof state at this time: ``` @@ -294,12 +297,12 @@ This reads, if there _is_ an element `y` in `is` that adds up to `k` with `x`, t hold, it would mean that `find_matching` would occasionally fail to find a matching number, even though it's there! We can't have that. -Finally, we want to specify what it means for `find_sum`, or solution function, to actually +Finally, we want to specify what it means for `find_sum`, our solution function, to actually work. The naive definition would be: > Given a list of integers, `find_sum` always finds a pair of numbers that add up to `k`. -Unfortunately, this is not true. What if, for instance, we have `find_sum` an empty list? +Unfortunately, this is not true. What if, for instance, we give `find_sum` an empty list? There are no numbers from that list to find and add together. Even a non-empty list may not include such a pair! We need a way to characterize valid input lists. I claim that all lists from this Advent of Code puzzle are guaranteed to have two numbers that @@ -311,11 +314,10 @@ we state this as follows: This defines a new property, `has_pair t is` (read "`is` has a pair of numbers that add to `t`"), which means: -* There are two numbers `n1` and `n2` such that, -* They are not equal to each other (`n1 <> n2`) and (`/\`), -* The number `n1` is an element of `is` (`In n1 is`) and, -* The number `n2` is an element of `is` (`In n2 is`) and, -* The two numbers add up to `t` (`n1 + n2 = t`). +> There are two numbers `n1` and `n2` such that, they are not equal to each other (`n1<>n2`) __and__ +> the number `n1` is an element of `is` (`In n1 is`) __and__ +> the number `n2` is an element of `is` (`In n2 is`) __and__ +> the two numbers add up to `t` (`n1 + n2 = t`). When making claims about the correctness of our algorithm, we will assume that this property holds. Finally, here's the theorem we want to prove: