Welcome to Prove-It’s documentation!

proveit Package

Functions

asExpression(truthOrExpression) Return the argument as Expressions.
asExpressions(*truthOrExpressions) Return the arguments as a list of Expressions via asExpression.
compositeExpression(expressions) Put the appropriate CompositeExpression wrapper around expressions.
expressionDepth(expr) Returns the depth of the expression tree for the given expression.
maybeFenced(formatType, innerFormatted, **kwargs) Return the innerFormatted string/latex iff kwargs[‘fence’]=True.
maybeFencedLatex(innerLatex, **kwargs) Return innerLatex, wrapped in parentheses iff kwargs[‘fence’]==True.
maybeFencedString(innerStr, **kwargs) Return innerStr, wrapped in parentheses iff kwargs[‘fence’]==True.
reset() Clear all references to Prove-It information.
safeDefaultOrDummyVar(defaultVar, *expressions)
safeDummyVar(*expressions)
singleOrCompositeExpression(exprOrExprs) Put the approriate CompositeExpression wrapper around a list (iterable) or dictionary of Expressions, or simply return the given Expression if it is one.
varIter(var, start, end)

Classes

Assumption(expr[, assumptions])
Axiom(expr, context, name)
Composite The base class for NamedExprs, ExprList, and ExprTensor.
Context([path]) A Context object provides an interface into the __pv_it database for access to the common expressions, axioms, theorems and associated proofs of a Prove-It context.
ContextException(message)
DuplicateLiteralError(message)
ExprList(*expressions) An ExprList is a composite expr composed of an ordered list of member Expressions.
ExprListError(msg)
ExprTensor(tensor[, shape, styles, …]) An ExprTensor is a composite Expression representing an n-dimensional tensor.
Expression(coreInfo[, subExpressions, …])
Function(operator, operand_or_operands[, …]) A Function is an Operation with a default format as a function: f(x), Q(x, y), etc.
Generalization(instanceTruth, newForallVarLists)
GeneralizationFailure(expr, assumptions, message)
HypotheticalReasoning(consequentTruth, …)
ImproperRelabeling(message)
ImproperSubstitution(message)
Indexed(var, index_or_indices[, base, …]) An Indexed Expression expresses a Variable, representing an ExprList or ExprTensor, being indexed to yield an element.
IndexedError(msg)
InnerExpr(topLevelExpr[, innerExprPath]) Represents an “inner” sub-expression of a particular “topLevel” expression.
InvalidAssumptions()
Iter(parameter_or_parameters, body, …[, …]) An Iter Expression represents an iteration of Expressions to be inserted into a containing composite Expression.
KnownTruth(expression, assumptions)
Label(stringFormat[, latexFormat, …]) Label is the base class for the Variable, Literal, and MultiVariable expr classes (Label is not itself an expr class).
Lambda(parameter_or_parameters, body[, …]) A lambda-function Expression.
LambdaError(message)
Literal(stringFormat[, latexFormat, …]) A Literal expresses contextual meaning.
MakeNotImplemented(exprSubClass)
ModusPonens(implicationExpr[, assumptions])
ModusPonensFailure(expr, assumptions, message)
NamedExprs(items[, styles, requirements]) An NamedExprs is a composite expr that maps strings to Expressions.
Operation(operator_or_operators, …[, …])
OperationError(message)
OperationOverInstances(operator, …[, …]) OperationOverInstances description: TODO
OperationSequence(operators, operands[, …])
ParameterExtractionError(specifics)
Proof(provenTruth, requiredTruths)
ProofFailure(expr, assumptions, message)
RelabelingFailure(expr, assumptions, message)
ScopingViolation(message)
Specialization(generalTruth, …[, …])
SpecializationFailure(expr, assumptions, message)
StyleOptions(expr) An Object for displaying the valid style options of an Expression.
Theorem(expr, context, name)
TransitiveRelation(operator, lhs, rhs) Base class for generic transitive relations.
TransitiveSequence(operators, operands[, …]) Base clase for Operation Expressions that represent a sequence of transitive relationships.
Variable(stringFormat[, latexFormat]) A Variable is an interchangeable label.

proveit.logic Package

Functions

compose(expressions[, assumptions]) Returns [A and B and …], the And operator applied to the collection of given arguments, derived from each separately.
concludeViaImplication(consequent, assumptions) Perform a breadth-first search of implications going in reverse from the consequent until reaching an antecedent that has been proven.
defaultSimplification(innerExpr[, inPlace, …]) Default attempt to simplify the given inner expression under the given assumptions.
evaluateTruth(expr, assumptions) Attempts to prove that the given expression equals TRUE under the given assumptions via proving the expression.
inBool(*elements)
isIrreducibleValue(expr)
reduceOperands(innerExpr[, inPlace, …]) Attempt to return an InnerExpr object that is provably equivalent to the given innerExpr but with simplified operands at the inner-expression level.

Classes

And(*operands)
Card(domain)
Difference(A, B)
Disjoint(*sets) The Disjoint operation defines a property for a collection of sets.
Distinct(*elements) The Distinct operation defines a property for any collection.
Equals(a, b)
EvaluationError(message)
Exists(instanceVarOrVars, instanceExpr[, …])
Forall(instanceVarOrVars, instanceExpr[, …])
Iff(A, B)
Implies(antecedent, consequent)
InSet(element, domain)
Intersect(*operands)
IrreducibleValue()
Membership(element)
Nonmembership(element) Base class for any ‘nonmembership object’ return by a domain’s ‘nonmembershipObject’ method.
Not(A)
NotEquals(a, b)
NotExists(instanceVarOrVars, instanceExpr[, …])
NotInSet(element, domain)
NotSubsetEq(subset, superset)
NotSupersetEq(superset, subset)
Or(*operands)
Set(*elems) Defines a set with only one item.
SetOfAll(instanceVarOrVars, instanceElement)
Subset(subset, superset)
SubsetEq(subset, superset)
Superset(superset, subset)
SupersetEq(superset, subset)
Union(*operands)

proveit.number Package

Functions

Frac(numer, denom)
GreaterEqOnlySeq(*operands)
GreaterOnlySeq(*operands)
LessEqOnlySeq(*operands)
LessOnlySeq(*operands)
greaterSequence(operators, operands) Create a GreaterSequence with the given operators or operands, or create an appropriate degenerate Expression when there are fewer than two operators.
isLiteralInt(expr)
lesserSequence(operators, operands) Create a LessSequence with the given operators or operands, or create an appropriate degenerate Expression when there are fewer than two operators.
num(x)

Classes

Abs(A)
Add(*operands)
Ceil(A)
DecimalSequence(*digits)
Div(operandA, operandB)
Exp(base, exponent)
Floor(A)
Greater(lhs, rhs)
GreaterEq(lhs, rhs)
GreaterSequence(operators, operands)
Integrate(index, integrand, domain[, conditions])
Interval(lowerBound, upperBound)
IntervalCC(lowerBound, upperBound)
IntervalCO(lowerBound, upperBound)
IntervalOC(lowerBound, upperBound)
IntervalOO(lowerBound, upperBound)
Len(operand)
Less(lhs, rhs)
LessEq(lhs, rhs)
LesserSequence(operators, operands)
Max(*operands)
Min(*operands)
Mod(dividend, divisor)
ModAbs(value, divisor)
Mult(*operands)
Neg(A)
Numeral(n[, stringFormat, latexFormat])
RealInterval(operator, lowerBound, upperBound) Base class for all permutations of closed and open intervals.
Round(A)
Sqrt(base)
Subtract(operandA, operandB)
Sum(indexOrIndices, summand[, domain, …])

Indices and tables