Welcome to Prove-It’s documentation!¶
proveit Package¶
Functions¶
|
Return the argument as Expressions. |
|
Return the arguments as a list of Expressions via as_expression. |
|
|
|
|
|
|
|
Given a nested OperationOverInstances, derive or equate an |
|
Put the appropriate CompositeExpression wrapper around expressions. |
|
@equality_prover works the same way as the @relation_prover decorator except that it also registers the “equality method” in InnerExpr with the past tense and present tense names. |
|
Returns the depth of the expression tree for the given expression. |
|
Given an ExprTuple of only IndexedVar and ExprRange entries, returns an ExprTuple of just the corresponding indices (including ranges of indices and nested ranges of indices). |
|
Return the dictionary mapping Variables to forms w.r.t. ranges of indices (or solo) in which the variable occurs as free (not within a lambda map that parameterizes the base variable). Examples of “forms”: x x_i x_1, …, x_n x_{i, 1}, …, x_{i, n_i} x_{1, 1}, …, x_{1, n_1}, ……, x_{m, 1}, …, x_{m, n_m} For example, (x_1, …, x_n) -> x_1 + … + x_n + x_{n+1} would report {x_{n+1}} for the x entry but not x_1, …, x_n. In another example, (x_1, …, x_n) -> x_1 + … + x_k + x_{k+1} + … + x_{n} would report {x_1, …, x_k, x_{k+1}, …, x_{n}} for the x entry because the masking is not “explicit” and actually depends upon what may be assumed about k. |
|
Returns the set of variables for that are free (unbound) in the given expression. For example, given (x_1, …, x_n) -> x_1 + … + x_{m} n is free. Even though there is ambiguity about the range of indices of x on the right versus the left without knowing m relative to n, lambda maps in Prove-It are not allowed to partially mask a range of parameters (in this example, m>n is not allowed). However, this restriction isn’t enforced until it really matters. When the ranges of x are relabeled or instantiated, then Prove-It will check that this restriction is satisfied. Axioms and theorems must not have any variables that are entirely free. |
|
Yield the InnerExpr objects that represent ‘inner’ as an inner expression of ‘expr’. |
|
|
|
Return the inner_formatted string/latex iff kwargs[‘fence’]=True. |
|
Return inner_latex, wrapped in parentheses iff kwargs[‘fence’]==True. |
|
Return inner_str, wrapped in parentheses iff kwargs[‘fence’]==True. |
|
@prover is a decorator for methods that are to return a proven judgment valid under “active” (default) assumptions. |
|
@relation_prover is a decorator for methods that are to return a proven judgment valid under “active” (default) assumptions, is a Relation type Expression, and has the original expression (self or self.expr) on the left hand side. |
|
Clear all references to Prove-It information. |
|
|
|
Return a dummy variable that isn’t contained in any of the given expression and not contained in any of the default assumptions. |
|
|
|
|
|
|
|
Put the approriate CompositeExpression wrapper around a list (iterable) or dictionary of Expressions, or simply return the given Expression if it is one. |
|
Return a conjunction of relations in the total ordering style. |
A simple algorithm to yield all inner expressions of an expression, including the expression itself. |
|
|
Given a nested OperationOverInstances, derive or equate an |
|
Return all of the used Literals of this Expression, included those in sub-expressions. |
|
Return all of the used Variables of this Expression, included those in sub-expressions. |
|
|
|
|
|
Classes¶
|
|
|
|
|
|
The base class for NamedExprs, ExprTuple, and ExprArray. |
|
|
A Composition is an Expression that represents the composition of functions (lambda maps). |
|
A Conditional expression is one that may reduce to its ‘value’ if and only if its ‘condition’ evaluates to TRUE. |
|
|
|
|
|
|
|
An ExprArray represents a 2-dimensional array. |
|
An ExprRange expression represents a range of “element” expressions within a containing ExprTuple. |
|
An ExprTuple is a composite Expression composed of an ordered list of member Expression “entries”. |
|
|
|
|
|
A Function is an Operation that will format as a function: f(x), Q(x, y), etc. |
|
|
|
|
|
|
|
An IndexedVar Expression expresses a Variable or nested IndexedVar, representing an ExprTuple (or ExprArray which is really just an ExprTuple of ExprTuples), being indexed to yield an element. The indices are typically parameters of containing ExprRanges, or additively shifted versions of such parameters. For example, (x_{1, 1+1} + … + x_{1, j+1} + … + x_{1, n+1}) * … * (x_{i, 1+1} + … + x_{i, j+1} + … + x_{i, n+1}) * … * (x_{m, 1+1} + … + x_{m, j+1} + … + x_{m, n+1}) is represented by a doubly-nested ExprRange using the IndexedVar x_{i, j+1}. |
|
Represents an “inner” sub-expression of a particular “top_level” Expression or Judgment. |
|
Iterator for InnerExpr objects of a given top-level expression. |
|
An Instantiation proof step eliminates some number of nested Forall operations and simultaneously replaces Variables with Expressions according to the replacement map (repl_map). |
|
|
|
|
|
Label is the base class for the Variable, Literal, and Multi_variable expr classes (Label is not itself an expr class). |
|
A lambda-function Expression. |
|
|
|
A Literal expresses contextual meaning. |
|
|
|
|
|
|
|
An NamedExprs is a composite expr that maps strings to Expressions. |
|
|
|
|
|
OperationOverInstances description: TODO |
|
|
Lambda’s are not allowed to mask a range of parameters while the body contains parameters outside of this range (partial masking). |
|
|
|
|
|
|
|
|
|
|
SimplificationDirectives are used to specify the directives to use during simplification (or shallow_simplification) that are particular to each Expression class. |
|
An Object for displaying the valid style options of an Expression. |
|
|
|
A Theory object provides an interface into the __pv_it database for access to the common expressions, axioms, theorems and associated proofs of a Prove-It theory. |
|
|
|
Used in __init__.py modules of theory packages for accessing common expressions, axioms, and theorems of the package. |
|
Transitive relation updater: A convenient class for updating a transitive relation (equality, less, subset, etc.) by adding relations that modify the relation via transitivity. |
|
Base class for generic transitive relations. |
|
|
|
|
|
A Variable is an interchangeable label. |
|
An ExprArray represented in column-major order. |
proveit.core_expr_types Package¶
proveit.logic Package¶
Functions¶
|
Returns [A and B and …], the And operator applied to the collection of given arguments, derived from each separately. |
|
Perform a breadth-first search of implications going in reverse from the consequent until reaching an antecedent that has been proven. |
|
Prove and return that lhs=rhs or lhs≠rhs or raise an UnsatisfiedPrerequisites or NotImplementedError if neither of these is readily known. |
|
Attempts to prove that the given expression equals FALSE under the given assumptions via disproving the expression. |
|
Attempts to prove that the given expression equals TRUE under the given assumptions via proving the expression. |
|
Return a nontrivial evaluation of the given expression if possible; otherwise return a nontrivial simplification if possible. |
|
|
|
|
|
Return the expression representing (A not_proper_superset B), internally represented as (B not_proper_subset A) but with a style that reverses the direction. |
|
Return the expression representing (A not_superset_eq B), internally represented as (B not_subset_eq A) but with a style that reverses the direction. |
|
Return the expression representing (A superset B), internally represented as (B subset A) but with a style that reverses the direction. |
|
Return the expression representing (A superset_eq B), internally represented as (B subset_eq A) but with a style that reverses the direction. |
Classes¶
|
|
|
A set of functions from a domain to a codomain that are one-to-one and onto. |
|
|
|
|
|
CartExp represents an exponentiation of a set by a positive, natural number to denote repeated Cartesion products. |
|
A CartProd represents the Cartesian product of sets to produce a new set. |
|
|
|
Base class for any ‘nonmembership object’ return by a domain’s ‘nonmembership_object’ method. |
|
|
|
The Disjoint operation defines a property for a collection of sets. |
|
The Distinct operation defines a property for any collection. |
|
|
|
|
|
|
|
|
|
|
|
A set of functions from a domain to a codomain. |
|
|
|
Represents the image of a set under a function (operator) which is the set obtained by applying the function to each element of the original set. |
|
|
|
Class membership denotes a collection of mathmematical objects that satisfy a certain common property. |
|
Set membership is a special case of class membership, so we’ll derive from InClass for code re-use. |
|
A set of functions from a domain to a codomain that are one-to-one and onto. |
|
|
|
|
|
Represents a function (operator) that may be applied to a set or tuple (ordered set) for applying the inverse of a function to each element. |
|
|
|
|
|
|
|
NotInClass denotes the logical negation of class membership (see InClass). |
|
Set nonmembership is a special case of class nonmembership, so we’ll derive from NotInClass for code re-use. |
|
|
|
|
|
|
|
|
|
Class to represent proper subset relation, such as A proper_subset B, to represent the claim that any element in set A is also in set B, while B also has at least one element not in set A. |
|
Defines an enumerated set (i.e. |
|
Class to capture the membership equivalence of 2 sets A and B. |
|
|
|
|
|
Class to capture the LACK of membership equivalence of 2 sets A and B. |
|
|
|
|
alias of |
|
|
|
alias of |
|
|
A set of functions from a domain to a codomain that are one-to-one and onto. |
|
Used in __init__.py modules of theory packages for accessing common expressions, axioms, and theorems of the package. |
|
|
|
|
|
|
|
proveit.numbers Package¶
Functions¶
|
Given an expression, expr, of the complex number polar form, |
|
Return the expression representing a fraction making obvious simplifications if the denominator is one or if either/both the numerator/denominator are fractions. |
|
Return an expression representing the product of the given factors using obvious simplifications: return ‘one’ if there are no factors, return the single factor if there is only 1, return ‘zero’ if there are any zeros, and combine fractions. |
|
Prove that the Lambda-map specified by fxn is contained in the set of monotonically-decreasing functions defined over the domain. |
|
Prove that ‘expr’ is an Expression that respresents a number in the given ‘number_set’. |
|
Assuming a and b are numeric rationals, prove and return that a ≠ b. |
|
Prove the most restrictive standard number set membership of the given expression. |
|
Returns the distributed sum of expression. |
|
Returns the distributed a-b expression. |
|
|
|
|
|
|
|
Return an expression representing a > b, internally represented as b < a but with a style that reverses the direction. |
|
Return an expression representing a >= b, internally represented as b <= a but with a style that reverses the direction. |
|
Return True iff the ‘expr’ represents an explicit, numeric integer. |
|
Return True iff the ‘expr’ represents an explicit, numeric natural number. |
|
Return True iff ‘expr’ represents an explicit, numeric rational number (as a numeric integer or fraction of numeric integers with a nonzero denominator). |
|
Return True iff a ≤ b. |
Return True iff a ≤ b. |
|
|
Return True iff a < b. |
|
Return True iff a < b. |
|
Returns the negated form of this expression. |
Return True iff a and b are numeric rational expressions that are not equal to each other. |
|
|
|
|
Return a conjunction of number ordering relations with a total-ordering style; for example, a < b <= c = d < e |
|
Return the integer numerator and denominator of a numeric rational. |
|
Return a simplified version of this expression with a quick-n-dirty approach suitable for additively shifted and/or negated integer indices and nested versions thereof. |
|
Return True iff the ‘factor’ can obviously be factors out of ‘term’. |
|
Return the most restrictive number set that the given expression may readily be proven to be within. |
|
Return the portion of expr_A that remains after removing the factors that are in common with expr_B. |
|
Given a numerator and a denominator as integers, return an Expression of the equivalent irreducible rational. |
|
Special function for squaring root version of an exponential. |
|
Special function for square root version of an exponential. |
|
For the number set given_set (which might, for example, be a continuous interval, an integer interval, etc.), return the most restrictive number set (such as Real, RealPos, Integer, etc.) that is already known to contain the given_set, or return the original given_set if no such standard set inclusion is already known. |
|
Return the a-b expression (which is internally a+(-b)). |
|
Utility function to produce a minimal standard number set that contains all the given number sets, if possible. |
|
Given an expression, expr, of the complex number polar form, |
Classes¶
|
|
|
|
|
|
|
|
|
The complex conjugate of a + i b for real numbers a and b is equal to a - i b. |
|
|
|
|
|
(equivalently, x is a factor of y, y is a multiple of x, or y/x is an integer). |
|
DividesProper(x, y) represents the claim that x divides y (i.e. |
|
An Expression class to represent an exponentiation. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The Kronecker delta function of i and j is equal to 1 if i=j or equals 0 otherwise. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
MonDecFuncs denotes the set of monotonically-decreasing functions on some domain D and codomain C and is meant to capture and articulate properties of functions such as 1/x^2 on (0, infty). |
|
|
|
|
|
Base class for number operation (i.e. |
|
|
|
|
|
|
|
Base class for all permutations of closed and open intervals. |
|
|
|
|
|
Used in __init__.py modules of theory packages for accessing common expressions, axioms, and theorems of the package. |