A proposition is something SBV is capable of proving/disproving in TP.

Proof for a property. This type is left abstract, i.e., the only way to create on is via a call to lemma/theorem etc., ensuring soundness. (Note that the trusted-code base here is still large: The underlying solver, SBV, and TP kernel itself. But this mechanism ensures we can't create proven things out of thin air, following the standard LCF methodology.)

Get the underlying proof object

Grab the underlying boolean in a proof. Useful in assumption contexts where we need a boolean

Calculate the root of trust. The returned list of proofs, if any, will need to be sorry and quickcheck free to have the given proof to be sorry-free.

Keeping track of where the sorry originates from. Used in displaying dependencies.

Dependencies of a proof, in a tree format.

Display the proof tree as ASCII text. The first argument is if we should compress the tree, showing only the first use of any sublemma.

Display the tree as an html doc for rendering purposes. The first argument is if we should compress the tree, showing only the first use of any sublemma. Second is the path (or URL) to external CSS file, if needed.

Accept the given definition as a fact. Usually used to introduce definitial axioms, giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions, if you assert nonsense, then you get nonsense back. So, calls to axiom should be limited to definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols.

Prove a given statement, using auxiliaries as helpers. Using the default solver.

Prove a lemma, using the given configuration

Prove a property via a series of equality steps, using the default solver. Let H be a list of already established lemmas. Let P be a property we wanted to prove, named name. Consider a call of the form calc name P (cond, [A, B, C, D]) H. Note that H is a list of already proven facts, ensured by the type signature. We proceed as follows:

• Prove: (H && cond) -> (A == B)
• Prove: (H && cond && A == B) -> (B == C)
• Prove: (H && cond && A == B && B == C) -> (C == D)
• Prove: (H && (cond -> (A == B && B == C && C == D))) -> P
• If all of the above steps succeed, conclude P.

cond acts as the context. Typically, if you are trying to prove Y -> Z, then you want cond to be Y. (This is similar to intros commands in theorem provers.)

So, calc-lemma is essentially modus-ponens, applied in a sequence of stepwise equality reasoning in the case of non-boolean steps.

If there are no helpers given (i.e., if H is empty), then this call is equivalent to lemmaWith.

Prove a property via a series of equality steps, using the given solver.

Inductively prove a lemma, using the default config. Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only partial correctness is guaranteed if non-terminating functions are involved.

Same as induct, but with the given solver configuration. Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only partial correctness is guaranteed if non-terminating functions are involved.

Inductively prove a lemma, using measure based induction, using the default config. Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only partial correctness is guaranteed if non-terminating functions are involved.

Same as sInduct, but with the given solver configuration. Inductive proofs over lists only hold for finite lists. We also assume that all functions involved are terminating. SBV does not prove termination, so only partial correctness is guaranteed if non-terminating functions are involved.

Apply a universal proof to some arguments, creating a boolean expression guaranteed to be true

Instantiation for a universally quantified variable

A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver cannot deal with, or if we want to postpone the proof for the time being. TP will keep track of the uses of sorry and will print them appropriately while printing proofs. NB. We keep this as a ProofObj as opposed to a Proof as it is then easier to use it as a lemma helper.

Monad for running TP proofs in.

Run a TP proof, using the default configuration.

Run a TP proof, using the given configuration.

Make TP proofs quiet. Note that this setting will be effective with the call to runTP/runTPWith, i.e., if you change the solver in a call to lemmaWith/theoremWith, we will inherit the quiet settings from the surrounding environment.

Change the size of the ribbon for TP proofs. Note that this setting will be effective with the call to runTP/runTPWith, i.e., if you change the solver in a call to lemmaWith/theoremWith, we will inherit the ribbon settings from the surrounding environment.

Make TP proofs produce statistics. Note that this setting will be effective with the call to runTP/runTPWith, i.e., if you change the solver in a call to lemmaWith/theoremWith, we will inherit the statistics settings from the surrounding environment.

Make TP proofs use proof-cache. Note that if you use this option then you are obligated to ensure all lemma/theorem names/type pairs you use are unique for the whole run. (That is, we will reuse proofs if they have the same name and type; hence if you prove two theorems that share name and type will be considered the same.) If you don't ensure this uniqueness, the results are not guaranteed to be sound. A good tip is to run the proof at least once to completion, and use cache for regression purposes to avoid re-runs. Also, this setting will be effective with the call to runTP/runTPWith, i.e., if you -- the solver in a call to lemmaWith/theoremWith, we will inherit the caching behavior settings from the surrounding environment.

Start a calculational proof, with the given hypothesis. Use [] as the first argument if the calculation holds unconditionally. The first argument is typically used to introduce hypotheses in proofs of implications such as A .=> B .=> C, where we would put [A, B] as the starting assumption. You can name these and later use in the derivation steps.

Alternative unicode for |-.

Chain steps in a calculational proof.

Unicode alternative for =:.

Attaching a hint

Alternative unicode for ??.

A quick-check step, taking number of tests.

A quick-check step, with specific quick-check args.

Case splitting over a list; empty and full cases

Case splitting over two lists; empty and full cases for each

The boolean case-split

Alternative unicode for ==>

Specifying a case-split, helps with the boolean case.

Mark the end of a calculational proof.

Mark a proof as trivial, i.e., the solver should be able to deduce it without any help.

Mark a proof as contradiction, i.e., the solver should be able to conclude it by reasoning that the current path is infeasible

Observing values in case of failure.