Я изучаю Coq, и в книге, из которой я учусь (CPDT), активно используется auto в доказательствах.
Поскольку я учусь, я думаю, что мне было бы полезно увидеть, что именно auto делает под капотом (чем меньше магии на раннем этапе, тем лучше). Есть ли способ заставить его точно отображать, какие тактики или методы он использует для вычисления доказательства?
Если нет, есть ли место, в котором подробно описано, что делает auto?
Есть несколько способов взглянуть на то, что происходит под капотом.
TLDR: поставьте info перед вашей тактикой или используйте Show Proof. до и после вызова тактики и найдите различия.
Чтобы увидеть, что делает конкретный вызов тактики, вы можете добавить префикс is с info, чтобы показать конкретные шаги доказательства, которые он предпринял.
(Это может быть нарушено в Coq 8.4, я вижу, что они предоставляют info_ версии некоторых тактик, прочтите сообщение об ошибке, если вам нужно.)
Это, вероятно, то, что вы хотите на начальном уровне, это уже может быть довольно кратким.
Еще один способ увидеть, что в данный момент происходит в доказательстве, — использовать команду Show Proof.. Он покажет вам текущий построенный термин с дырами и покажет вам, какую дыру должна заполнить каждая из ваших текущих целей.
Это, вероятно, более продвинутый вариант, особенно если вы используете тактику, такую как induction или inversion, так как построенный термин будет достаточно сложным и потребует от вас понимания лежащей в основе природы схем индукции или зависимого сопоставления с образцом (которое следует использовать в CPDT). скоро научит вас).
После того, как вы закончите доказательство с помощью Qed. (или Defined.), вы также можете попросить взглянуть на термин, который был построен с использованием Print term., где term — название теоремы/термина.
Это часто будет большим и уродливым термином, и требуется некоторая тренировка, чтобы иметь возможность читать их для связанных терминов. В частности, если термин был построен с использованием мощных тактик (таких как omega, crush и т. д.), он, вероятно, будет нечитаемым. По сути, вы бы использовали это только для сканирования определенного места интересующего вас термина. Если он содержит более 10 строк, даже не пытайтесь читать его в таком грубом формате! :)
Со всем предыдущим вы можете использовать Set Printing All. заранее, чтобы Coq печатал развернутые, явные версии всего. Это также многословно, но может помочь, когда вам интересно, каковы значения неявных параметров.
Это все, что пришло мне в голову, хотя может быть и больше.
Что касается того, что делает тактика, обычно лучший ответ можно найти в документации:
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic155
По сути, auto пытается использовать все предоставленные подсказки (в зависимости от используемой вами базы данных) и решить вашу задачу, объединив их до некоторой глубины (которую вы можете указать). По умолчанию база данных core, а глубина 5.
Более подробную информацию об этом можно найти здесь:
http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#Hints-базыданных
info_auto показывает только путь к успеху. Чтобы увидеть, что именно пытается auto, можно использовать debug auto.: он показывает все неудачи (!) и успехи.
- person Anton Trunov; 02.01.2018
