Just found an interesting resource about blogging in LaTeX using WordPress. Eric Finster at Curious Reasoning has put together a Python script that allows you to prepare blog posts in LaTeX and convert them to the proper format. Might come in handy for a few posts I have planned.
One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language 
. Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, we can simply write down new tactics as part of a proof development. In this post I will develop a small tactic that solves propositions of the 
subset of first order predicate logic automatically. Continue reading
Sooner or later everyone who uses LaTeX to typeset documents containing maths will encounter the problem of how to draw commutative diagrams. There are many packages, some general purpose other specialized for the task. An excellent survey of some of these alternatives by James Milne can be found here.
I use TikZ for most drawings I use in documents, so naturally I also want to use TikZ to draw commutative diagrams. The survey by Milne includes a description of how to use the matrix librariy in TikZ to typeset commutative diagrams and Felix Lenders has a short PDF document with much the same contents. I, on the other hand, do not use the matrix library and that’s the reason for writing this blog post.
Continue reading
Sometimes it’s nice to have an extra script font available to make distinctions between different kinds of objects clearer. One such font is Ralph Smith’s Formal Script (see here for the TeX Catalogue entry) which is provided by the mathrsfs package.
This gives you a new LaTeX font command \mathscr{} for use in math mode. My version of AUCTeX for Emacs did not include a font key command for this, so I added one (bound to the standard font command prefix — which for me is C-c C-f — plus C-x).
(add-hook 'LaTeX-mode-hook (lambda () (add-to-list 'LaTeX-font-list '(?\C-x "" "" "\\mathscr{" "}")))) |
And this is how it looks: 
Edsko de Vries of Trinity College Dublin has created a very useful overview of the series of lectures on category theory by Eugenia Cheng and Simon Willerton that has been available on Youtube for quite some time. So, if for example you wanted to know more about limits you could just look it up and jump right to the relevant videos. The overview is also available as a mind map.
A little Max patch for changing the parameters of a Doepfer MCV4 MIDI to CV interface I made a while ago. It’s not extensively tested, but seems to work so far. The user interface is in German, but I guess everything is pretty self-explanatory and obvious even if you don’t know any German at all. If you find bugs or make changes, I’d like to hear about it. Have fun!
Download Max patch (make sure, the files extension is maxpat and your browser does not add .txt to the file name!)
The strangest things happen. Once I was a GNU/Linux user who spent most of the time staring at a framebuffer console and used vim exclusively. Today I use Mac OS X and Aquamacs most of the time (although I still use vim for many tasks) because editing LaTeX and Coq (with the fantastic ProofGeneral mode) is so much nicer using Emacs. Like every serious Emacs user I hate to leave the editor for tasks like file management or revision control. With egg managing projects under git revision control is a breeze. This blog post by the author of egg has a partial introduction so I’ll just summarize my daily usage of egg.
When I have just edited a single file, I’ll hit C-x v i and the enter key. This stages the current buffer’s modifications. To commit the staged changes, use C-x v w, review the staged changes and edit the commit messages in the buffer that pops up, and finish off with C-c C-c.
If I have edited multiple files and I don’t want to commit all files in one go, I conjure up the status of the git repository using the incantation C-x v s. This will show basically what git-status would show you. The display is usually very crowded because for each modification to a file tracked by git it shows a diff. To hide this, navigate to the section you want to unclutter, e.g. Unstaged Changes:, and hit H. Now, to stange or unstage a file, position the cursor on its name, and hit s. To ge to the commit screen, just use c. That’s all I normally do with egg.
The Maybe monad is pretty useful whenever you’re dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.
Continue reading
A test case for Coq syntax highlighting in GeSHi (for the WP-Syntax plugin).
Inductive nat : Set := | O : nat | S : nat -> nat. Inductive fin : nat -> Type := | FO : forall n, fin (S n) | FS : forall n, fin n -> fin (S n). Implicit Arguments FO [n]. Implicit Arguments FS [n]. Fixpoint fin2nat {n : nat} (k : fin n) : nat := match k with | FO _ => 0 | FS _ k' => S (fin2nat k') end. Example f0 : fin 3 := FO. Example f1 : fin 3 := FS FO. Example f2 : fin 3 := FS (FS FO). Eval compute in fin2nat f2. |
In languages like Coq where all computations must terminate and only total functions are allowed it would still be nice to be able to express non-terminating computations. While searching for solutions other people had come up with I stumbled across this little Coq development: SK Combinator Calculus Interpreter.
The main insight is that you can view partiality as a computational effect that can be hidden inside a monad. I think it’s a clever and intriguing idea.
