Re-implementing the XMonad window manager core in Coq: PDF

Regarding the question of totality on slide 40, a naïve analysis would say that the deconstruction "let (y : ys) =" could fail (if the list returned from reverse were empty), and thus the function would not be total. Of course this is not the case, since reversing a non-empty list returns a non-empty list, but this requires that reverse be dependently typed.

(Slightly off-topic: the Mercury logic programming language supports just the right amount of dependency to allow this specification of reverse, and would deduce totality for this function.)

Back on topic, yes, most practical functions can be rewritten to be structurally recursive. The most brain-dead easy way is add a "time-to-live" argument to the recursive function. This argument is a Peano number initially set to a value higher than the expected number of recurrences. (In the example from the slides, one could choose the total number of windows on the screen.) The function is then modified to decrement the time-to-live argument on each recurrence, and to return a dummy value should the time-to-live reach zero. It's then trivial to prove that the function terminates, and usually easy to prove that it does what it's supposed to do before the time-to-live zeros out.