pascal_cuoq said: "There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of com

pascal_cuoq said: "There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of computer-assisted proofs." For predicates that can be computed in coq, we can do away with the names: Fixpoint even n := match n with | 0 => True | 1 => False | S (S m) => even m end. Note that "True" and "False" are propositions (have sort "Prop") with trivial and no proofs, respectively, and are not "true" and "false", which are the constructors of the inductive type "bool". If the return type were changed to bool, "even n = true" (rather than just "even n") would be a predicate meaning "n is an even natural number". Additionally, your wish is already coming true! For certain types of problems, coq can be hooked up to external solvers (for SAT, for instance) which generate proof terms that are then checked by coq. See http://www.lri.fr/~melquion/doc/09-calculemus-article.pdf http://www.lri.fr/~melquion/doc/09-calculemus-article.pdf for an example.