Module TheoremUsage

This module contains some operations to access and check proof for theorems formulated as properties in Curry programs.

Current assumptions:

  • A theorem is represented in a source file as a EasyCheck property, e.g.:
    sortPreservesLength xs = length xs -=- length (sort xs)
  • A theorem is considered as proven and, thus, not be checked by CurryCheck or the contract wrapper (see currypp), if there exists a file named with prefix "Proof" and the name of the theorem, e.g., Proof-sortPreservesLength.agda. The name is not case sensitive, the file name extension is arbitrary and the special characters in the name are ignored. Hence, a proof for sortlength could be also stored in a file named PROOF_sort-perserves-length.smt.
  • A proof that some operation f is deterministic has the name fIsDeterministic so that a proof for last can be stored in proof-last-is-deterministic.agda (and also in some other files).

Author: Michael Hanus

Version: August 2016

Summary of exported operations:

determinismTheoremFor :: String -> String   
The name of a proof of a determinism annotation for the operation given as the argument.
getProofFiles :: String -> IO [String]   
Get the names of all files in the directory (first argument) containing proofs of theorems.
existsProofFor :: String -> [String] -> Bool   
Does the list of file names (second argument) contain a proof of the theorem given as the first argument?
isProofFileName :: String -> Bool   
Is this a file name with a proof, i.e., start it with proof?
isProofFileNameFor :: String -> String -> Bool   
Is this the file name of a proof of property prop?
getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl]   
Get all theorems which are contained in a given program.

Exported operations:

determinismTheoremFor :: String -> String   

The name of a proof of a determinism annotation for the operation given as the argument.

Further infos:
  • solution complete, i.e., able to compute all solutions

getProofFiles :: String -> IO [String]   

Get the names of all files in the directory (first argument) containing proofs of theorems.

existsProofFor :: String -> [String] -> Bool   

Does the list of file names (second argument) contain a proof of the theorem given as the first argument?

isProofFileName :: String -> Bool   

Is this a file name with a proof, i.e., start it with proof?

isProofFileNameFor :: String -> String -> Bool   

Is this the file name of a proof of property prop?

getTheoremFunctions :: String -> CurryProg -> IO [CFuncDecl]   

Get all theorems which are contained in a given program. A theorem is a property for which a proof file exists in the directory provided as first argument.