kdrag.tactics

Tactics are helpers that organize calls to the kernel. The code of these helpers don’t have to be trusted.

Functions

`ForAllI`(vs, pf)	All vs must be FreshVars Combinator name tries to make it clear that this is a smt.ForAll that works on Proofs instead of BoolRefs.
`FreshVar`(name, sort[, assume])	Create a schema variable with the given name and sort.
`FreshVars`(names, sort)	Create a list of schema variables with the given names and sort.
`Lemma`(goal[, fixes, assumes])
`PTheorem`(goal)	A decorator to create a theorem from a function that takes a ProofState as argument.
`Theorem`(goal)	A decorator to create a theorem from a function that takes a ProofState as argument.
`auto`([shows])
`forallI`(e, cb)	Open a forall quantifier but giving a new goal and fresh variables to a callback function.
`open_binder`(pf)	Open a proof with schematic variables so that it can be reconstructed.
`prove`(thm[, fixes, assumes, by, admit, ...])	Prove a theorem using a list of previously proved lemmas.
`simp`(t[, by])
`simp_tac`(e)	Simplify an expression using simp and return the resulting equality as a proof.
`skolem`(pf)	Skolemize an existential quantifier.
`subst`(pf, vs, subst)	Perform substitution into a forall quantified proof, instantiating into a new context vs

Classes

`Calc`(vars, lhs[, assume])	Calc is for equational reasoning.
`Goal`(sig, ctx, goal)
`LemmaCallback`(cb[, annot])
`ProofState`(goal[, _parent])	A tactic class for interactive proofs.

class kdrag.tactics.Calc(vars: list[ExprRef], lhs: ExprRef, assume=[])

Bases: object

Calc is for equational reasoning. One can write a sequence of formulas interspersed with useful lemmas.

Parameters:

vars (list[ExprRef])
lhs (ExprRef)

eq(rhs, by=[], **kwargs)

ge(rhs, by=[])

gt(rhs, by=[])

le(rhs, by=[])

lt(rhs, by=[])

qed(**kwargs)

kdrag.tactics.ForAllI(vs: list[ExprRef], pf: Proof) → Proof

All vs must be FreshVars Combinator name tries to make it clear that this is a smt.ForAll that works on Proofs instead of BoolRefs.

Parameters:

vs (list[ExprRef])
pf (Proof)

Return type:

Proof

kdrag.tactics.FreshVar(name: str, sort: SortRef, assume=None) → ExprRef

Create a schema variable with the given name and sort.

Parameters:

name (str)
sort (SortRef)

Return type:

ExprRef

kdrag.tactics.FreshVars(names: str, sort: SortRef) → list[ExprRef]

Create a list of schema variables with the given names and sort.

Parameters:

names (str)
sort (SortRef)

Return type:

list[ExprRef]

class kdrag.tactics.Goal(sig, ctx, goal)

Bases: NamedTuple

Parameters:

sig (list[ExprRef])
ctx (list[BoolRef])
goal (BoolRef | QuantifierRef)

count(value, /): Return number of occurrences of value.

ctx: list[BoolRef]: Alias for field number 1

classmethod empty() → Goal

Return type:: Goal

goal: BoolRef | QuantifierRef: Alias for field number 2

index(value, start=0, stop=9223372036854775807, /)

Return first index of value.

Raises ValueError if the value is not present.

is_empty() → bool

Return type:: bool

proof() → ProofState

Return type:: ProofState

sig: list[ExprRef]: Alias for field number 0

to_expr()

Convert goal into formula it represents

>>> x = smt.Int("x")
>>> Goal(sig=[x], ctx=[x > 0], goal=x > -1).to_expr()
Implies(x > 0, x > -1)
>>> Goal(sig=[], ctx=[], goal=x > 0).to_expr()
x > 0
>>> Goal(sig=[], ctx=[x > 0], goal=x > -1).to_expr()
Implies(x > 0, x > -1)

kdrag.tactics.Lemma(goal: BoolRef, fixes=None, assumes=None) → ProofState

Parameters:: goal (BoolRef)
Return type:: ProofState

class kdrag.tactics.LemmaCallback(cb: Callable[[], NoneType], annot: object = None)

Bases: object

Parameters:

cb (Callable[[], None])
annot (object)

annot: object = None

cb: Callable[[], None]

kdrag.tactics.PTheorem(goal: BoolRef | str)

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

>>> x = smt.Int("x")
>>> @PTheorem(x + 1 > x)
... def mytheorem(l: ProofState):
...     "An example theorem"
...     l.auto()
Lemma Complete! Change PTheorem to Theorem

