Возникла проблема с неспособностью использовать деструктивный татик в определении

Question

Я работаю с определением в coq, которое должно извлечь что-то из теоремы, но не может разрушить определение.

Theorem sp : forall (X : Type) (T : X -> Prop)..... , exists (a : X), T a.
Definition yield_sp : (X : Type) (T : X -> Prop) (H : sp X T .....)..... : X.

Когда я пытаюсь уничтожить H, coq предупреждает, что

Анализ случая по типу сортировки не допускается для индуктивного определения, например.

Я хотел бы знать причину этого, а также узнать, как использовать определение для получения элемента из «существующего» предложения.

Answer 1

Вы не можете извлечь свидетеля из доказательства существования.Есть несколько вариантов:

• Измените выражение доказательства на {x : T | P x}, которое ведет себя более или менее подобно экзистенциальному квантификатору, но поддерживает функцию проекции proj1_sig : {x : T | P x} -> T.

• Примите аксиому выбора, как в https://coq.inria.fr/library/Coq.Logic.ClassicalChoice.html

• Если вы определяете количество по счетному типу и , ваше предложение разрешимоВы можете использовать трюк в этом вопросе для извлечения свидетеля.