Рассмотрим предикат, который моделирует отношение оценки. Отношение прекратится со значением true или false, поэтому я хочу, чтобы значения моих цепочек были либо конфигурацией, либо логическим значением:
Inductive compile_step :
conf_type + bool -> conf_type + bool -> Prop
Я знаю, что оценка завершается, и я хочу доказать это формально , Поэтому я определяю завершающий предикат:
Inductive terminating {A} (r: A -> A -> Prop) (c': A) :=
| TStep : (forall c1, r c' c1 -> terminating r c1) ->
terminating r c'.
И пытаюсь доказать это:
Lemma compiling_terminates (c': A):
terminating compile_step c'.
Теперь, каково мое удивление, что Coq сходит с ума. Здесь разумнее всего применить TStep и решить эту задачу:
(H) c '⟹ c1 означает завершение compile_step c1
Вот где проблемы начало:
- инверсия H:
Ошибка: инверсия потребует анализа случая при сортировке Set, которая не допускается для индуктивного определения compile_step.
destruct H:
Ошибка: анализ случая при сортировке Set не допускается для индуктивного определения compile_step.
индукция H:
Ошибка: не удается найти комбинатор исключения compile_step_re c, исключение индуктивного определения compile_step при сортировке Set, вероятно, не разрешено.
Ошибка воспроизводится на более глубоких уровнях иерархии.
Есть ли простое объяснение этому? Есть ли простое решение?
Возможно, , это полезно для некоторых из вас.