FunProofs

Simple Coq proofs of random, interesting mathematical and data structure properties.

Proofs

BBQ: An array-based implementation of a bounded buffer queue matches a list-based implementation.
BoolComplete: Functionally complete sets of boolean operations to express all truth tables.
DerivParse: Regular expression parser using derivatives.
Div9: Divisibility rules.
FizzBuzz.v: The FizzBuzz interview question.
Graham (incomplete): Graham's number and Knuth up-arrow notation.
Hats: Optimal strategy for a red/blue hat logic problem.
OddE: All odd numbers have an 'e' in English.
Quorum: Two majority subsets have a non-empty intersection.
Sqrt2: Irrationality of sqrt 2.
TriSum.v: The triangle sum and related sums for other powers.

Name		Name	Last commit message	Last commit date
Latest commit History 47 Commits
Lib		Lib
.gitignore		.gitignore
BBQ.v		BBQ.v
BoolComplete.v		BoolComplete.v
DerivParse.v		DerivParse.v
Div9.v		Div9.v
FizzBuzz.v		FizzBuzz.v
Graham.v		Graham.v
Hats.v		Hats.v
Makefile		Makefile
OddE.v		OddE.v
Quorum.v		Quorum.v
README.md		README.md
Sqrt2.v		Sqrt2.v
TriSum.v		TriSum.v
_CoqProject		_CoqProject