kdrag.tactics
Tactics are helpers that organize calls to the kernel. The code of these helpers don’t have to be trusted.
Functions
|
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. |
|
Create a list of schema variables with the given names and sort. |
|
Open a forall quantifier but giving a new goal and fresh variables to a callback function. |
|
Open a proof with schematic variables so that it can be reconstructed. |
|
Prove a theorem using a list of previously proved lemmas. |
|
|
|
Simplify an expression using simp and return the resulting equality as a proof. |
|
Perform substitution into a forall quantified proof, instantiating into a new context vs |
Classes
|
Calc is for equational reasoning. |
|
|
|
A tactic class for interactive proofs. |
|
- class kdrag.tactics.Calc(vars: list[ExprRef], lhs: ExprRef, assume=[])
Bases:
objectCalc 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.
- 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
- 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
- sig: list[ExprRef]
Alias for field number 0
- class kdrag.tactics.Lemma(goal: BoolRef)
Bases:
objectA tactic class for interactive proofs. Lemma 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. Lemma is not part of the trusted code base and bugs in its implementation are not a soundness concern. Lemma “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.
- Parameters:
goal (BoolRef)
- 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() >>> l.qed() |= False
- Return type:
- 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
- Parameters:
pf (Proof | int)
- assumption()
Exact match of goal in the context
- auto(**kwargs)
auto discharges a goal using z3. It forwards all parameters to kd.prove
- 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
- 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)
- copy()
Lemma methods mutates the proof state. This can make you a copy. Does not copy the pushed Lemma stack.
>>> p,q = smt.Bools("p q") >>> l = Lemma(smt.Implies(p,q)) >>> l1 = l.copy() >>> l.intros() [p] ?|= q >>> l1 [] ?|= Implies(p, q)
- einstan(n)
einstan opens an exists quantifier in context and returns the fresh eigenvariable. [exists x, p(x)] ?|= goal becomes p(x) ?|= goal
- eq(rhs: ExprRef, **kwargs)
replace rhs in equational goal
- Parameters:
rhs (ExprRef)
- exists(*ts)
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
- ext()
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() 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
- Return type:
ExprRef
- fixes() 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
- Return type:
list[ExprRef]
- generalize(*vs: ExprRef)
Put variables forall quantified back on goal. Useful for strengthening induction hypotheses.
- Parameters:
vs (ExprRef)
- have(conc: BoolRef, **kwargs)
Prove the given formula and add it to the current context
- Parameters:
conc (BoolRef)
- 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)
- instan(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.instan(0, smt.IntVal(42)) [ForAll(x, x == y), 42 == y] ?|= True
- 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.
>>> p,q = smt.Bools("p q") >>> l = Lemma(smt.Or(p,q)) >>> l.left() [] ?|= p
- newgoal(newgoal: BoolRef, **kwargs)
Try to show newgoal is sufficient to prove current goal
- Parameters:
newgoal (BoolRef)
- pop()
Pop state off the Lemma stack.
- pop_lemmas()
- push()
Push a copy of the current Lemma 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:
- rewrite(rule: Proof | int, at=None, rev=False)
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.
- Parameters:
rule (Proof | int)
- right()
Select the right case of an Or goal.
>>> p,q = smt.Bools("p q") >>> l = Lemma(smt.Or(p,q)) >>> l.right() [] ?|= q
- 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)
To document the current goal
- Parameters:
thm (BoolRef)
- simp(at=None, unfold=False, path=None)
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
- split(at=None)
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
- symm()
Swap left and right hand side of equational goal
>>> x,y = smt.Ints("x y") >>> Lemma(x == y).symm() [] ?|= y == x
- unfold(*decls: FuncDeclRef, at=None)
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)
- 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.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)
- 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!...)
- 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:
- Returns:
A proof object of thm
- Return type:
>>> 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)
- 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:
- 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))