Parameters:: goal (BoolRef | str)

class kdrag.tactics.ProofState(goal: Goal, _parent=None)

Bases: object

A tactic class for interactive proofs. ProofState stores a mutational partial proof state that can be changed via tactic methods. Once proof is completed, an actual kd.Proof object is constructed by the Lemma.qed method. ProofState is not part of the trusted code base and bugs in its implementation are not a soundness concern. ProofState “merely” orchestrates and infers info for calls to the kernel. In my experience it is best to run the entire Lemma mutation in a single Jupyter cell while experimenting.

ProofState can be seen as - A Builder or Factory for kd.Proof objects. l.qed() is the analog of a build function which calls the constructor kd.prove under the hood - A node of a Zipper-like context for a proof tree. In other words a partially complete proof.

Parameters:: goal (Goal)

__enter__() → ProofState

On entering a with block, return self. This marks that at the exit of the with block, qed will be automatically called and kd.Proof propagated back to a parent

Return type:: ProofState

__exit__(exc_type, exc_value, traceback): On exiting a with block, if no exception occurred, call qed and propagate the proof to the parent

add_lemma(lemma: Proof)

Record a lemma in the current ProofState state.

Parameters:: lemma (Proof)

admit() → Goal

admit the current goal without proof. Don’t feel bad about keeping yourself moving, but be aware that you’re not done.

>>> l = Lemma(smt.BoolVal(False)) # a false goal
>>> _ = l.admit()
Admitting lemma False
>>> l.qed()
|= False

Return type:: Goal

apply(pf: Proof | int)

apply matches the conclusion of a proven clause

>>> x,y = smt.Ints("x y")
>>> l = kd.Lemma(smt.Implies(smt.Implies(x == 7, y == 3), y == 3))
>>> l.intros()
[Implies(x == 7, y == 3)] ?|= y == 3
>>> l.apply(0)
[Implies(x == 7, y == 3)] ?|= x == 7

>>> mylemma = kd.prove(kd.QForAll([x], x > 1, x > 0))
>>> kd.Lemma(x > 0).apply(mylemma)
[] ?|= x > 1

>>> p,q = smt.Bools("p q")
>>> l = kd.Lemma(smt.Implies(smt.Not(p), q))
>>> l.intros()
[Not(p)] ?|= q
>>> l.apply(0)
[Not(q)] ?|= p

Parameters:: pf (Proof | int)

assumes(hyp: BoolRef)

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p, q))
>>> l.assumes(p)
[p] ?|= q

Parameters:: hyp (BoolRef)

assumption() → Goal

Exact match of goal in the context

Return type:: Goal

auto(**kwargs) → ProofState

auto discharges a goal using z3. It forwards all parameters to kd.prove

Return type:: ProofState

beta(at=None)

Perform beta reduction on goal or context

>>> x = smt.Int("x")
>>> l = Lemma(smt.Lambda([x], x + 1)[3] == 4)
>>> l.beta()
[] ?|= 3 + 1 == 4
>>> l = Lemma(smt.Implies(smt.Lambda([x], x + 1)[3] == 5, True))
>>> l.intros()
[Lambda(x, x + 1)[3] == 5] ?|= True
>>> l.beta(at=0)
[3 + 1 == 5] ?|= True

case(thm=None) → ProofState

To make more readable proofs, case lets you state which case you are currently in from a cases It is basically an alias for have followed by clear(-1).

>>> p = smt.Bool("p")
>>> l = Lemma(smt.Or(p, smt.Not(p)))
>>> _ = l.cases(p)
>>> l.case(p)
[p == True] ?|= Or(p, Not(p))
>>> _ = l.auto()
>>> l.case(smt.Not(p))
[p == False] ?|= Or(p, Not(p))

Return type:: ProofState

cases(t)

cases let’s us consider an object by cases. We consider whether Bools are True or False We consider the different constructors for datatypes

>>> import kdrag.theories.nat as nat
>>> x = smt.Const("x", nat.Nat)
>>> l = Lemma(smt.BoolVal(True))
>>> l.cases(x)
[is(Z, x) == True] ?|= True
>>> l.auto() # next case
[is(S, x) == True] ?|= True

clear(n: int)

Remove a hypothesis from the context

Parameters:: n (int)

contra()

Prove the goal by contradiction.

>>> p = smt.Bool("p")
>>> l = Lemma(p)
>>> l.contra()
[Not(p)] ?|= False

copy()

ProofState methods mutates the proof state. This can make you a copy. Does not copy the pushed ProofState stack.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p,q))
>>> l1 = l.copy()
>>> l.intros()
[p] ?|= q
>>> l1
[] ?|= Implies(p, q)

