InnerExpr

class proveit.InnerExpr(top_level, inner_expr_path=(), assumptions=None)

Bases: object

Represents an “inner” sub-expression of a particular “top_level” Expression or Judgment. The inner_expr method of the Expression (or Judgment) class will start an InnerExpr with that particular expression (or judgment) as the top-level. This acts as an expression wrapper, starting at the top-level but can “descend” to any sub-expression (or the ‘assumptions’ in the Judgment case) via accessing sub-expression attributes (or ‘assumptions’). This will allow us to manipute the inner expression in the theory of the containing Expression/Judgment object. One can change the style of the inner expression or replace it with an equivalent form.

Equivalence methods may be registered via InnerExpr.register_equivalence_method(…). Registering an equivalence method allows one to directly replace the inner expression with a form that is produced by calling the equivalence method. Examples are:

evaluation, simplification, commutation, association, etc.

When registering such a method, a noun form (as above), a past tense form, and an action form are to be simplied (e.g., ‘evaluation’, ‘evaluated’, and ‘evaluate’). Calling the first version (e.g., ‘evaluation’) will produce a proven equality between the original top-level expression and a form in which the inner expression is replaced with its new form. Calling the second version (e.g., ‘evaluated’) will prove the equality as before but simply return the right side (the new form of the top-level, with the inner expression replaced). The last version (e.g., ‘evaluate’) is to be applied to proven (or easilty provable) top-level expressions and will yield the proven top-level expression (under given assumptions) with the inner expression replaced by its equivalent form.

For example, let “expr = [((a - 1) + b + (a - 1)/d) < e]”, and let “inner_expr = expr.inner_expr().lhs.terms[2].numerator”. Then

1. inner_expr.repl_lambda() will return _x_ -> [((a - 1) + b + _x_/d) < e], replacing the particular inner expression. (note that the second “a - 1” is singled out, distinct from the first “a - 1” because the subexpr object tracks the sub-expression by “location”).

2. inner_expr.with… will return an expression that is the same but with an altered style for the inner expression part. The InnerExpr class looks specifically for attributes of the inner expression class that start with ‘with’ and assumes they function to alter the style.

3. inner_expr.commutation(0, 1) would return:

   |- [((a - 1) + b + (a - 1)/d) < e]

   = [((a - 1) + b + (-1 + a)/d) < e]

   assuming ‘a’ is known to be a number.

4. inner_expr.commuted(0, 1) would return:

   [((a - 1) + b + (-1 + a)/d) < e]

   assuming ‘a’ is known to be a number. It will prove #3 along the way.

5. inner_expr.commute(0, 1) would return

   |- ((a - 1) + b + (-1 + a)/d) < e

   assuming the original expr may be proven via automation and ‘a’ is known to be a number.

6. inner_expr.substitution(a + 1 - 2) would return

   |- [((a - 1) + b + (a - 1)/d) < e]

   = [((a - 1) + b + (a + 1 - 2)/d) < e]

7. inner_expr.substitute(a + 1 - 2) would return

   |- [((a - 1) + b + (a + 1 - 2)/d) < e]

Note: When substitituting, auto-simplification may only affect sub-expressions touched by a substitution.

In addition, the InnerExpr class has ‘simplify_operands’ and ‘evaluate_operands’ methods for effecting ‘simplify’ or ‘evaluate’ (respectively) on all of the operands of the inner expression.

Methods Summary

cur_sub_expr(self)
repl_lambda(self[, params_of_param])	Returns the lambda function/map that would replace this particular inner expression within the top-level expression.
substitute(self, equality_or_replacement, …)	Substitute the replacement in place of the inner expression and return a new proven statement (assuming the top level expression is proven, or can be proven automatically).
substitution(self, equality_or_replacement, …)	Equate the top level expression with a similar expression with the inner expression replaced by the replacement.

Methods Documentation

cur_sub_expr(self)

repl_lambda(self, params_of_param=None)

Returns the lambda function/map that would replace this particular inner expression within the top-level expression.

substitute(self, equality_or_replacement, \*\*defaults_config)

Substitute the replacement in place of the inner expression and return a new proven statement (assuming the top level expression is proven, or can be proven automatically).

equality_or_replacement may be a proven equality with the current inner expression on the left side or it may be the replacement.

Note: auto-simplification may only affect sub-expressions touched by the substitution.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

substitution(self, equality_or_replacement, \*\*defaults_config)

Equate the top level expression with a similar expression with the inner expression replaced by the replacement.

equality_or_replacement may be a proven equality with the current inner expression on the left side or it may be the replacement.

Note: auto-simplification may only affect sub-expressions touched by the substitution.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘substituted’ returns the right-hand side of ‘substitution’. ‘substitute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘substitution’ for the inner expression.