andrejbauer

(** An attempt to formalize graphs. *)

Require Import Arith.

(** In order to avoid the intricacies of constructive mathematics,
    we consider finite simple graphs whose sets of vertices are
    natural numbers 0, 1, , ..., n-1 and the edges form a decidable
    relation.  *)

(** We shall work a lot with statements of the form

andrejbauer

Official Zermelo-Fraenkel set theory only has the elementhood relation symbol ∈, and nothing else. Other constants, such as ∅, ⊆, ∩, ∪, f[x], etc. can be mechanically eliminated. The result of the elimination is a formula which is logically equivalent to the original, but is more complicated.

This program eliminates constants and function symbols, and generates LaTeX showing the formula before and after the elimination.

andrejbauer

(* 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).
*)

andrejbauer

(* 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

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

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

(* 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

(* 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

/*
  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: