What abilities does coq have apart from simple proofs? Can it complete induction? Can I use it to solve polynomial equations? Can I use it to prove bijections?
2
-
1$\begingroup$ Yes, and a lot more. Many Coq users are addicted to using Coq. Happy learning! $\endgroup$– Not An ITP ExpertFeb 16 at 1:27
-
$\begingroup$ From a proof theoretic point of view, you can prove with Coq anything that you have ever learned about math, if you put in enough effort. $\endgroup$– Trebor ♦Feb 16 at 11:34
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
Coq (and most other proof assistants) can be used to formalize most any mathematical proof. For the most part you have to write the proof yourself and Coq checks it, working with the user interactively. There is some automation as well to make it easier.
You can certainly use Coq to write a proof that a particular set of numbers are solutions to a particular polynomial. While Coq is not a computer algebra system and not used as such, if you use a CAS separately to find the roots, Coq has good support for “proofs by calculation” and it is likely you could easily write the proof. There might even be some automation or some ability to integrate with other tools like SMT solvers or computer algebra systems to find the roots for you and put them in your proof. Coq has been around for a while and there are a lot of tools.
