Вложенные теоремы в Coq

Question

Возможно ли создание вложенных теорем в контексте текущей теоремы?

У меня есть сильное ощущение, что эта функция еще не реализована полностью. Примеры,

1) Я не могу уничтожить некоторые из типов, которые были в контексте во время процесса доказательства.

Например, есть

"Error: my_var is used in conclusion." 

, когда я пытаюсь определить тип теоремы. У меня есть также

"Error: ... depends on the variable ... which is not declared in the context." 

Но google дал мне только одну ссылку с аналогичной ошибкой. Более того, на самом деле у меня есть m в контексте в этом разделе. Что не так?

2) Я разрушил натуральное число n. Я определил несколько первых шагов. Мне нужно определить синоним на длительный срок. Я хочу локально определить

Definition X:=(n.+1;ob). 

Но я не могу. Я хочу использовать аналог, чтобы ... в ....

Любые идеи?

Answer 1

Действительно, вы правы. «объявление теоремы в доказательстве» не поддерживается Coq из-за некоторых особенностей с побочными эффектами.

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