andrejbauer

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

andrejbauer

(* Content-type: application/vnd.wolfram.mathematica *)

(*** Wolfram Notebook File ***)
(* http://www.wolfram.com/nb *)

(* CreatedBy='Mathematica 11.2' *)

(*CacheID: 234*)
(* Internal cache information:
NotebookFileLineBreakTest

andrejbauer

#!/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

andrejbauer

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

andrejbauer

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

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.