kdrag.tactics.prove

kdrag.tactics.prove(thm: BoolRef, by: Proof | Sequence[Proof] | None = None, admit=False, timeout=1000, dump=False, solver=None, instan: Callable[[...], list[Proof]] | None = None, unfold=0) → 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.

  • instan (Callable[[...], list[Proof]] | 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(smt.ForAll([x], succ(x) == x + 1), instan=lambda x1: [succ.defn(x1)])
|- ForAll(x, succ(x) == x + 1)