Add more text to draft.

code/aoc-2020

@@ -1 +1 @@
-Subproject commit 2b69cbd391398ed21ccf3b2b06d62dc46207fe85
+Subproject commit 7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82

content/blog/01_aoc_coq.md

@@ -737,4 +737,137 @@ this set will become empty, so if nothing else, our program will
 eventually terminate in an "error" state. Thus, it will stop
 running no matter what. 
 
-The problem is: how do we express that?
+This seems like a task for induction, in this case on the size
+of the valid set. In particular, strong mathematical induction
+{{< sidenote "right" "strong-induction-note" "seem to work best." >}}
+Why strong induction? If we remove a single element from a set,
+its size should decrease strictly by 1. Thus, why would we need
+to care about sets of <em>all</em> sizes less than the current
+set's size?<br>
+<br>
+Unfortunately, we're not working with purely mathematical sets.
+Coq's default facility for sets is simply a layer on top
+of good old lists, and makes no effort to be "correct by construction".
+It is thus perfectly possible to have a "set" which inlcudes an element
+twice. Depending on the implementation of <code>set_remove</code>,
+we may end up removing the repeated element multiple times, thereby
+shrinking the length of our list by more than 1. I'd rather
+not worry about implementation details like that.
+{{< /sidenote >}}
+Someone on StackOverflow [implemented this](https://stackoverflow.com/questions/45872719/how-to-do-induction-on-the-length-of-a-list-in-coq),
+so I'll just use it. The Coq theorem corresonding to strong induction
+on the length of a list is as follows:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 205 207 >}}
+
+It reads,
+
+> If for some list `l`, the property `P` holding for all lists
+shorter than `l` means that it also holds for `l` itself, then
+`P` holds for all lists.
+
+This is perhaps not particularly elucidating. We can alternatively
+think of this as trying to prove some property for all lists `l`.
+We start with all empty lists. Here, we have nothing else to rely
+on; there are no lists shorter than the empty list, and our property
+must hold for all empty lists. Then, we move on to proving
+the property for all lists of length 1, already knowing that it holds
+for all empty lists. Once we're done there, we move on to proving
+that `P` holds for all lists of length 2, now knowing that it holds
+for all empty lists _and_ all lists of length 1. We continue
+doing this, eventually covering lists of any length.
+
+Before proving termination, there's one last thing we have to
+take care off. Coq's standard library does not come with
+a proof that removing an element from a set makes it smaller;
+we have to provide it ourselves. Here's the claim encoded
+in Coq:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 217 219 >}}
+
+This reads, "if a set `s` contains a finite natural
+number `f`, removing `f` from `s` reduces the set's size".
+The details of the proof are not particularly interesting,
+and I hope that you understand intuitively why this is true.
+Finally, we make our termination claim.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 230 231 >}}
+
+It's quite a strong claim - given _any_ program counter,
+set of valid addresses, and accumulator, a valid input program
+will terminate. Let's take a look at the proof.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 232 234 >}}
+
+We use `intros` again. However, it brings in variables
+in order, and we really only care about the _second_ variable.
+We thus `intros` the first two, and then "put back" the first
+one using `generalize dependent`. Then, we proceed by
+induction on length, as seen above.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 235 236>}}
+
+Now we're in the "inductive step". Our inductive hypothesis
+is that any set of valid addresses smaller than the current one will
+guarantee that the program will terminate. We must show
+that using our set, too, will guarantee termination. We already
+know that a valid input, given a state, can have one of three
+possible outcomes: "ok" termination, "failed" termination,
+or a "step". We use `destruct` to take a look at each of these
+in turn. The first two cases ("ok" termination and "failed" termination)
+are fairly trivial:
+
+{{< codelines "Coq" "aoc-2020/day8.v" 237 240 >}}
+
+We basically connect the dots between the premises (in a form like `done`)
+and the corresponding inference rule (`run_noswap_done`). The more
+interesting case is when we can take a step.
+
+{{< codelines "Coq" "aoc-2020/day8.v" 241 253 >}}
+
+Since we know we can take a step, we know that we'll be removing
+the current program counter from the set of valid addresses. This
+set must currently contain the present program counter (since otherwise
+we'd have "failed"), and thus will shrink when we remove it. This,
+in turn, lets us use the inductive hypothesis: it tells us that no matter the
+program counter or accumulator, if we start with this new "shrunk"
+set, we will terminate in some state. Coq's constructive
+nature helps us here: it doesn't just tells us that there is some state
+in which we terminate - it gives us that state! We use `edestruct` to get
+a handle on this final state, which Coq automatically names `x`. At this
+time Coq still isn't convinced that our new set is smaller, so we invoke
+our earlier `set_remove_length` theorem to placate it.
+
+We now have all the pieces: we know that we can take a step, removing
+the current program counter from our current set. We also know that
+with that newly shrunken set, we'll terminate in some final state `x`.
+Thus, all that's left to say is to apply our "step" rule. It asks
+us for three things:
+
+1. That the current program counter is in the set. We've long since
+established this, and `auto` takes care of that.
+2. That a step is possible. We've already established this, too,
+since we're in the "can take a step" case. We apply `Hst`,
+the hypothesis that confirms that we can, indeed, step.
+3. That we terminate after this. The `x` we got
+from our induction hypothesis came with a proof that
+running with the "next" program counter and accumulator
+will result in termination. We apply this proof, automatically
+named `H0` by Coq.
+
+And that's it! We've proved that a program terminates no matter what.
+This has also (almost!) given us a solution to part 1. Consider the case
+in which we start with program counter 0, accumulator 0, and the "full"
+set of allowed program counters. Since our proof works for _all_ configurations,
+it will also work for this one. Furthermore, since Coq proofs are constructive,
+this proof will __return to us the final program counter and accumulator!__
+This is precisely what we'd need to solve part 1.
+
+But wait, almost? What's missing? We're missing a few implementation details:
+* We've not provided a concrete impelmentation of integers.
+* We assumed (reasonably, I would say) that it's possible to convert a natural
+number to an integer.
+* We also assumed (still reasonably) that we can try convert an integer
+back to a finite natural number, failing if it's too small or too large.
+
+{{< todo >}}Finish up{{< /todo >}}