Skip to content

Commit

Permalink
Removed the Relation to Other Work section from the Readme file follo…
Browse files Browse the repository at this point in the history
…wing feedback suggesting that it was not helpful.
  • Loading branch information
larryleeelucidsolutions committed Aug 25, 2018
1 parent d87f026 commit 98a5ff1
Showing 1 changed file with 0 additions and 19 deletions.
19 changes: 0 additions & 19 deletions Readme.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,25 +7,6 @@ Combinatorics, it asserts that if you put n things into m containers,
and n > m, then at least one of the containers contains more than
one thing.

Relation to Other Work
----------------------

The Coq Standard Library does not contain a proof of the Pigeonhole
principle. In addition, the Coq Package Index, only contains one
other proof of the Pigeonhole principle. This proof is contained in
the [CoLoR library](https://github.com/fblanqui/color/blob/bd939824c1b9b3147cc596086627cca586fbbeed/Util/List/ListOccur.v) in a module defining a predicate named `occur`.

The proof given by the CoLoR library is not a stand-alone proof
and depends on several other functions and predicates provided by
the library. Accordingly, a developer cannot use this proof without
including the entire library and familiarizing themselves with the
definitions and notations defined therein.

In contrast, in this library, we present a stand-alone proof that
relies solely on the Coq Standard Library. A developer looking for
a proof of the Pigeonhole principle can include this proof directly
without any additional complications.

Authors
-------

Expand Down

0 comments on commit 98a5ff1

Please sign in to comment.