Анализ воздействия Coq

Question

Допустим, у меня есть несколько доказательств, основанных на структуре данных (или лемме) A .Затем я произвел рефакторинг от A до A ', есть ли у Coq возможность общей практики / инструмента узнать, на все доказательства повлиял мой рефакторинг?

Спасибо, что пролили свет на этот вопрос.

edit1: спасибо за все ваши предложения, я дам им попытку и вернемся к этому.

Answer 1

Возможно, вы захотите взглянуть на PUMPKIN PATCH ( GitHub repo ).Вот цитата из файла readme проекта:

Это плагин-прототип для поиска исправлений для неработающих доказательств Coq.Чтобы использовать PUMPKIN, программист модифицирует сценарий с одним доказательством, чтобы обеспечить пример адаптации доказательства к изменению.PUMPKIN обобщает этот пример в патч многократного использования, который можно использовать для исправления других сломанных доказательств.

Не уверен, что это именно то, что вы ищете, но он может представлять интерес.

Answer 2

Еще одним полезным инструментом может быть dpdgraph , который позволяет отображать всю зависимость использования между различными объектами.

Answer 3

Насколько мне известно, такого инструмента нет.Я обычно делаю рефакторинг кода и пытаюсь его исправить.Из-за доказательств Coq и дисциплины типизации, когда код компилируется снова, обычно это работает.