kdrag.tactics.Theorem

kdrag.tactics.Theorem(goal: BoolRef | str) → Callable[[Callable[[ProofState], None]], Proof]

A decorator to create a theorem from a function that takes a ProofState as argument.

>>> x = smt.Int("x")
>>> @Theorem(x + 1 > x)
... def mytheorem(l: ProofState):
...     "An example theorem"
...     l.auto()
>>> mytheorem
|= x + 1 > x
>>> mytheorem.__doc__
'An example theorem'
>>> @Theorem("forall (x : Int), x + 1 > x")
... def mytheorem2(l: ProofState):
...     l.auto()
>>> mytheorem2
|= ForAll(x, x + 1 > x)
>>> @Theorem("x + 1 > x") # Getting globals from scope
... def mytheorem3(l: ProofState):
...     l.auto()
>>> mytheorem3
|= x + 1 > x

Parameters:

goal (BoolRef | str)

Return type:

Callable[[Callable[[ProofState], None]], Proof]