Неконструктивные доказательства в Coq?

Question

Можно ли доказать теорему существования неконструктивным образом в Coq? В частности, я думаю о доказательстве того, что существуют иррациональные числа s.t. x^y рационально.

Answer 1

Для этого конкретного доказательства вам нужно будет принять исключенную среднюю аксиому. Вы можете импортировать его из библиотеки:

Require Import Coq.Logic.Classical_Prop. 
About classic. 

или добавить себя в какой-то конкретной форме (более продвинутое использование, как это требует некоторой осторожности). Тем не менее, реальные цифры в стандартной библиотеке уже классические, поэтому вы можете извлечь из них этот принцип.