Skip to content

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

License

Notifications You must be signed in to change notification settings

langston-barrett/coq-big-o

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

25 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Big O Notation for Coq

Build Status Documentation

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.

About

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published