CODEWITHSUNDEEP
coq
Adam
Adam

Reputation: 1354

Nonconstructive proofs in Coq?

Can one prove an existence theorem in a nonconstructive way in Coq? Specifically I am thinking about the proof that there are irrational numbers s.t. x^y is rational.

Upvotes: 2

Views: 306

Answers (1)

ejgallego
ejgallego

Reputation: 6852

For that particular proof you will need to assume the excluded middle axiom. You can either import it from the library:

Require Import Coq.Logic.Classical_Prop.
About classic.

or add it yourself in some specific form (more advanced use as it requires some care). Nevertheless, the real numbers in the standard library are already classical so you can derive this principle from them.

Upvotes: 6

Related Questions