Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Finish up the Coq Advent of Code post.

Browse Source
This commit is contained in:
Danila Fedorin 2020-12-02 18:45:28 -08:00
parent 234b795157
commit 8f0f2eb35e
1 changed files with 37 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

72
content/blog/00_aoc_coq.md
View File

@ -1,8 +1,7 @@
--- ---
title: "Advent of Code in Coq - Day 1" 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"] tags: ["Advent of Code", "Coq"]
draft: true
--- ---
The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite 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! With this in mind, we can move on to writing some Coq!
### Defining the Functions ### Defining the Functions
The first step to proving our code correct is to actually write the code! As a first The first step to proving our code correct is to actually write the code! To start with,
step, let's write a helper function that, given a number `x`, tries to find another number 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: `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 >}} {{< 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 Here, `is` is the list of numbers that we want to search.
we want to add up to (`2020` in our particular case), and `x` is the same as it was in We proceed by case analysis: if the list is empty, we can't
the previous paragraph. 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`). 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 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 up to `total`, and return `Some y` (equivalent to `Just y` in Haskell) if it does.
into the rest of the list. 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 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, 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. In our case, this means `find_matching` searching an empty list.
* The __inductive case__. Assuming that a property holds for any list * The __inductive case__. Assuming that a property holds for any list
`[b, c, ...]`, we want to show that the property also holds for `[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. 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 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]`. 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, 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 not yet introduced the variables `k`, `x`, and `y`, they remain
inside a `forall` quantifier at that time. To be able to refer 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 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? 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 We ask Coq this question using `inversion Hev`. Effectively, the question
the question: what are the possible ways we could have acquired `Hev`? 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 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 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! 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 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 >}} {{< 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, 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 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`. `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` `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 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)`. `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` 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 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, of whether `a` adds up to `k` or not, we're good to go! To do this,
we perform case analysis using `destruct`. we perform case analysis using `destruct`.
Our particular use of `destruct` says: check any possible value for `Nat.eqb (x+a) k`, 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. `Nat.eqb` returns a boolean 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`, 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: 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 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 `Hev` has been considerably simplified: now that we know the condition
of the `if` expression, we can just replace it with the `then` branch. 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 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 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 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`, 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 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. that the __function__ `?=` evaluates to `true`. These are fundamentally different.
One talks about mathematical equality, while the other about some function `eqb` 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 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 Coq's implementation! Fortunately, Coq comes with a proof that if two numbers
are equal according to `eqb`, they are mathematically equal. This proof is 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: 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` 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: 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 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. 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: work. The naive definition would be:
> Given a list of integers, `find_sum` always finds a pair of numbers that add up to `k`. > 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 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 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 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`"), This defines a new property, `has_pair t is` (read "`is` has a pair of numbers that add to `t`"),
which means: which means:
* There are two numbers `n1` and `n2` such that, > There are two numbers `n1` and `n2` such that, they are not equal to each other (`n1<>n2`) __and__
* They are not equal to each other (`n1 <> n2`) and (`/\`), > the number `n1` is an element of `is` (`In n1 is`) __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 number `n2` is an element of `is` (`In n2 is`) and, > the two numbers add up to `t` (`n1 + n2 = t`).
* The two numbers add up to `t` (`n1 + n2 = t`).
When making claims about the correctness of our algorithm, we will assume that this 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: property holds. Finally, here's the theorem we want to prove: