I implemented the following Coq program following example code from this online book.
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Example test_next_weekday:
(next_weekday (next_weekday saturday)) =
tuesday.
I attempt to compile this file error.v by running $ coqc error.v, and get a There are pending proofs error.
$ coqc error.v
Error: There are pending proofs
make: *** [makefile:7: make] Error 1
Why am I getting this error?
It's unfortunate that Coq does not have a complete list of errors in the reference manual; I've reported an issue for this on GitHub.
The error message Error: There are pending proofs means "there are theorems that you have stated but not completed the proofs of. Newer versions of Coq (perhaps only the development versions at this point) should name the pending theorems (see this PR on GitHub).
The solution is to either give a proof of test_next_weekday (as suggested in the comments), to close the proof with Admitted., or to abort the proof with Abort..