Using Qucs for filter design

Posted on 2011/02/15 by Thomas Strathmann

Qucs, short for Quite Universal Circuit Simulator, is as the name suggests a simulation package for electronic circuits. It’s free and sports a nice graphical schematic capture interface. One of its many nice and useful features is the ability to write equations so you can calculate all kinds of stuff from simple linear equations up to Fourier transforms as part of the simulation. In this post I present a simple Qucs schematic for designing Sallen-Key Butterworth filters. It comes in three varieties: lowpass, highpass, and bandpass. Continue reading →

Posted in Electronics, Tools | Tagged , | 3 Comments

WordPress blogging in LaTeX

Posted on 2011/02/11 by Thomas Strathmann

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.

Posted in Tools | Tagged , | Leave a comment

Beginning Ltac

Posted on 2011/02/10 by Thomas Strathmann

One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language \mathcal{L}_{tac}. 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 \wedge, \vee, \forall, \Rightarrow subset of first order predicate logic automatically. Continue reading →

Posted in Coq | Tagged | Leave a comment

How to draw commutative diagrams in LaTeX with TikZ

Posted on 2011/02/02 by Thomas Strathmann

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 →

Posted in Mathematics, Tools | Tagged , , , | 24 Comments

Another script font for LaTeX

Posted on 2011/01/29 by Thomas Strathmann

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: \mathscr{A}, \mathscr{B}, \mathscr{C}, \mathscr{D}, \mathscr{E}, \mathscr{F}, \mathscr{G}, \dots

Posted in Tools | Tagged , , | Leave a comment

Category Theory Video Lectures

Posted on 2011/01/27 by Thomas Strathmann

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.

Posted in Mathematics | Tagged | 1 Comment

Doepfer MCV4 MIDI to CV interface editor in Max

Posted on 2011/01/25 by Thomas Strathmann

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!

MCV4 editor screenshot

Download Max patch (make sure, the files extension is maxpat and your browser does not add .txt to the file name!)

Posted in Music Software | Tagged , , , | Leave a comment

How I use git Part 2: Emacs integration

Posted on 2011/01/25 by Thomas Strathmann

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.

Posted in Tools | Tagged , | 1 Comment

The Maybe monad in Coq

Posted on 2011/01/25 by Thomas Strathmann

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 →

Posted in Coq, Haskell | Tagged | 8 Comments

Coq Syntax Highlighting Test

Posted on 2011/01/24 by Thomas Strathmann

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.
Posted in Coq, Tools | Tagged , , | Leave a comment