

@ 735,6 +735,139 @@ A program can always take a step, and each time it does, 



the set of valid program counters decreases in size. Eventually, 



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? 



running no matter what. 







This seems like a task for induction, in this case on the size 



of the valid set. In particular, strong mathematical induction 



{{< sidenote "right" "stronginductionnote" "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/howtodoinductiononthelengthofalistincoq), 



so I'll just use it. The Coq theorem corresonding to strong induction 



on the length of a list is as follows: 







{{< codelines "Coq" "aoc2020/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" "aoc2020/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" "aoc2020/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" "aoc2020/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" "aoc2020/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" "aoc2020/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" "aoc2020/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 >}} 


