kdrag.tele

Refinement subtyping

https://www.philipzucker.com/refinement_kdrag1/ Semantic Refinement/Dependent Typing for Knuckledragger/SMTLIB Pt 1
https://belle.sourceforge.net/doc/subtypes.pdf Predicate Subtyping with Predicate Sets - Joe Hurd

Module Attributes

Type

User telescope type.

Functions

`DeclareFunction`(name, tele0, T[, by])
`Fin`(n)
`HasType`(ctx, t0, T)	Formula that corresponds to typing judgement ctx \|= t0 : T
`Id`(x, y)
`Pi`(tele0, B)	Multiarity Pi.
`Program`(name, args, T, body)
`TExists`(xs, P)	Dependent exists quantifier for a telescope of variables.
`TForAll`(xs, P)	Dependent forall quantifier for a telescope of variables.
`ann`(x, T)	Annotate an expression with a type.
`axiom_sig`(f, tele0, T)	Assign signature to a function f with a telescope of arguments tele0 as an axiom
`define`(name, args, T, body[, by])	Define a function with a precondition given by a telescope of arguments and a postcondition given by a subset that output will lie in.
`has_type`(ctx, t0, T[, by])	Tactic to check that an expression t0 has type T in a context ctx.
`normalize`(xs)	Normalize a telescope to a list of (variable, formula) pairs.
`open_binder`(e[, n])	Open a formula in telescope form forall x, P(x), forall y, Q(y), R
`prove_sig`(f, tele0, T[, by])
`subsort_domain`(T)	Get the domain sort of a SubSort, which is either an ArrayRef or a QuantifierRef.

Classes

ProgramState(name, args, T, body)

Interactive proof of a function definition.

kdrag.tele.DeclareFunction(name, tele0: Telescope, T: SubSort, by=[]) → FuncDeclRef

>>> x, y = smt.Ints("x y")
>>> Nat = smt.Lambda([x], x >= 0)
>>> GE = lambda x: smt.Lambda([y], y >= x)
>>> inc = DeclareFunction("inc", [(x, Nat)], GE(x))

Parameters:

tele0 (Telescope)
T (SubSort)

Return type:

FuncDeclRef

kdrag.tele.Fin(n)

>>> m = smt.Int("m")
>>> Fin(3)
Lambda(x, And(Lambda(n, n >= 0)[x], x < 3))
>>> kd.prove(smt.Not(smt.Exists([m], Fin(0)[m])))
|= Not(Exists(m,
        Lambda(x, And(Lambda(n, n >= 0)[x], x < 0))[m]))

kdrag.tele.HasType(ctx: Telescope, t0: ExprRef, T: SubSort) → BoolRef

Formula that corresponds to typing judgement ctx |= t0 : T

>>> x = smt.Int("x")
>>> HasType([(x, Nat)], x+1, Pos)
Implies(And(x >= 0), Lambda(n, n > 0)[x + 1])

Parameters:

ctx (Telescope)
t0 (ExprRef)
T (SubSort)

Return type:

BoolRef

kdrag.tele.Id(x: ExprRef, y: ExprRef) → SubSort

>>> x, y = smt.Ints("x y")
>>> p = smt.Const("p", Unit)
>>> has_type([x], Unit.tt, Id(x, x))
|= Implies(And(True), Lambda(p!..., x == x)[tt])
>>> has_type([x, y, (p, Id(x,y))], Unit.tt, Id(y, x))
|= Implies(And(True, True, x == y), Lambda(p!..., y == x)[tt])

Parameters:

x (ExprRef)
y (ExprRef)

Return type:

SubSort

kdrag.tele.Pi(tele0: Telescope, B: SubSort) → SubSort

Multiarity Pi. Dependent Function subsort B is a family because it may include parameters from tele0.

>>> x, y = smt.Ints("x y")
>>> GE = lambda x: smt.Lambda([y], y >= x)
>>> Pi([(x, Nat)], GE(x))
Lambda(f!...,
    ForAll(x, Implies(x >= 0, Lambda(y, y >= x)[f!...[x]])))
>>> smt.simplify(Pi([(x, Nat)], GE(x))[smt.Lambda([x], x)])
True

Parameters:

tele0 (Telescope)
B (SubSort)

Return type:

SubSort

kdrag.tele.Program(name: str, args: Telescope, T: SubSort, body: ExprRef)

Parameters:

name (str)
args (Telescope)
T (SubSort)
body (ExprRef)

class kdrag.tele.ProgramState(name: str, args: Telescope, T: SubSort, body: ExprRef)

Bases: ProofState

Interactive proof of a function definition. See https://rocq-prover.org/doc/master/refman/addendum/program.html

>>> n = kd.kernel.FreshVar("n", smt.IntSort())
>>> m = smt.Int("m")
>>> l = Program("test_inc1", [(n,Nat)], Pos, n + 1)
>>> l.define()
test_inc1

Parameters:

name (str)
args (Telescope)
T (SubSort)
body (ExprRef)

__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)

property ctx

cvc5(by=[], admit=False)

