Как эффективно использовать поиск доказательств Agda?
При написании доказательств я заметил, что поиск доказательств Agda часто не нашел решений, которые кажутся мне очевидными. К сожалению, с небольшим примером, который иллюстрирует проблему, кажется, сложно, поэтому я пытаюсь описать наиболее распространенные шаблоны.
- Я забыл добавить
-m в отверстие, чтобы Агда посмотрела на область модуля. Могу ли я сделать этот флаг по умолчанию? Какие недостатки имели бы?
- Часто текущее отверстие может быть заполнено параметром функции, которую я собираюсь реализовать. Даже добавляя
-m, Agda не будет рассматривать функциональные параметры или символы, введенные в предложениях let или where. Есть ли что-то не так, просто попробовав их всех?
- При просмотре цели символы, представленные в предложениях
let или where, даже не отображаются. Почему?
Какие другие привычки могут сделать использование авто более эффективным?
Ответы
Ответ 1
Поиск доказательств автоответчика Agda жестко привязан к компилятору. Это делает его быстрым, но ограничивает количество настроек, которые вы можете сделать. Один альтернативный подход было бы реализовать аналогичную процедуру поиска доказательств с использованием Agda отражающий механизм. С недавней расширенной версией отражения с использованием монада ТС, вам больше не нужно выполнять свою собственную процедуру унификации.
Carlos Tome работал над повторной реализацией этих идей (проверьте его код https://github.com/carlostome/AutoInAgda). Он работал над несколькими версии, которые пытаются использовать информацию из контекста, распечатывают информацию об отладке, и т.д. Надеюсь, это поможет!
