CODEWITHSUNDEEP
testingidristheorem-proving
Bubbler
Bubbler

Reputation: 982

Testing if a proof is sound in Idris

I'm trying to write a test code to check if plusComm : (a : Nat) -> (b : Nat) -> a + b = b + a indeed proves a + b = b + a on natural numbers, i.e. the code does not fake one using typed holes, postulate, believe_me, assert_total, etc.

Specifically, if the proof is faked in some way, I want the program to fail in one of the three ways:

If these options are not feasible, I'm open to source code analysis as a last resort (for my purposes, that should be written in Idris too). I heard of Language.Reflection but I'm not sure if it's the right tool here.

The code below is one attempt that failed because proofEval doesn't even look at the actual value passed:

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))

The above, when compiled and run, produces the following output and exits without error.

Compiled Successfully!
3

Upvotes: 1

Views: 89

Answers (1)

Bubbler
Bubbler

Reputation: 982

Partial answer

I found 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

Output:

Compiled Successfully!
2

Some possible fake proofs and the results:

-- 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

Note that assert_total or believe_me is not caught using this method as marked in the linked snippet.

Upvotes: 1

Related Questions