Как эффективно использовать автоматический поиск доказательств Agda?

При написании доказательств я заметил, что автоматический поиск доказательств Agda часто не находит решений, которые мне кажутся очевидными. К сожалению, создание небольшого примера, иллюстрирующего проблему, кажется трудным, поэтому я пытаюсь вместо этого описать наиболее распространенные закономерности.

  • Я забыл добавить -m в отверстие, чтобы Agda посмотрела на область видимости модуля. Могу ли я установить этот флаг по умолчанию? Какие у этого были бы недостатки?
  • Часто текущая дыра может быть заполнена параметром функции, которую я собираюсь реализовать. Даже при добавлении -m Agda не будет учитывать параметры функций или символы, указанные в предложениях let или where. Что-то не так в том, чтобы просто попробовать их все?
  • При просмотре цели символы, указанные в предложениях let или where, даже не отображаются. Почему?

Какие еще привычки могут сделать использование авто более эффективным?


agda
person Helmut Grohne    schedule 26.02.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Автоматический поиск доказательств Agda встроен в компилятор. Это делает его быстрым, но ограничивает количество настроек, которые вы можете сделать. Одним из альтернативных подходов может быть реализация аналогичной процедуры поиска доказательств с использованием механизма отражения Agda. С недавней усиленной версией отражения с использованием монады TC вам больше не нужно реализовывать собственную процедуру унификации.

Карлос Томе работал над повторной реализацией этих идей (посмотрите его код https://github.com/carlostome/AutoInAgda). Он работал над несколькими версиями, которые пытались использовать информацию из контекста, выводить отладочную информацию и т. Д. Надеюсь, это поможет!

person BabaBaluchi    schedule 25.09.2017