kdrag.tactics.prove

kdrag.tactics.prove(thm: BoolRef, fixes: list[ExprRef] = [], assumes: list[BoolRef] = [], by: Proof | Sequence[Proof] | None = None, admit=False, timeout=1000, dump=False, solver=None, unfold: int | list[FuncDeclRef] | None = None) → Proof

Prove a theorem using a list of previously proved lemmas.

In essence prove(Implies(by, thm)).

This wraps the kernel version in order to provide better counterexamples.

Parameters:

  • thm (smt.BoolRef) – The theorem to prove.

  • thm – The theorem to prove.

  • by (list[Proof]) – A list of previously proved lemmas.

  • admit (bool) – If True, admit the theorem without proof.

  • fixes (list[ExprRef])

  • assumes (list[BoolRef])

  • unfold (int | list[FuncDeclRef] | None)

Returns:

A proof object of thm

Return type:

Proof

>>> prove(smt.BoolVal(True))
|= True

>>> prove(smt.RealVal(1) >= smt.RealVal(0))
|= 1 >= 0

>>> x = smt.Int("x")
>>> succ = kd.define("succ", [x], x + 1)
>>> prove(succ(x) == x + 1, unfold=1)
|= succ(x) == x + 1
>>> succ2 = kd.define("succ2", [x], succ(succ(x)))
>>> prove(succ2(x) == x + 2, unfold=2)
|= succ2(x) == x + 2
>>> prove(succ(x) == x + 1, unfold=[succ])
|= succ(x) == x + 1