kdrag.tactics.lemma

kdrag.tactics.lemma(thm: BoolRef, by: list[None] = [], admit=False, timeout=1000, dump=False, solver=None, defns=True, simps={}) → None

Prove a theorem using a list of previously proved lemmas.

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

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.

Returns:

A proof object of thm

Return type:

Proof

>>> lemma(BoolVal(True))

>>> lemma(RealVal(1) >= RealVal(0))