eq(rhs: ExprRef, **kwargs)

replace rhs in equational goal

Parameters:: rhs (ExprRef)

exact(pf: Proof)

Exact match of goal with given proof

>>> p = smt.Bool("p")
>>> l = Lemma(smt.Implies(p, p))
>>> l.exact(kd.prove(smt.BoolVal(True)))
Traceback (most recent call last):
    ...
ValueError: Exact tactic failed. Given: True Expected: Implies(p, p)
>>> l.exact(kd.prove(smt.Implies(p, p)))
Nothing to do!

Parameters:: pf (Proof)

exists(*ts) → ProofState

Give terms ts to satisfy an exists goal ?|= exists x, p(x) becomes ?|= p(ts)

>>> x,y = smt.Ints("x y")
>>> Lemma(smt.Exists([x], x == y)).exists(y)
[] ?|= y == y

Return type:: ProofState

ext(at=None)

Apply extensionality to a goal

>>> x = smt.Int("x")
>>> l = Lemma(smt.Lambda([x], smt.IntVal(1)) == smt.K(smt.IntSort(), smt.IntVal(1)))
>>> _ = l.ext()

fix(prefix=None) → ExprRef

Open a single ForAll quantifier

>>> x = smt.Int("x")
>>> l = Lemma(smt.ForAll([x], x != x + 1))
>>> _x = l.fix()
>>> l
[x!...] ; [] ?|= x!... != x!... + 1
>>> _x.eq(x)
False
>>> Lemma(smt.ForAll([x], x != x + 1)).fix("w")
w!...

Return type:: ExprRef

fixes(prefixes=None) → list[ExprRef]

fixes opens a forall quantifier. ?|= forall x, p(x) becomes x ?|= p(x)

>>> x,y = smt.Ints("x y")
>>> l = Lemma(kd.QForAll([x,y], y >= 0, x + y >= x))
>>> _x, _y = l.fixes()
>>> l
[x!..., y!...] ?|= Implies(y!... >= 0, x!... + y!... >= x!...)
>>> _x, _y
(x!..., y!...)
>>> _x.eq(x)
False
>>> Lemma(kd.QForAll([x,y], x >= 0)).fixes("z w")
[z!..., w!...]

Return type:: list[ExprRef]

generalize(*vs: ExprRef)

Put variables forall quantified back on goal. Useful for strengthening induction hypotheses.

Parameters:: vs (ExprRef)

get_lemma(thm: BoolRef) → Proof

Parameters:: thm (BoolRef)
Return type:: Proof

have(conc: BoolRef, **kwargs) → ProofState

Prove the given formula and add it to the current context

>>> x = smt.Int("x")
>>> l = Lemma(smt.Implies(x > 0, x > -2))
>>> l.intros()
[x > 0] ?|= x > -2
>>> l.have(x > -1, by=[])
[x > 0, x > -1] ?|= x > -2
>>> l.have(x > 42)
[x > 0, x > -1] ?|= x > 42

Parameters:: conc (BoolRef)
Return type:: ProofState

induct(x: ExprRef, using: Callable[[ExprRef, Callable[[ExprRef, BoolRef], BoolRef]], Proof] | None = None)

Apply an induction lemma instantiated on x.

Parameters:

x (ExprRef)
using (Callable[[ExprRef, Callable[[ExprRef, BoolRef], BoolRef]], Proof] | None)

intros() → ExprRef | list[ExprRef] | Goal

intros opens an implication. ?|= p -> q becomes p ?|= q

>>> p,q,r = smt.Bools("p q r")
>>> l = Lemma(smt.Implies(p, q))
>>> l.intros()
[p] ?|= q
>>> l = Lemma(smt.Not(q))
>>> l.intros()
[q] ?|= False

Return type:: ExprRef | list[ExprRef] | Goal

left(n=0)

Select the left case of an Or goal. Since we’re working classically, the other cases are negated and added to the context.

>>> p,q,r = smt.Bools("p q r")
>>> l = Lemma(smt.Or(p,q))
>>> l.left()
[Not(q)] ?|= p
>>> l = Lemma(smt.Or(p,q,r))
>>> l.left(1)
[Not(p), Not(r)] ?|= q

newgoal(newgoal: BoolRef, **kwargs)

Try to show newgoal is sufficient to prove current goal

Parameters:: newgoal (BoolRef)

obtain(n) → ExprRef | list[ExprRef]

obtain opens an exists quantifier in context and returns the fresh eigenvariable. [exists x, p(x)] ?|= goal becomes p(x) ?|= goal

Return type:: ExprRef | list[ExprRef]

