Возникла проблема с невозможностью использовать destruct tatic в определении

Я работаю с определением в 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 предупреждает, что

Case analysis on sort Type is not allowed for inductive definition ex.

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

Я предполагаю, что двоеточие отсутствует после Theorem sp?

Bubbler 22.05.2019 13:40

да, я напортачил с определением

shrubbroom 23.05.2019 14:55
3 метода стилизации элементов HTML
3 метода стилизации элементов HTML
Когда дело доходит до применения какого-либо стиля к нашему HTML, существует три подхода: встроенный, внутренний и внешний. Предпочтительным обычно...
Формы c голосовым вводом в React с помощью Speechly
Формы c голосовым вводом в React с помощью Speechly
Пытались ли вы когда-нибудь заполнить веб-форму в области электронной коммерции, которая требует много кликов и выбора? Вас попросят заполнить дату,...
Стилизация и валидация html-формы без использования JavaScript (только HTML/CSS)
Стилизация и валидация html-формы без использования JavaScript (только HTML/CSS)
Будучи разработчиком веб-приложений, легко впасть в заблуждение, считая, что приложение без JavaScript не имеет права на жизнь. Нам становится удобно...
Flatpickr: простой модуль календаря для вашего приложения на React
Flatpickr: простой модуль календаря для вашего приложения на React
Если вы ищете пакет для быстрой интеграции календаря с выбором даты в ваше приложения, то библиотека Flatpickr отлично справится с этой задачей....
В чем разница между Promise и Observable?
В чем разница между Promise и Observable?
Разберитесь в этом вопросе, и вы значительно повысите уровень своей компетенции.
Что такое cURL в PHP? Встроенные функции и пример GET запроса
Что такое cURL в PHP? Встроенные функции и пример GET запроса
Клиент для URL-адресов, cURL, позволяет взаимодействовать с множеством различных серверов по множеству различных протоколов с синтаксисом URL.
2
2
225
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

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

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

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

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

Является ли это синтаксисом coq, который не позволяет получить что-то просто из оператора exists? Я думаю, что для этого нужно объявить, что существует проекционная функция, которая точно может вычислить, поскольку стрелка означает вычислимое отношение в coq.

shrubbroom 24.05.2019 10:12

Другие вопросы по теме