Примитивные операции в доказательствах

Question

Для изучения зависимых типов я переписываю свою старую игру Haskell в Идрисе. В настоящее время «движок» игры использует встроенные интегральные типы, такие как Word8. Я хотел бы доказать некоторые леммы, связанные с численными свойствами этих чисел (например, двойное отрицание является тождественным). Однако нельзя сказать что-то о поведении примитивных арифметических операций. Что было бы лучше, просто использовать believe_me или другую ручную работу (по крайней мере для самых основных свойств) или переписать мой код с помощью Nat, Fin и других «высокоуровневых» числовых типов?

Answer 1

Я предлагаю использовать postulate для любого из необходимых вам примитивных свойств, будучи осторожным только для использования вещей, которые действительно верны для рассматриваемых числовых типов (что в основном означает только осторожность при переполнении). Так что вы можете сказать что-то вроде:

postulate add_commutes : (x, y : Int) -> x + y = y + x 

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

Answer 2

Я считаю, что на данный момент, как правило, лучше использовать Nat, когда сможете. В конечном итоге разработчики Idris планируют реализовать общий механизм для замены удобных для поиска типов с быстрыми примитивными в компиляции, но пока это происходит только для Nat. Вы могли бы believe_me, если бы вы действительно этого хотели, но у вас получились бы функции, с которыми нелегко работать в доказательствах. Обратите внимание, что если вы решите сыграть с believe_me, то вы должны также рассмотреть really_believe_me, что, по-видимому, делает его более правдоподобным для проверки типа.