pop(): Pop state off the ProofState stack.

pop_goal() → Goal

Return type:: Goal

pop_lemmas()

push()

Push a copy of the current ProofState state onto a stack. This why you can try things out, and if they fail

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p,q))
>>> l.push()
[] ?|= Implies(p, q)
>>> l.intros()
[p] ?|= q
>>> l.pop()
[] ?|= Implies(p, q)

push_lemmas()

qed(**kwargs) → Proof

return the actual final Proof of the lemma that was defined at the beginning.

Return type:: Proof

qfix(prefix=None) → ExprRef

Return type:: ExprRef

qfixes(prefixes=None) → list[ExprRef]

Return type:: list[ExprRef]

repeat(f: Callable[[], Goal]) → Goal

>>> p = smt.Bool("p")
>>> l = Lemma(smt.Implies(p, smt.Implies(p, p)))
>>> l.intros()
[p] ?|= Implies(p, p)
>>> l = Lemma(smt.Implies(p, smt.Implies(p, p)))
>>> l.repeat(lambda: l.intros())
[p, p] ?|= p

Parameters:: f (Callable[[], Goal])
Return type:: Goal

revert(n: int)

Move a hypothesis back onto the goal as an implication. >>> p,q = smt.Bools(“p q”) >>> l = Lemma(smt.Implies(p, q)) >>> l.intros() [p] ?|= q >>> l.revert(0) [] ?|= Implies(p, q)

Parameters:: n (int)

right()

Select the right case of an Or goal. Since we’re working classically, the other cases are negated and added to the context.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Or(p,q))
>>> l.right()
[Not(p)] ?|= q

rw(rule: Proof | int, at=None, rev=False, **kwargs) → ProofState

rewrite allows you to apply rewrite rule (which may either be a Proof or an index into the context) to the goal or to the context.

>>> x = kd.FreshVar("x", smt.RealSort())
>>> pf = kd.prove(smt.Implies(x >= 0, smt.Sqrt(x) ** 2 == x)).forall([x])
>>> l = Lemma(smt.Implies(x >= 0, smt.Sqrt(x + 2)**2 == x + 2))
>>> l.intros()
[x!... >= 0] ?|= ((x!... + 2)**(1/2))**2 == x!... + 2
>>> l.rw(pf,by=[])
[x!... >= 0, x!... + 2 >= 0] ?|= x!... + 2 == x!... + 2

Parameters:: rule (Proof | int)
Return type:: ProofState

search(*args, at=None, db={})

Search the lemma database for things that may match the current goal.

>>> import kdrag.theories.nat as nat
>>> n = smt.Const("n", nat.Nat)
>>> l = Lemma(smt.ForAll([n], nat.Z + n == n))
>>> ("kdrag.theories.nat.add_Z", nat.add_Z) in l.search().keys()
True
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search().keys()
False
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search(nat.add).keys()
True

show(thm: BoolRef, **kwargs) → ProofState

Documents the current goal and discharge it if by keyword is used

>>> x = smt.Int("x")
>>> l = Lemma(smt.Implies(x > 0, smt.And(x > -2, x > -1)))
>>> l.intros()
[x > 0] ?|= And(x > -2, x > -1)
>>> l.split()
[x > 0] ?|= x > -2
>>> with l.show(x > -2).sub() as sub1:
...     _ = sub1.auto()
>>> l
[x > 0] ?|= x > -1
>>> l.show(x > -1, by=[])
Nothing to do. Hooray!
>>> l.qed()
|= Implies(x > 0, And(x > -2, x > -1))

Parameters:: thm (BoolRef)
Return type:: ProofState

simp(at=None, unfold=False, path=None) → ProofState

Use built in z3 simplifier. May be useful for boolean, arithmetic, lambda, and array simplifications.

>>> x,y = smt.Ints("x y")
>>> l = Lemma(x + y == y + x)
>>> l.simp()
[] ?|= True
>>> l = Lemma(x == 3 + y + 7)
>>> l.simp()
[] ?|= x == 10 + y
>>> l = Lemma(smt.Lambda([x], x + 1)[3] == y)
>>> l.simp()
[] ?|= 4 == y
>>> l = Lemma(1 + ((2 + smt.IntVal(4)) + 3))
>>> l.simp(path=[1,0])
[] ?|= 1 + 6 + 3

Return type:: ProofState

specialize(n, *ts)

Instantiate a universal quantifier in the context.

>>> x,y = smt.Ints("x y")
>>> l = Lemma(smt.Implies(smt.ForAll([x],x == y), True))
>>> l.intros()
[ForAll(x, x == y)] ?|= True
>>> l.specialize(0, smt.IntVal(42))
[ForAll(x, x == y), 42 == y] ?|= True

