{{ message }}

Instantly share code, notes, and snippets.

# Andrej Bauer andrejbauer

Created Feb 5, 2021
The finite truth values are precisely the decidable truth values.
View finite.v
 (** Prop is a complete lattice. We can ask which propositions are finite. *) Definition directed (D : Prop -> Prop) := (exists p , D p) /\ forall p q, D p -> D q -> exists r, D r /\ (p -> r) /\ (q -> r). (** A proposition p is finite when it has the following property: for any directed D, if p ≤ sup D then there is q ∈ D such that p ≤ q. *) Definition finite (p : Prop) := forall D, directed D -> (p -> exists q, D q /\ q) -> exists q, D q /\ (p -> q).
Created Jan 4, 2021
The initial algebra for the functor X ↦ (X → ∅) → ∅ is ∅.
View doubleNegationInitialAlgebra.agda
 -- empty type data 𝟘 : Set where absurd : {A : Set} → 𝟘 → A absurd () -- booleans data 𝟚 : Set where false true : 𝟚
Created Nov 15, 2020
The proof that excluded middle follows if all subsets of a singleton set are finite.
View finite_subsets_and_LEM.v
 (* If all subsets of a singleton set are finite, then excluded middle holds.*) Require Import List. (* We present the subsets of X as characteristic maps S : X -> Prop. Thus to say that x : X is an element of S : Powerset X we write S x. *) Definition Powerset X := X -> Prop. (* Auxiliary relation "l lists the elements of S". *) Definition lists {X} (l : list X) (S : Powerset X) := forall x, S x <-> In x l.
Last active Feb 28, 2021
Formalization of the fact that a dependent type theory with excluded middle cannot have a universe Set such that Set → Set injects into Set.
View UniverseInjection.agda
 -- Counterexample by Chung Kil Hur, improved by Andrej Bauer -- We show that it is inconsistent to have an injection I : (Set → Set) → Set and excluded middle. -- Indeed, excluded middle and I together give a surjection J : Set → (Set → Set), -- which by Lawvere's fixed point theorem begets a fixed point operator on Set. -- However, negation does not have a fixed point. module cantor where -- generalities
Last active Jan 15, 2020
Unions of algebraic sets are algebraic
View algebraic.v
 (* A Coq formalization of the theorem that the the union of algebraic sets are algebraic. The file is self-contained, so we start with some general definitions and facts from logic and sets, and basic algebraic definitions. It should be straight-forward to translate it to any setting that has a decent library of basic facts of logic, set theory and algebra. *) (* We formalize the following "paper" proof.
Last active Sep 25, 2020
Generation of constructible numbers in Mathematica
View ConstructibleNumbers.nb
 (* Content-type: application/vnd.wolfram.mathematica *) (*** Wolfram Notebook File ***) (* http://www.wolfram.com/nb *) (* CreatedBy='Mathematica 11.2' *) (*CacheID: 234*) (* Internal cache information: NotebookFileLineBreakTest
Created Aug 14, 2019
Pictures of algebraic numbers
View algebraic.py
 #!/usr/local/bin/python3 # Compute algebraic numbers in the complex plane and draw a nice picture import numpy import sys import argparse import math import cairo import pickle
Last active May 2, 2018
Experiments in using multicore OCaml effects to simulate dynamically created local effects.
View localization.ml
 (** * General support for creation of dynamic effects *) (** We show how to use the multicore Ocaml effects to dynamically generate local effects. Such effects are akin to the Eff resources, and they can be used to implement ML references. The code is based on "Eff directly in OCaml" by Oleg Kiselyov and KC Sivaramakrishnan (http://kcsrk.info/papers/caml-eff17.pdf). It was written by Andrej Bauer, Oleg Kiselyov, and Stephen Dolan at the Dagstuhl seminar "Algebraic Effect Handlers go Mainstream". *)
Created Apr 19, 2018
Use of effects and handlers to compute the tree representation of a functional.
View functional2tree.eff
 (** This code is compatible with Eff 5.0, see http://www.eff-lang.org *) (** We show that with algebraic effects and handlers a total functional [(int -> bool) -> bool] has a tree representation. *) (* A tree representation of a functional. *) type tree = | Answer of bool | Question of int * tree * tree
Last active Apr 7, 2021
Graph theory in Coq
View Graph.v
 (** 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