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 qualified name of the theorem, e.g., Proof-Sort-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_sort_preserves_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: November 2020

Summary of exported operations:

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

Exported operations:

determinismTheoremFor :: String -> String  Deterministic 

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

getModuleProofFiles :: String -> String -> IO [String]  Deterministic 

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

existsProofFor :: (String,String) -> [String] -> Bool  Deterministic 

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

isProofFileNameFor :: (String,String) -> String -> Bool  Deterministic 

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

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

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.