kdrag.property

Generic properties like associativity, commutativity, idempotence, etc.

Functions

`assoc_comm`(f)
`assoc_norm`(e[, trace])
`comm_norm`(e[, trace])
`idem_norm`(e[, trace])

Classes

`Antisymm`(args, *kwargs)	forall x y, rel(x, y) and rel(y, x) implies x = y
`Assoc`(args, *kwargs)	forall x y z, f(f(x,y),z) = f(x,f(y,z))
`Asymm`(args, *kwargs)	forall x y, rel(x, y) implies not rel(y, x)
`Comm`(args, *kwargs)	forall x y, f(x,y) = f(y,x)
`GenericProof`(f)	GenericProof is a dictionary of proofs indexed on meta (python) information.
`Idem`(args, *kwargs)	forall x, f(x,x) = x
`Identity`(args, *kwargs)
`Irrefl`(args, *kwargs)	forall x, not rel(x, x)
`LeftIdentity`(args, *kwargs)	forall x, f(e,x) = x
`Refl`(args, *kwargs)	forall x, rel(x, x)
`RightIdentity`(args, *kwargs)	forall x, f(x,e) = x
`Total`(args, *kwargs)	forall x y, rel(x, y) or rel(y, x)
`TypeClass`(*L)	Subclass this to define a typeclass.

class kdrag.property.Antisymm(*args, **kwargs)

Bases: Protocol

forall x y, rel(x, y) and rel(y, x) implies x = y

antisymm: Proof

rel: FuncDeclRef

class kdrag.property.Assoc(*args, **kwargs)

Bases: Protocol

forall x y z, f(f(x,y),z) = f(x,f(y,z))

assoc: Proof

f: FuncDeclRef

class kdrag.property.Asymm(*args, **kwargs)

Bases: Protocol

forall x y, rel(x, y) implies not rel(y, x)

asymm: Proof

rel: FuncDeclRef

class kdrag.property.Comm(*args, **kwargs)

Bases: Protocol

forall x y, f(x,y) = f(y,x)

comm: Proof

f: FuncDeclRef

class kdrag.property.GenericProof(f)

Bases: object

GenericProof is a dictionary of proofs indexed on meta (python) information.

Because z3 and hence knuckledragger does not have strong generic support inside its logic, we can borrow a bit of python to parametrize theorems over other data or over sorts.

This has some of the flavor of single dispatch.

It is similar to an axiom schema is some respects (in usage it takes in python data and outputs a kd.Proof) except that one must register the theorems as proven by other means.

It is a way to refer to a collection of similar proofs akin to single entry typeclasses or modules in other theorem proving systems.

>>> x = lambda T: smt.Const("x", T)
>>> obvious = GenericProof(lambda T: smt.ForAll([x(T)], x(T) == x(T)) )
>>> obvious.lemma(smt.IntSort(), by=[])
>>> R = smt.RealSort()
>>> obvious.register(R, kd.prove(smt.ForAll([x(R)], x(R) == x(R))))

get(*args) → Proof | None

Return type:: Proof | None

lemma(*args, **kwargs)

register(*args)

class kdrag.property.Idem(*args, **kwargs)

Bases: Protocol

forall x, f(x,x) = x

f: FuncDeclRef

idem: Proof

class kdrag.property.Identity(*args, **kwargs)

Bases: LeftIdentity, RightIdentity, Protocol

e: ExprRef

f: FuncDeclRef

left_id: Proof

right_id: Proof

class kdrag.property.Irrefl(*args, **kwargs)

Bases: Protocol

forall x, not rel(x, x)

irrefl: Proof

rel: FuncDeclRef

class kdrag.property.LeftIdentity(*args, **kwargs)

Bases: Protocol

forall x, f(e,x) = x

e: ExprRef

f: FuncDeclRef

left_id: Proof

class kdrag.property.Refl(*args, **kwargs)

Bases: Protocol

forall x, rel(x, x)

refl: Proof

rel: FuncDeclRef

class kdrag.property.RightIdentity(*args, **kwargs)

Bases: Protocol

forall x, f(x,e) = x

e: ExprRef

f: FuncDeclRef

right_id: Proof

class kdrag.property.Total(*args, **kwargs)

Bases: Protocol

forall x y, rel(x, y) or rel(y, x)

rel: FuncDeclRef

total: Proof

class kdrag.property.TypeClass(*L)

Bases: object

Subclass this to define a typeclass. The class itself holds a registry of information The key can be any valid Python key, but the expected types are smt.ExprRef and smt.FuncDeclRef. When you instantiate the class as usual, you hand the key to the constructor and the class will look up the information in the registry and populate the fields in the returned instance . look up the information in the registry and populate the fields in the returned instance. See https://okmij.org/ftp/ML/canonical.html for more on the programmatic approach to typeclasses.

>>> class Monoid(TypeClass):
...     def check(self, T):
...         assert isinstance(self.mappend, smt.FuncDeclRef) and self.mappend.arity() == 2
...         assert isinstance(self.mempty, smt.ExprRef)
...         assert self.mappend.domain(0) == self.mappend.domain(1) == self.mempty.sort() == self.mappend.range()
...
>>> x = smt.Int("x")
>>> Monoid.register(smt.IntSort(), mappend=(x + x).decl(), mempty=smt.IntVal(0))
>>> Monoid(smt.IntSort())
Monoid({'key': (Int,), 'mappend': +, 'mempty': 0})

assert_eq(a, b)

classmethod get_registry() → dict

Return type:: dict

classmethod lookup(*L)

classmethod register(*L, **kwargs)

kdrag.property.assoc_comm(f: FuncDeclRef) → Proof

Parameters:: f (FuncDeclRef)
Return type:: Proof

kdrag.property.assoc_norm(e: ExprRef, trace=None) → ExprRef

>>> T = smt.DeclareSort("T")
>>> x, y, z,w = smt.Ints("x y z w")
>>> assoc_norm((x + y) + (z + w)).eq(x + (y + (z + w)))
True

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

kdrag.property.comm_norm(e: ExprRef, trace=None) → ExprRef

>>> x,y = smt.Ints("x y")
>>> assert comm_norm(y + x).eq(x + y)

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

kdrag.property.idem_norm(e: ExprRef, trace=None) → ExprRef

>>> idem_norm(smt.And(a, smt.And(a, a)))
a

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