import proveit
from proveit import (Lambda, ExprTuple, ExprRange, IndexedVar, safe_dummy_var,
defaults, Function, ProofFailure)
from proveit import A, a, b, f, g, i, j, k, l, m, n, x, y
from proveit.logic import Equals, NotEquals, Not, EvaluationError, InSet
from proveit.linear_algebra import TensorProd
from proveit.numbers import (zero, one, two, three, four, e as e_nat, Add, Exp,
Integer, Mult, Natural, NaturalPos, Neg, num, subtract)
from proveit.core_expr_types import Len
from proveit.core_expr_types import (
a_i_to_j, x_1_to_n, y_1_to_n, f_i_to_j, f_i_to_jp1)
from proveit.core_expr_types.tuples import (
len_of_ranges_with_repeated_indices_from_1, range_from1_len,
len_of_ranges_with_repeated_indices_from_1, len_of_ranges_with_repeated_indices,
len_of_empty_range_of_ranges)
from proveit.core_expr_types.tuples import general_range_of_ranges
%begin demonstrations
Equals(ExprTuple(a, b, x, y), ExprTuple(a, b, x, y)).prove()
ExprTuple(a, b, x, y).deduce_equal_or_not(ExprTuple(x, y))
ExprTuple(a, b, x, y).deduce_equal_or_not(
ExprTuple(x, b, x, y), assumptions=[NotEquals(a, x)])
defaults.assumptions = [InSet(n, NaturalPos)]
partitioned = x_1_to_n.partition(one, assumptions=[InSet(n, NaturalPos)])
eq = Equals(ExprTuple(*partitioned.lhs.entries, y),
ExprTuple(*partitioned.rhs.entries, y))
eq.prove(assumptions=[InSet(n, NaturalPos)])
shifted = x_1_to_n.shift_equivalence(new_start=zero, assumptions=[InSet(n, NaturalPos)])
eq = Equals(ExprTuple(*shifted.lhs.entries, y),
ExprTuple(*shifted.rhs.entries, y))
eq.lhs.inner_expr()[0].partition(one)
eq.lhs.deduce_equal(eq.rhs, assumptions=[InSet(n, NaturalPos)])
eq = Equals(ExprTuple(a, y, *partitioned.lhs.entries),
ExprTuple(a, y, *partitioned.rhs.entries))
eq.prove(assumptions=[InSet(n, NaturalPos)])
eq.lhs.deduce_equal(eq.rhs, assumptions=[InSet(n, NaturalPos)])
eq.lhs.map_elements(lambda x : Not(x))
ExprTuple.map_elements_together(lambda x, y : Equals(x, y), eq.lhs, eq.lhs)
For efficiency, this is limited: ExprRanges must be aligned
try:
ExprTuple.map_elements_together(lambda x, y : Equals(x, y), eq.lhs, eq.rhs)
assert False, "ValueError expected"
except ValueError as e:
print("Expected error:", e)
ExprRange(order='decreasing')
flag¶An ExprRange with the order='decreasing'
flag produces an ExprRange of the form f(i),...,f(j), where 0 <= (i-j) and j < i (i.e. the ExprRange represents 0 or more elements and is in decreasing order)
For example, if
self = $f(3),...,f(6)$,
then order='decreasing'
would return:
$|- f(6),...,f(3)$
test = ExprRange(i, IndexedVar(a, i), j, zero, order='decreasing')
inc_test = ExprRange(i, IndexedVar(a, i), j, zero)
try:
ExprRange(i, IndexedVar(a, i), two, zero, order='increasing')
assert False, "Expecting a ValueError; should not get this far!"
except ValueError as _e:
print("Expected exception: ", _e)
ExprRange(i, IndexedVar(a, i), two, zero, order='decreasing')
test.lambda_map
(test.start_index, test.end_index, test.true_start_index, test.true_end_index)
(inc_test.start_index, inc_test.end_index,
inc_test.true_start_index, inc_test.true_end_index)
test.body
inc_test.body
test.first()
inc_test.first()
test.last()
inc_test.last()
empty_test_inc = ExprRange(i, IndexedVar(a, i), one, zero, order='increasing')
empty_test_inc.reduction()
empty_test_dec = ExprRange(i, IndexedVar(a, i), zero, one, order='decreasing')
empty_test_dec.reduction()
empty_test_dec.lambda_map
partition_test_inc = ExprRange(i, IndexedVar(a, i), zero, four, order='increasing')
partition_test_inc.partition(two)
partition_test_dec = ExprRange(i, IndexedVar(a, i), four, zero, order='decreasing')
partition_test_dec.start_index, partition_test_dec.true_start_index
partition_test_dec.partition(two)
from proveit import fa
from proveit.numbers import Complex
assumptions = [InSet(Add(j, Neg(i), one), Natural),
InSet(i, Natural), InSet(j, Natural)]
f_i_to_j_dec = ExprRange(a, fa, i, j, order='decreasing')
from proveit.core_expr_types.tuples import negated_shift_equivalence
negated_shift_equivalence
# negated_shift_equivalence.instantiate({i:Neg(i), j:Neg(j), k:subtract(i, one), a:Neg(one), l:subtract(j, one)}, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
# # Natural), InSet(subtract(subtract(j, one), i),
# Natural)])
# f_i_to_j_dec.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
# Natural)])
# f_i_to_j__shift__eq_dec = \
# f_i_to_j_dec.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
# Natural)]).lhs.entries[0]
# assert False
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, zero), one, n)).computation(assumptions=[InSet(n, NaturalPos)])
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), two, n), one, zero)).computation(assumptions=[InSet(n, Natural)])
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, n), one, n)).computation(assumptions=[InSet(n, Natural), InSet(n, NaturalPos)])
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, zero), two, one)).computation(assumptions=[InSet(n, Natural)])
The following 5 cells have been commented out — they create and then depend on the one-element expr_range in the first cell, which returns an error
# expr_range = ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, one), one, one)
# lambda_map = Lambda((expr_range.parameter, expr_range.body.parameter), expr_range.body.body)
# singular_nested_range_reduction.instantiate({f:lambda_map, i:one, j:one, m:one})
# Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, one), one, one)).computation()
# Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, two), one, one)).computation()
assumptions = [InSet(Add(j, Neg(i), one), Natural),
InSet(i, Natural), InSet(j, Natural)]
f_i_to_jp1
eq = f_i_to_jp1.partition(j, assumptions=assumptions)
eq.rhs.merger(assumptions=assumptions)
f_i_to_j__shift__eq = \
f_i_to_j.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(Add(j, one), i),
Natural)])
f_i_to_j__shift__eq.rhs
Add(subtract(i, one), one).simplification(assumptions=[InSet(i, Integer)])
Add(Add(i, Neg(two)), two).simplification(assumptions=[InSet(i, Integer)])
Add(subtract(j, one), one).simplification(assumptions=[InSet(j, Integer)])
Add(subtract(j, two), two).simplification(assumptions=[InSet(j, Integer)])
f_i_to_j__shift__eq.rhs.entries[0].shift_equivalence(
old_shift=one, new_shift=two,
assumptions=[InSet(j, Integer), InSet(i, Integer),
InSet(subtract(j, subtract(i, one)), Natural)])
from proveit import fa
from proveit.numbers import Complex
f_i_to_j_dec = ExprRange(a, fa, i, j, order='decreasing')
assumptions = [InSet(Add(Neg(j), i, Neg(one)), Natural),
InSet(i, Natural), InSet(j, Natural)]
#InSet(Neg(Add(x, one)), Complex).prove(assumptions=[InSet(x, Complex)])
Neg(Add(Neg(Add(x, one)), one)).distribution(assumptions=[InSet(x, Complex)])
InSet(subtract(subtract(Neg(j), one), Neg(i)), Natural)
# f_i_to_j__shift__eq_dec = \
# f_i_to_j_dec.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
# Natural)]).lhs.entries[0]
# lhs_done = f_i_to_j__shift__eq_dec.inner_expr().lhs[0].with_decreasing_order()
# lhs_done.inner_expr().rhs[0].with_decreasing_order()
# f_i_to_j__shift__eq_dec.rhs.entries[0].shift_equivalence(
# old_shift=one, new_shift=two,
# assumptions=[InSet(j, Integer), InSet(i, Integer),
# InSet(subtract(j, subtract(i, one)), Natural)])
tup=ExprTuple(a, b)
Len(a_i_to_j).computation(assumptions=[InSet(Add(j, Neg(i), one), Natural)])
tup_jdgmt = tup.prove(assumptions=[tup])
Not clear what the following cell is/was trying to accomplish:
# tup.prove(assumptions=[tup]).instantiate({a:a_i_to_j},
# assumptions=[InSet(Add(j, Neg(i), one), Natural)])
eq = f_i_to_jp1.partition(k, assumptions=[InSet(subtract(Add(k, one), i), Natural),
InSet(subtract(Add(j, one), k), Natural)])
eq.rhs.merger(assumptions=[InSet(subtract(Add(k, one), i), Natural),
InSet(subtract(Add(j, one), k), Natural)])
eq = f_i_to_jp1.partition(i, assumptions=[InSet(subtract(Add(j, one), i), Natural)])
eq.rhs.merger(assumptions=[InSet(subtract(Add(j, one), i), Natural)])
eq = f_i_to_j.partition(subtract(j, one), assumptions=[InSet(subtract(j, i), Natural)])
Add(subtract(j, one), one).simplification(assumptions=[InSet(j, Natural)])
eq.rhs.merger(assumptions=[InSet(subtract(j, i), Natural), InSet(j, Natural)])
ExprTuple.range_expansion()
method¶For self an ExprTuple with a single entry that is an ExprRange of the form f(i),...,f(j), where 0 <= (j-i) <= 9 (i.e. the ExprRange represents 1 to 10 elements), derive and return an equality between self and an ExprTuple with explicit entries replacing the ExprRange. For example, if
self = ExprTuple$(f(3),...,f(6))$,
then self.range_expansion()
would return:
$|- (f(3),...,f(6)) = (f(3), f(4), f(5), f(6))$
First not that we cannot create an ExprRange with only one element explicitly:
try:
ExprTuple(ExprRange(a, Function(g, a), two, two))
assert False, "Expecting a ValueError"
except ValueError as e:
print("Expected Error:", e)
We can, however, create an ExprRange that doesn't obviously have one element but may turn out to have one element after a simplification or substitution.
expr_tuple_with_1_elem_range = ExprTuple(ExprRange(a, Function(g, a), two, Mult(one, two)))
expr_tuple_with_1_elem_range.simplification()
ExprRange indices are already expected to be simplified w.r.t. quick_simplified_index
from proveit.numbers
, however, which deals with basic Add
and Neg
simplifications and combines all literal integers at the end of an Add
.
try:
# A one-element ExprRange (hidden by choosing the start and end indices
# that are equal but appear different)
example_expr_range_2 = ExprRange(i, IndexedVar(x, i), one, Add(one, zero))
assert False, "Expecting ValueError"
except ValueError as e:
print("Expected Error:", e)
range_expansion
does the same thing as simplification
in this case:
expr_tuple_with_1_elem_range.range_expansion()
# generate some example ExprTuples each containing a single ExprRange element
expr_tuple_with_2_elem_range, expr_tuple_with_2_elem_range_exp, expr_tuple_with_3_elem_range, expr_tuple_with_unknown_elem_range, expr_tuple_too_big = [
ExprTuple(ExprRange(a, Function(g, a), two, three)),
ExprTuple(ExprRange(a, Exp(two, Add(a, one)), two, three)),
ExprTuple(ExprRange(a, Exp(e_nat, Add(a, j)), two, four)),
ExprTuple(ExprRange(a, Exp(e_nat, Add(a, j)), i, k)),
ExprTuple(ExprRange(a, Function(g, a), two, num(20)))]
# find equivalent explicitly 2-element ExprTuple
expr_tuple_with_2_elem_range.range_expansion()
# find equivalent explicitly 2-element ExprTuple
# notice the automatic simplification
expr_tuple_with_2_elem_range_exp.range_expansion()
# find equivalent explicitly 2-element ExprTuple
# notice the automatic simplification
expr_tuple_with_3_elem_range.range_expansion()
# When the number of elements represented by the ExprRange is not known,
# the range_expansion() method fails with an informative error message
try:
expr_tuple_with_unknown_elem_range.range_expansion()
assert False, "Expecting an EvaluationError; should not get this far!"
except EvaluationError as the_error:
print("EvaluationError: {}".format(the_error))
# but if we give the method enough information about the indexing
# we can generate the equivalent explicit ExprTuple
expr_tuple_with_unknown_elem_range.range_expansion(
assumptions=[Equals(k, Add(i, four)), Equals(subtract(k, i), four)])
# When the number of elements represented by the ExprRange is > 10,
# the range_expansion() method fails with an informative error message
try:
expr_tuple_too_big.range_expansion(assumptions=[Equals(subtract(num(20), two), num(18))])
assert False, "Expecting an EvaluationError; should not get this far!"
except ValueError as the_error:
print("ValueError: {}".format(the_error))
# a related issue to ask about
try:
Equals(subtract(num(20), two), num(18)).prove()
except ProofFailure as the_error:
print("ProofFailure: {}".format(the_error))
A related example where the ExprRange and ExprTuple are being used as an argument for a TensorProd operator.
# create an example ExprRange
example_expr_range = ExprRange(i, IndexedVar(x, i), one, three)
# use the example ExprRange as the arg(s) for a TensorProd:
example_tensor_prod_over_range = TensorProd(example_expr_range)
# find the ExprTuple equivalent to the (ExprTuple-wrapped) ExprRange:
expr_range_eq_expr_tuple = ExprTuple(example_expr_range).range_expansion()
# find the equivalent explicit tensor prod
example_tensor_prod_over_range.inner_expr().operands.substitution(
expr_range_eq_expr_tuple)
%end demonstrations