Проверка правильности доказательства в Идрисе - PullRequest
Новая
       31

Проверка правильности доказательства в Идрисе

1 голос
/ 09 марта 2019

Я пытаюсь написать тестовый код, чтобы проверить, действительно ли plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a доказывает a + b = b + a на натуральных числах, то есть код не фальсифицирует код с использованием типизированных дырок, postulate, believe_me, assert_total, и т.д.

В частности, если доказательство каким-то образом сфальсифицировано, я хочу, чтобы программа провалилась одним из трех способов:

  • Ошибка компиляции
  • Ошибка времени выполнения, например * 1013 выдаёт ошибку сегментации *
  • Время выполнения бесконечного цикла

Если эти опции неосуществимы, я открыт для анализа исходного кода в качестве крайней меры (для моих целей это должно быть написано также в Idris). Я слышал о Language.Reflection, но я не уверен, что это правильный инструмент здесь.

Приведенный ниже код - одна попытка, которая не удалась, потому что proofEval даже не смотрит на фактическое переданное значение: 

plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm a b = ?plusComm

proofEval : {a : ty} -> (a = b) -> ty
proofEval {a=a} _ = a

main : IO ()
main = do
  putStrLn "Compiled Successfully!"
  print (proofEval (plusComm 1 2))

Вышеуказанное при компиляции и запуске выдает следующий вывод и завершается без ошибок. 

Compiled Successfully!
3

1 Ответ

1 голос
/ 10 марта 2019

Частичный ответ

Я нашел способ поймать postulate и дыры, используя зависимые кортежи : 

plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = plusCommutative

proofEval : (a : Nat) -> (b : Nat) -> (a : Nat ** (b : Nat ** (a + b = b + a)))
proofEval a b = (a ** (b ** plusComm a b))

main : IO ()
main = do
  putStrLn "Compiled Successfully!"
  print $ fst $ snd $ proofEval 1 2
  -- `print $ fst $ proofEval 1 2` doesn't work for the purpose

Вывод: 

Compiled Successfully!
2

Некоторые возможные поддельные доказательства и результаты: 

-- typed hole
plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
plusComm = ?plusComm
-- result: runtime error (abort)
ABORT: Attempt to evaluate hole Main.plusComm1

-- postulate
postulate plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a
-- result: compilation error
reachable postulates:
  Main.plusComm

Обратите внимание, что assert_total или believe_me не перехватывается при использовании этого метода , как отмечено в связанном фрагменте.

...