Skip to content

Instantly share code, notes, and snippets.

View andrejbauer's full-sized avatar

Andrej Bauer andrejbauer

View GitHub Profile
@andrejbauer
andrejbauer / gist:4272538
Created December 12, 2012 23:10
A lemma which explains how transport and function extensionalty interact.
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).
@andrejbauer
andrejbauer / assoc.elf
Created June 18, 2013 09:00
Twelf seems very finicky about certain details. Here I explore how associative lists depend in unreasonable ways on the complexity of the value type.
% 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
andrejbauer / mandelbrot.c
Created December 11, 2013 22:23
A simple program for computing the Mandelbrot set.
/*
This program is an adaptation of the Mandelbrot program
from the Programming Rosetta Stone, see
http://rosettacode.org/wiki/Mandelbrot_set
Compile the program with:
gcc -o mandelbrot -O4 mandelbrot.c
Usage:
@andrejbauer
andrejbauer / mandelbrot.ml
Created December 28, 2013 22:48
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
andrejbauer / topology.v
Last active November 28, 2023 19:40
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.
(* 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
andrejbauer / Bijection.md
Last active November 29, 2023 22:05
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)

Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@andrejbauer
andrejbauer / README.md
Last active February 24, 2022 14:40
How to formulate and prove the statement "all functions are continuous" in an effectful functional language?

Are all functions continuous?

Mathematical background

Brouwer's statement "all functions are continuous" can be formulated without reference to topology as follows.

Definition: A functional f : (N → N) → N is continuous at a : N → N when there exists m : N such that, for all b : N → N, if ∀ k < m, a k = b k then f a = f b.

@andrejbauer
andrejbauer / example.m31
Last active February 19, 2024 09:02
Example of Andromeda ML-programming
(* In Andromeda everything the user writes is "meta-level programming. *)
(* ML-level natural numbers *)
mltype rec mlnat =
| zero
| succ of mlnat
end
(* We can use the meta-level numbers to define a program which computes n-fold iterations
of f. Here we give an explicit type of iterate because the ML-type inference cannot tell
@andrejbauer
andrejbauer / algebra.v
Last active March 12, 2021 06:34
Uinversal algebra in Coq
(* An initial attempt at universal algebra in Coq.
Author: Andrej Bauer <Andrej.Bauer@andrej.com>
If someone knows of a less painful way of doing this, please let me know.
We would like to define the notion of an algebra with given operations satisfying given
equations. For example, a group has of three operations (unit, multiplication, inverse)
and five equations (associativity, unit left, unit right, inverse left, inverse right).
*)