Thursday, 14 April 2011

A Theorem-Proving Exercise for Novices

Listening to:

Louis Armstrong, Ain’t Misbehavin’.


I have used this exercise as a good one for getting a student up to speed with a proof-assistant such as HOL4.

Using your theorem-proving system of choice, define the notion of sublist, a binary relation on lists l1 and l2, which is true if and only if all the elements of l1 appear in l2 in the same order. Naturally, l2 may contain other elements.

For example, [1,2,3] is a sub-list of [0,1,2,2,4,5,6,3,10], but is not a sub-list of [1,4,3,2].

Having defined this relation in whatever way seems most natural, prove that it is reflexive, anti-symmetric and transitive.

Thursday, 28 April 2011

Emacs and its fonts

Listening to:

Schutz, Sinfonia Sacrae, op. 6, no. 8: Adjuro vos Filiae Jerusalem

Emacs has terrible font handling: there seem to be about three different APIs, and the documentation doesn’t seem to be as clear as it might about which to use. Then there is the additional confusion to do with fonts on X. There are old style fonts that are specified like


and then there are GTK font specifications like

  Deja Vu Sans Mono 

sometimes with additional -12 type suffixes.

It’s all terribly confusing. I recently found myself unable to set my font to one that was narrow enough to allow two Emacs windows across one 1280 pixel wide monitor. I posted to Stack Overflow about it, but nobody has come to my aid just yet.

In the meantime, I have adopted a 9pt Lucida Typewriter Sans that looks OK. This does produce a pretty narrow Emacs window, and when I switch to xmonad, I’ll be able to have two such windows tiling nicely beside each other.