Call cvc5 to see if the current goal is solvable. Currently a sanity check only.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p, p))
>>> l.cvc5()
cvc5 proved the goal
[] ?|= Implies(p, p)

define()

emt(): Use egraph based equality modulo theories to simplify the goal. >>> x, y, z, w = smt.Ints(“x y z w”) >>> l = Lemma(smt.Implies(x + y + 1 == z, x + y + 1 == w)) >>> l.intros() [x + y + 1 == z] ?|= x + y + 1 == w >>> l.emt() [x + y + 1 == z] ?|= z == w

eq(rhs: ExprRef, **kwargs)

replace rhs in equational goal

Parameters:: rhs (ExprRef)

esolve() → dict[Expr, Expr]

Solve an exists goal using sympy. Returns a dictionary mapping from variables to solutions.

>>> x,y = smt.Reals("x y")
>>> l = Lemma(smt.Exists([x], x + y**2 == 1))
>>> l.esolve()
{X!...: 1 - y**2}

Return type:: dict[Expr, Expr]

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

goals: list[Goal | LemmaCallback]

have(conc0: BoolRef | str, **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
>>> l.have("x > 42")
[x > 0, x > -1] ?|= x > 42

Parameters:: conc0 (BoolRef | str)
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

lemmas: list[dict[int, Proof]]

newgoal(newgoal: BoolRef, **kwargs)

Try to show newgoal is sufficient to prove current goal

Parameters:: newgoal (BoolRef)

obtain(n: int | QuantifierRef) → ExprRef | list[ExprRef]

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

>>> x,y = smt.Ints("x y")
>>> l = Lemma(smt.Implies(smt.Exists([x], x * x == y), y >= 0))
>>> l.intros()
[Exists(x, x*x == y)] ?|= y >= 0
>>> _x = l.obtain(0)
>>> l
[x!...] ; [x!...*x!... == y] ?|= y >= 0
>>> l = Lemma(smt.Implies(smt.Exists([x], x * x == y), y >= 0))
>>> _ = l.intros()
>>> _x = l.obtain(smt.Exists([x], x * x == y))

Parameters:: n (int | QuantifierRef)
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))
>>> db = kd.utils.lemma_db()
>>> res = l.search()
>>> ("kdrag.theories.nat.add_Z", nat.add_Z) in res
True
>>> ("kdrag.theories.nat.add_S", nat.add_S) in res
False
>>> ("kdrag.theories.nat.add_S", nat.add_S) in l.search(nat.add,db=db)
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

solve(*vs) → dict[Expr, Expr]

Solve for variables using the context

>>> x,y,z = smt.Reals("x y z")
>>> l = Lemma(smt.Implies(smt.And(x + y == 10, y + z == 4), True))
>>> _ = l.intros()
>>> _ = l.split(at=0)
>>> l.solve(x,z)
{x: 10 - y, z: 4 - y}

Return type:: dict[Expr, Expr]

