This question gets at the heart of computation, logic and provability. Coq is based on a logic system called the "Calculus of constructions" https://en.wikiped

This question gets at the heart of computation, logic and provability. Coq is based on a logic system called the "Calculus of constructions" https://en.wikipedia.org/wiki/Calculus_of_constructions https://en.wikipedia.org/wiki/Calculus_of_constructions. As such it has the same limitations as that logical system. Most notably, Gödel's incompleteness theorems place a limit on what's provable in Coq, or indeed many other systems. There are various kinds of logic systems, each with different kinds of 'power'. Power is a double-edge sword in logic systems, as with power comes the capacity to introduce paradoxes and inconsistencies. As with programming languages, certain logic systems and automated logics are suited for particular cases. For example, there is a system 'MetiTarski' like a Domain Specific Language, designed to prove theorems about real-valued special functions.(https://www.cl.cam.ac.uk/~lp15/papers/Arith/ https://www.cl.cam.ac.uk/~lp15/papers/Arith/).