Запутывающие обязательства, порожденные тактикой «Программы»

Question

Я совсем новичок в ассистенте, и все еще нахожусь в ногах.Я столкнулся со случаем, с которым я не знаю, как справиться: я пытался использовать тактику Program Fixpoint, чтобы ослабить требования к моему коду, чтобы впоследствии впоследствии доказать необходимые свойства, так называемые Obligations.В то время как большинство из них были простыми, были сформированы две обязательства, цели которых имели форму [a-quite-simplee-xpr] = [my-function-name]_obligation_3, в целом цели были связаны с другими обязательствами, которые были доказаны ранее.Я пытался развернуть и сделать замены, но это не помогло.Если нет общего решения для таких проблем, я могу выслать сценарий проверки + снимок экрана с обязательством добавить некоторый контекст.

Заранее спасибо.

Answer 1

Единственное, что может происходить, это то, что у вас есть типы, которые содержат как «данные», так и «доказательства» (обычно, если вы пытаетесь создать типы уточнения с помощью sig, или пользовательский индуктивный тип, который содержит термины проверки) и что ваши функции требуют доказательств пропозиционального равенства, которое обычно слишком сильно для таких зависимых типов.

Условия доказательства должны быть неактуальными: самый простой выход - решить эту цель, используя аксиому из ProofIrrelevance (в stdlib).

Существуют способы без аксиом, но я считаю, что они требуют гораздо больше работы / опыта.