测试Idris中的证据是否合理

Question

我正在尝试编写一个测试代码来检查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

Answer 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未使用链接代码段中标记的此方法捕获。