specialize(n: int | QuantifierRef, *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

Parameters:: n (int | QuantifierRef)

splintro()

Split and intro on a conjunction in the goal.

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

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

symp() → Expr

Use sympy to simplify the current goal. Does not mutate the goal. Returns the sympy expression.

>>> x,y,z = smt.Reals("x y z")
>>> l = Lemma(smt.ForAll([x,y], x**2 + 2*x*y + y**2 == (x + y)**2))
>>> _ = l.fixes()
>>> l.symp()
True

Return type:: Expr

top_goal() → Goal

Return type:: Goal

unfold(*decls: FuncDeclRef, at=None, keep=False) → 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

vampire(by=[], admit=False)

Call vampire to see if the current goal is solvable. Currently a sanity check only.

>>> p,q = smt.Bools("p q")
>>> l = Lemma(smt.Implies(p, p))
>>> l.vampire()
...
Vampire proved the goal
[] ?|= Implies(p, p)

type kdrag.tele.SubSort = FuncRef

kdrag.tele.TExists(xs: Telescope, P: BoolRef) → BoolRef

Dependent exists quantifier for a telescope of variables. Kind of like a proof irrelevant Sigma type.

Subtype / Refinement style usage

>>> x, y, z = smt.Reals("x y z")
>>> TExists([(x, x > 0), (y, y > x)], y > -1)
Exists(x, And(x > 0, Exists(y, And(y > x, y > -1))))

“Dependent type” style usage

>>> Pos = smt.Lambda([x], x > 0)
>>> GT = lambda x: smt.Lambda([y], y > x)
>>> TExists([(x, Pos), (y, GT(x))], y > -1)
Exists(x, And(x > 0, Exists(y, And(y > x, y > -1))))

Parameters:

xs (Telescope)
P (BoolRef)

Return type:

BoolRef

kdrag.tele.TForAll(xs: Telescope, P: BoolRef) → BoolRef

Dependent forall quantifier for a telescope of variables. Kind of like a proof irrelevant Pi type.

Subtype / Refinement style usage

>>> x, y, z = smt.Reals("x y z")
>>> TForAll([(x, x > 0), (y, y > x)], y > -1)
ForAll(x, Implies(x > 0, ForAll(y, Implies(y > x, y > -1))))

“Dependent type” style usage

>>> Pos = smt.Lambda([x], x > 0)
>>> GT = lambda x: smt.Lambda([y], y > x)
>>> TForAll([(x, Pos), (y, GT(x))], y > -1)
ForAll(x, Implies(x > 0, ForAll(y, Implies(y > x, y > -1))))

Parameters:

xs (Telescope)
P (BoolRef)

Return type:

BoolRef

type kdrag.tele.Telescope = list[tuple[ExprRef, BoolRef] | tuple[ExprRef, SubSort] | ExprRef]

type kdrag.tele.Type = SubSort

User telescope type.

Telescopes are dependent or refined contexts of variables. They can tag variables with SubSet expressions or formulas that involve the bound variable. Internally, the are normalized to _Tele, which is a list of (variable, formula) pairs.

kdrag.tele.ann(x: ExprRef, T: SubSort) → ExprRef

Annotate an expression with a type.

>>> x = smt.Int("x")
>>> ann(x, Nat)
ann(x, Lambda(n, n >= 0))

Parameters:

x (ExprRef)
T (SubSort)

Return type:

ExprRef

kdrag.tele.axiom_sig(f: FuncDeclRef, tele0: Telescope, T: SubSort) → Proof

Assign signature to a function f with a telescope of arguments tele0 as an axiom

Parameters:

f (FuncDeclRef)
tele0 (Telescope)
T (SubSort)

Return type:

Proof

kdrag.tele.define(name: str, args: Telescope, T: SubSort, body: ExprRef, by=None, **kwargs) → FuncDeclRef

Define a function with a precondition given by a telescope of arguments and a postcondition given by a subset that output will lie in.

Automatically

>>> n = kd.kernel.FreshVar("n", smt.IntSort())
>>> m = smt.Int("m")
>>> inc = define("test_inc", [(n,Nat)], Pos, n + 1)
>>> inc.pre_post
|= ForAll(n!...,
    Implies(And(n!... >= 0),
        Lambda(n, n > 0)[test_inc(n!...)]))
>>> pred = define("pred", [(n, Pos)], Nat, n - 1)
>>> myid = define("myid", [(n, Nat)], Nat, pred(inc(n)))

Parameters:

name (str)
args (Telescope)
T (SubSort)
body (ExprRef)

Return type:

FuncDeclRef

kdrag.tele.has_type(ctx: Telescope, t0: ExprRef, T: SubSort, by=None, **kwargs) → Proof

Tactic to check that an expression t0 has type T in a context ctx.

>>> x = smt.Int("x")
>>> Nat = smt.Lambda([x], x >= 0)
>>> has_type([(x, Nat)], x+1, Nat)
|= Implies(And(x >= 0), Lambda(x, x >= 0)[x + 1])

Parameters:

ctx (Telescope)
t0 (ExprRef)
T (SubSort)

Return type:

Proof

kdrag.tele.normalize(xs: Telescope) → _Tele

Normalize a telescope to a list of (variable, formula) pairs.

>>> x, y, z = smt.Ints("x y z")
>>> normalize([x, y, z])
[(x, True), (y, True), (z, True)]
>>> normalize([(x, x > 0), (y, y > x), z])
[(x, x > 0), (y, y > x), (z, True)]
>>> normalize([(x, smt.Lambda([x], x > 0)), (y, smt.Lambda([y], y > x)), z])
[(x, x > 0), (y, y > x), (z, True)]

Parameters:: xs (Telescope)
Return type:: _Tele

kdrag.tele.open_binder(e: BoolRef, n: int = 100000) → tuple[_Tele, BoolRef]

Open a formula in telescope form forall x, P(x), forall y, Q(y), R

>>> x, y = smt.Ints("x y")
>>> open_binder(TForAll([(x, x > 0), (y, y > 0)], x == y))
([(X!..., X!... > 0), (Y!..., Y!... > 0)], X!... == Y!...)
>>> open_binder(TForAll([(x, x > 0), (y, y > 0)], x == y), n=1)
([(X!..., X!... > 0)], ForAll(y, Implies(y > 0, X!... == y)))

Parameters:

e (BoolRef)
n (int)

Return type:

tuple[_Tele, BoolRef]

kdrag.tele.prove_sig(f: FuncDeclRef, tele0: Telescope, T: SubSort, by=None) → Proof

Parameters:

f (FuncDeclRef)
tele0 (Telescope)
T (SubSort)

Return type:

Proof

kdrag.tele.subsort_domain(T: SubSort) → SortRef

Get the domain sort of a SubSort, which is either an ArrayRef or a QuantifierRef.

>>> T = smt.Array("T", smt.IntSort(), smt.BoolSort())
>>> subsort_domain(T)
Int
>>> x = smt.Int("x")
>>> subsort_domain(smt.Lambda([x], x > 0))
Int

Parameters:: T (SubSort)
Return type:: SortRef