copilot-theorem-4.7.1: k-induction for Copilot.

Safe Haskell | Safe
Language | Haskell2010

Copilot.Theorem.Prove

Description

Connection to theorem provers.

Synopsis

- data Output = Output Status [String]
- data Status
  - = Sat
  - | Valid
  - | Invalid
  - | Unknown
  - | Error
- data Prover = Prover {
  - proverName :: String
  - startProver :: Spec -> IO r
  - askProver :: r -> [PropId] -> [PropId] -> IO Output
  - closeProver :: r -> IO ()
  }
- type PropId = String
- data PropRef a where
  - PropRef :: forall a. PropId -> PropRef a
- type Proof a = ProofScheme a ()
- type UProof = Writer [Action] ()
- data ProofScheme a b where
  - Proof :: forall b a. Writer [Action] b -> ProofScheme a b
- data Action where
  - Check :: Prover -> Action
  - Assume :: PropId -> Action
  - Admit :: Action
- data Universal
- data Existential
- check :: Prover -> Proof a
- prove :: Spec -> PropId -> UProof -> IO Bool
- combine :: Prover -> Prover -> Prover

# Documentation

data Output Source #

Output produced by a prover, containing the `Status` of the proof and additional information.

Constructors

Output Status [String] |

data Status Source #

Status returned by a prover when given a specification and a property to prove.

Constructors

Sat |
Valid |
Invalid |
Unknown |
Error |

data Prover Source #

A connection to a prover able to check the satisfiability of specifications.

The most important is `askProver`, which takes 3 arguments :

- The prover descriptor
- A list of properties names which are assumptions
- A properties that have to be deduced from these assumptions

Constructors

Prover |

Fields

- proverName :: String
- startProver :: Spec -> IO r
- askProver :: r -> [PropId] -> [PropId] -> IO Output
- closeProver :: r -> IO ()

type PropId = String Source #

A unique property identifier

data PropRef a where Source #

Reference to a property.

Constructors

PropRef :: forall a. PropId -> PropRef a |

type Proof a = ProofScheme a () Source #

A proof scheme with unit result.

type UProof = Writer [Action] () Source #

A sequence of computations that generate a trace of required prover `Action`s.

data ProofScheme a b where Source #

A proof scheme is a sequence of computations that compute a result and generate a trace of required prover `Action`s.

Constructors

Proof :: forall b a. Writer [Action] b -> ProofScheme a b |

#### Instances

Instances details

Applicative (ProofScheme a) Source # |

Instance details

Defined in Copilot.Theorem.Prove

Methods

pure :: a0 -> ProofScheme a a0 Source #

(<*>) :: ProofScheme a (a0 -> b) -> ProofScheme a a0 -> ProofScheme a b Source #

liftA2 :: (a0 -> b -> c) -> ProofScheme a a0 -> ProofScheme a b -> ProofScheme a c Source #

(*>) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a b Source #

(<*) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a a0 Source #

Functor (ProofScheme a) Source # |
Instance details Defined in Copilot.Theorem.Prove Methods fmap :: (a0 -> b) -> ProofScheme a a0 -> ProofScheme a b Source # (<$) :: a0 -> ProofScheme a b -> ProofScheme a a0 Source #
Monad (ProofScheme a) Source # |
Instance details Defined in Copilot.Theorem.Prove Methods (>>=) :: ProofScheme a a0 -> (a0 -> ProofScheme a b) -> ProofScheme a b Source # (>>) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a b Source # return :: a0 -> ProofScheme a a0 Source #

data Action where Source #

Prover actions.

Constructors

Check :: Prover -> Action |
Assume :: PropId -> Action |
Admit :: Action |

data Universal Source #

Empty datatype to mark proofs of universally quantified predicates.

data Existential Source #

Empty datatype to mark proofs of existentially quantified predicates.

check :: Prover -> Proof a Source #

Record a requirement for satisfiability checking.

prove :: Spec -> PropId -> UProof -> IO Bool Source #

Try to prove a property in a specification with a given proof scheme.

Return `True` if a proof of satisfiability or validity is found, false otherwise.

combine :: Prover -> Prover -> Prover Source #

Combine two provers producing a new prover that will run both provers in parallel and combine their outputs.

The results produced by the provers must be consistent. For example, if one of the provers indicates that a property is `Valid` while another indicates that it is `Invalid`, the combination of both provers will return an `Error`.