split(at=None) → ProofState

split breaks apart an And or bi-implication == goal. The optional keyword at allows you to break apart an And or Or in the context

>>> p = smt.Bool("p")
>>> l = Lemma(smt.And(True,p))
>>> l.split()
[] ?|= True
>>> l.auto() # next goal
[] ?|= p

Return type:: ProofState

sub() → ProofState

Return type:: ProofState

sublemma() → ProofState

Create a sub ProofState for the current goal. This is useful to break up a proof into smaller lemmas. The goal is the same but the internally held kd.Proof database is cleared, making it easier for z3 On calling ‘l.qed(), the sublemma will propagate it’s kd.Proof back to it’s parent.

>>> l1 = Lemma(smt.BoolVal(True))
>>> l2 = l1.sublemma()
>>> l2
[] ?|= True
>>> l2.auto()
Nothing to do. Hooray!
>>> l1
[] ?|= True
>>> l2.qed()
|= True
>>> l1
Nothing to do. Hooray!
>>> l1.qed()
|= True

Return type:: ProofState

symm()

Swap left and right hand side of equational goal

>>> x,y = smt.Ints("x y")
>>> Lemma(x == y).symm()
[] ?|= y == x

top_goal() → Goal

Return type:: Goal

unfold(*decls: FuncDeclRef, at=None) → ProofState

Unfold all definitions once. If declarations are given, only those are unfolded.

>>> import kdrag.theories.nat as nat
>>> l = Lemma(nat.Z + nat.Z == nat.Z)
>>> l
[] ?|= add(Z, Z) == Z
>>> l.unfold(nat.double) # does not unfold add
[] ?|= add(Z, Z) == Z
>>> l.unfold()
[] ?|= If(is(Z, Z), Z, S(add(pred(Z), Z))) == Z

Parameters:: decls (FuncDeclRef)
Return type:: ProofState

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]

kdrag.tactics.auto(shows=None, **kwargs) → Proof

Return type:: Proof

kdrag.tactics.forallI(e: QuantifierRef, cb: Callable[[BoolRef, ExprRef], Proof]) → Proof

Open a forall quantifier but giving a new goal and fresh variables to a callback function.

>>> x = smt.Int("x")
>>> forallI(smt.ForAll([x], x > x - 1), lambda goal, x1: kd.prove(goal))
|= ForAll(x, x > x - 1)

Parameters:

e (QuantifierRef)
cb (Callable[[BoolRef, ExprRef], Proof])

Return type:

Proof

kdrag.tactics.open_binder(pf: Proof) → tuple[list[ExprRef], Proof]

Open a proof with schematic variables so that it can be reconstructed.

>>> x,y,z = smt.Reals("x y z")
>>> pf = kd.prove(smt.ForAll([x,y], x + y + 1 > x + y))
>>> open_binder(pf)
([x!..., y!...], |= x!... + y!... + 1 > x!... + y!...)

Parameters:: pf (Proof)
Return type:: tuple[list[ExprRef], Proof]

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

kdrag.tactics.simp(t: ExprRef, by: list[Proof] = [], **kwargs) → Proof

Parameters:

t (ExprRef)
by (list[Proof])

Return type:

Proof

kdrag.tactics.simp_tac(e: ExprRef) → Proof

Simplify an expression using simp and return the resulting equality as a proof.

>>> import kdrag.theories.nat as nat
>>> simp_tac(nat.Z + nat.S(nat.Z))
|= add(Z, S(Z)) == S(Z)

Parameters:: e (ExprRef)
Return type:: Proof

kdrag.tactics.skolem(pf: Proof) → tuple[list[ExprRef], Proof]

Skolemize an existential quantifier.

>>> x = smt.Int("x")
>>> pf = kd.prove(smt.Exists([x], x > 0))
>>> skolem(pf)
([x!...], |= x!... > 0)

Parameters:: pf (Proof)
Return type:: tuple[list[ExprRef], Proof]

kdrag.tactics.subst(pf: Proof, vs: list[ExprRef], subst: list[ExprRef]) → Proof

Perform substitution into a forall quantified proof, instantiating into a new context vs

>>> x,y,z = smt.Reals("x y z")
>>> p = kd.prove(smt.ForAll([x,z], smt.And(z == z, x == x)))
>>> subst(p, [y, z], [y + 1, z])
|= ForAll([y, z], And(z == z, y + 1 == y + 1))

Parameters:

pf (Proof)
vs (list[ExprRef])
subst (list[ExprRef])

Return type:

Proof