在 Idris 中测试证明是否合理答案

【问题标题】：Testing if a proof is sound in Idris在 Idris 中测试证明是否合理
【发布时间】：2019-03-09 06:57:00
【问题描述】：

我正在尝试编写一个测试代码来检查 plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a 是否确实在自然数上证明 a + b = b + a，即代码不会使用类型孔伪造一个，postulate，believe_me，assert_total，等等

具体来说，如果证明以某种方式被伪造，我希望程序以以下三种方式之一失败：

编译错误
运行时错误，例如段错误
运行时无限循环

如果这些选项不可行，我愿意将源代码分析作为最后的手段（出于我的目的，这也应该用 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

【问题讨论】：

标签： testing idris theorem-proving

【解决方案1】：

部分回答

我找到a way to catch postulate and holes using dependent tuples：

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 不会使用此方法捕获，如链接的 sn-p 中所标记。

【讨论】：