kdrag.theories.real.seq

Module Attributes

cumsum_smul	cumsum_comm = cumsum(lambda x, cumsum(lammbda y, a[x,y]) ) ???
cauchy_mod	is_convergent = kd.define(

Functions

test()

Classes

Series()

class kdrag.theories.real.seq.Series

Bases: object

powers = powers

kdrag.theories.real.seq.cauchy_mod = cauchy_mod

is_convergent = kd.define(

“is_convergent”, [a], kd.QForAll(

[eps], eps > 0, smt.Exists(

[N], kd.QForAll([m], m > N, smt.Exists([x], real.abs(a[m] - x) < eps))

),

),

)

kdrag.theories.real.seq.cumsum_smul = |= ForAll([a, x],        cumsum(RSeq.smul(x, a)) == RSeq.smul(x, cumsum(a)))

cumsum_comm = cumsum(lambda x, cumsum(lammbda y, a[x,y]) ) ???

# TODO: unstable @kd.Theorem(

“forall (a : RSeq) (x : Real) (n : Int), cumsum (smul x a) n = smul x (cumsum a) n”

) def cumsum_smul(l):

a, x, n = l.fixes() l.induct(n)

# n < 0 # TODO: These induction cases look disgusting with too many lambdas. l.fix() l.simp() l.intros() l.unfold(cumsum, smul) l.simp() l.auto(by=[smul.defn, cumsum.defn])

# n == 0 l.auto(by=[smul.defn, cumsum.defn])

# n > 0 l.fix() l.simp() l.unfold(cumsum, smul) l.simp() l.unfold(cumsum, smul) l.simp() l.auto(by=[smul.defn, cumsum.defn])

Type:

# TODO

Parameters:

args (smt.ExprRef | Proof)

kdrag.theories.real.seq.test()

>>> True
True