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

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 KnuckleDragger kernel itself. But this mechanism ensures we can't create proven things out of thin air, following the standard LCF methodology.)

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 given statement, using auxiliaries as helpers. Using the given solver.

Prove a given statement, using auxiliaries as helpers. Essentially the same as lemma, except for the name, using the default solver.

Prove a given statement, using auxiliaries as helpers. Essentially the same as lemmaWith, except for the name.

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. If H is a singleton, then we bail out. A single step in H indicates a usage mistake, since there's no sequence of steps to reason about.

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

Same as calc, except tagged as Theorem

Same as calcWith, except tagged as Theorem

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 theorem. Same as induct, but tagged as a theorem, 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 inductThm, 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 strong 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.

Inductively prove a theorem, using strong induction. Same as sInduct, but tagged as a theorem, 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 sInductThm, 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 an instance of the proof itself.

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. KnuckleDragger will keep track of the uses of sorry and will print them appropriately while printing proofs.

Monad for running KnuckleDragger proofs in.

Run a KD proof, using the default configuration.

Run a KD proof, using the given configuration.

Bring an IO proof into current proof context.

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 =:.

Specify a helper for the given proof step

Alternative unicode for ??.

Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're mixing proofs and booleans in one group of hints.

Smart constructor for creating a helper from a boolean. This is hardly needed, unless you're mixing proofs and booleans in one group of hints.

Specifying a case-split

Mark the end of a calculational proof.