Skip to content

Instantly share code, notes, and snippets.


Andrej Bauer andrejbauer

View GitHub Profile
View beamer-slides-with-notes.pdf
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
andrejbauer /
Last active Jan 15, 2020
A bijection between numbers and pairs of numbers.

A bijection between numbers and pairs of numbers

Every once in a while I am faced with someone who denies that the rational numbers (or fractions, or pairs of integers) can be put into a bijective correspondence with natural numbers. To deal with the situation, I coded up the bijection. So now I can just say: "Really? Interesting. Please provide a pair of numbers (i,j) which is not enumerated by f, as defined in my gist." I am still waiting for a valid counter-example.

Anyhow, here is a demo of f and g at work. I am using the Python version, but a Haskell variant is included as well.

The 100-th pair is:

>>> f(100)
(10, 4)
andrejbauer / topology.v
Last active Oct 22, 2019
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
View topology.v
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
(* We think of subsets as propositional functions.
Thus, if [A] is a type [x : A] and [U] is a subset of [A],
[U x] means "[x] is an element of [U]".
Definition P (A : Type) := A -> Prop.
andrejbauer /
Created Dec 28, 2013
A simple program to compute the Mandelbrot set.
(* The Mandelbrot set.
Compile with:
ocamlbuild mandelbrot.native
Example usage:
./mandelbrot.native --xmin 0.27085 --xmax 0.27100 --ymin 0.004640 --ymax 0.004810 --xres 1000 --maxiter 1024 --file pic.ppm
andrejbauer / mandelbrot.c
Created Dec 11, 2013
A simple program for computing the Mandelbrot set.
View mandelbrot.c
This program is an adaptation of the Mandelbrot program
from the Programming Rosetta Stone, see
Compile the program with:
gcc -o mandelbrot -O4 mandelbrot.c
andrejbauer / assoc.elf
Created Jun 18, 2013
Twelf seems very finicky about certain details. Here I explore how associative lists depend in unreasonable ways on the complexity of the value type.
View assoc.elf
% Testing how lookup in an associative list works.
% We consider associative lists with keys of type key and values
% of type value.
% Ideally, we want key to be any type with decidable
% equality and value to be any type. However, we use natural numbers
% as keys so that we can convince Twelf that key has decidable equality.
% Is there a way to tell Twelf "assume key has decidable equality"?
andrejbauer / gist:4272538
Created Dec 12, 2012
A lemma which explains how transport and function extensionalty interact.
View gist:4272538
Variable A : Type.
Variable P : A -> Type.
Variable Q : forall x, P x -> Type.
Lemma transport_funext (f g : forall x, P x) (n : forall x, Q x (f x)) (E : forall x, f x = g x) (x : A) :
(transport (fun h => forall x, Q x (h x)) (funext E) n) x = transport (Q x) (E x) (n x).
You can’t perform that action at this time.