Big O Notation for Coq
A flexible yet easy-to-use formalization of Big O, Big Theta, and more Bachmann-Landau notations based on seminormed vector spaces.
Table of Contents
Table of Contents
Features
Definitions
- Bachmann-Landau notations
- Big O
- Big Ω
- Big Θ
- little o
- little ω
- (Optional) Unicode notation:
f ∈ ω(g) → g ∈ Ω(f) - Alternate definitions and proofs of their equivalence
Theorems & Lemmas
This is not an exhaustive list:
- Big Θ as an equivalence relation on functions
- Big O as a partial ordering on functions
- Big Ω as a partial ordering on functions
- Duality of Big O and Big Ω: f ∈ O(g)
↔ g ∈ Ω(f) - f ∈ o(g) → f ∈ O(g)
- f ∈ ω(g) → f ∈ Ω(g)
- Various facts about the compositions of functions
- Indifference of these notations to multiplication by constants
- If you have ideas for useful lemmas, please open an issue!
API Documentation
You can view the documentation online or build it locally:
./configure && make html && firefox html/toc.html
to build the API documentation with coqdoc.
Installation
You can build this package using the Nix package manager:
nix-build . && ls result/lib/coq/8.5/user-contrib/BigO/
Alternatively, you can use the the standard
./configure && make
If you're using Nix, you can easily intergrate this library with your own
package's default.nix or shell.nix, and Coq should automatically find it.
{
stdenv,
coq,
pkgs ? import <nixpkgs> { }
}:
let
coq_big_o = with pkgs; callPackage (fetchFromGitHub {
owner = "siddharthist";
repo = "coq-big-o";
rev = "some commit hash"; # customize this
sha256 = "appropriate sha256 checksum"; # and this
}) { };
in stdenv.mkDerivation {
name = "my-coq-project";
src = ./.;
buildInputs = [ coq coq_big_o ];
...
}Otherwise, just copy what you built to somewhere that Coq will find it.
Related Work
I don't know of any. If anyone else is interested in formal complexity theory, let me know!
This project leans heavily on the math-classes library for definitions of algebraic structures, specifically seminormed vector spaces.
Contributing
Pull requests for fixes, new results, or anything else are welcome! Just run
nix-shell
to be dropped into a shell with all dependencies installed.