Theorems (or conjectures) for the theory of proveit.core_expr_types.tuples¶
In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprTuple, ExprRange, IndexedVar, Function, var_range
from proveit import a, b, c, d, f, g, i, j, k, l, m, n, x, y, fab
from proveit.core_expr_types import Len
from proveit.core_expr_types import \
(range_1_to_i, range_1_to_ip1, range_i_to_j, range_i_to_jp1,
a_1_to_i, b_1_to_i, b_1_to_j, c_1_to_i, c_1_to_k, d_1_to_j, fi, fj, f_jp1, fk,
f_1_to_i, f_i_to_j, gk, g_i_to_j, i_to_j_len, j_to_k_len,
f_1_to_n, i_1_to_n, j_1_to_n, x_1_to_k, y_1_to_l, x_0_to_jmi,
concat_len_equiv, concat_len_simple_equiv, iter_ext_equiv,
partition_equiv, merge_equiv,
partition_front_equiv, merge_front_equiv,
partition_back_equiv, merge_back_equiv,
merge_series_conditions, merge_series_equiv)
from proveit.core_expr_types.tuples import \
(f_i_to_j__1_to_n, f_1_to_i__1_to_n, f_ik_to_jk__1_to_n, fk_i_to_j,
general_range_of_ranges, range_len_conditions, range_len_sum, shift_equiv, neg_shift_equiv, shift_equiv_both, neg_shift_equiv_both)
from proveit.logic import Forall, Equals, NotEquals, And, Or, InSet, Implies
from proveit.numbers import (Natural, NaturalPos, Integer, Add, Neg,
Mult, zero, one, two, subtract, Interval)
In [2]:
%begin theorems
In [3]:
singular_range_reduction = Forall((f, i, j), Equals(ExprTuple(f_i_to_j),
ExprTuple(Function(f, i))),
conditions=[Equals(i, j)])
In [4]:
tuple_len_0_typical_eq = Equals(Len([]), Len([ExprRange(a, a, one, zero)]))
In [5]:
tuple_len = Forall(i, Forall(a_1_to_i,
Equals(Len([a_1_to_i]), i)),
domain=Natural)
In [6]:
range_len = Forall((f, i, j),
Equals(Len([f_i_to_j]), i_to_j_len),
conditions=InSet(i_to_j_len, Natural))
In [7]:
range_len_typical_eq = Forall((f, i, j),
Equals(Len([f_i_to_j]), Len(range_i_to_j)),
conditions=InSet(i_to_j_len, Natural))
In [8]:
range_len_is_nat = Forall((f, i, j),
InSet(Len([f_i_to_j]), Natural),
conditions=InSet(i_to_j_len, Natural))
In [9]:
range_from1_len = Forall(i, Forall(f, Equals(Len([f_1_to_i]), i)),
domain=Natural)
In [10]:
range_from1_len_typical_eq = Forall(i, Forall(f, Equals(Len([f_1_to_i]),
Len(range_1_to_i))),
domain=Natural)
In [11]:
range_from1_len_is_nat = Forall(i, Forall(f,
InSet(Len([f_1_to_i]), Natural)),
domain=Natural)
In [12]:
extended_range_len = Forall((f, x), Forall((i, j),
Equals(Len([f_i_to_j, x]),
Add(j, Neg(i), two)),
conditions=[InSet(Len(f_i_to_j), Natural)]))
In [13]:
extended_range_len_typical_eq = \
Forall((f, x), Forall((i, j), Equals(Len([f_i_to_j, x]), Len(range_i_to_jp1)),
conditions=[InSet(Len(f_i_to_j), Natural)]))
In [14]:
extended_range_from1_len = Forall(i, Forall((f, x), Equals(Len([f_1_to_i, x]),
Add(i, one))),
domain=Natural)
In [15]:
extended_range_from1_len_typical_eq = \
Forall((f, x), Forall(i, Equals(Len([f_1_to_i, x]), Len(range_1_to_ip1)),
domain=Natural))
In [ ]:
Compute the length of an ExprTuple with any number of expression ranges:
In [16]:
general_len = \
Forall(n, Forall((f_1_to_n, i_1_to_n, j_1_to_n),
Equals(Len(f_ik_to_jk__1_to_n),
range_len_sum).with_wrap_before_operator(),
conditions=range_len_conditions).with_wrapping(),
domain=NaturalPos)
In [17]:
len_of_ranges_with_repeated_indices = \
Forall(n, Forall((f_1_to_n, i, j),
Equals(Len(f_i_to_j__1_to_n),
Mult(n, i_to_j_len)).with_wrap_before_operator(),
condition=InSet(i_to_j_len, Natural)),
domain=NaturalPos)
In [18]:
len_of_ranges_with_repeated_indices_from_1 = \
Forall(n, Forall((f_1_to_n, i),
Equals(Len(f_1_to_i__1_to_n),
Mult(n, i)).with_wrap_before_operator(),
condition=InSet(i, Natural)),
domain=NaturalPos)
In [19]:
len_of_empty_range_of_ranges = Forall((m, n), Forall((f, i, j),
Equals(Len(general_range_of_ranges),
zero).with_wrap_before_operator()),
domain=Natural, condition=Equals(Add(n, one), m))
In [ ]:
In [20]:
n_repeats_reduction = Forall((n, x), Equals([ExprRange(i, x, one, n)], ExprTuple(x, ExprRange(i, x, one, subtract(n, one)))),
conditions=[InSet(n, NaturalPos)])
In [21]:
empty_inside_range_of_range = Forall((f, i, j, m, n), Equals(ExprTuple(ExprRange(a, ExprRange(b, fab, i, j), m, n)),
ExprTuple()),
conditions=[Equals(Add(j, one), i)])
In [22]:
empty_outside_range_of_range = Forall((f, i, j, m, n), Equals(ExprTuple(ExprRange(a, ExprRange(b, fab, i, j), m, n)),
ExprTuple()),
conditions=[Equals(Add(n, one), m)])
In [23]:
partition = \
Forall((f, i, j, k), partition_equiv,
conditions=[InSet(subtract(Add(j, one), i), Natural),
InSet(subtract(k, j), Natural)])
In [24]:
merge = Forall((f, i, j, k, l), merge_equiv,
conditions=[InSet(subtract(k, i), Natural),
InSet(subtract(l, j), Natural),
Equals(k, Add(j, one))])
In [25]:
partition_front = Forall((f, i, j), partition_front_equiv,
conditions=[InSet(subtract(j, i),
Natural)])
In [26]:
merge_front = Forall((f, i, j, k), merge_front_equiv,
conditions=[InSet(subtract(k, i), Natural),
Equals(j, Add(i, one))])
In [27]:
partition_back = Forall((f, i, j), partition_back_equiv,
conditions=[InSet(subtract(j, i),
Natural)])
In [28]:
merge_back = Forall((f, i, j, k), merge_back_equiv,
conditions=[InSet(subtract(k, i),
Natural),
Equals(k, Add(j, one))])
In [29]:
merge_extension = Forall((f, i, j), iter_ext_equiv.reversed(),
conditions=[InSet(Len([f_i_to_j]),
Natural)])
In [30]:
merge_pair = Forall((f, i, j), Equals(ExprTuple(fi, fj),
ExprTuple(f_i_to_j)),
conditions=[Equals(j, Add(i, one))])
In [31]:
merge_series = Forall((f, i, j), Forall(x_0_to_jmi,
merge_series_equiv,
conditions = [merge_series_conditions]),
conditions=[InSet(subtract(j, i), Natural)])
In [32]:
# Transform the lambda function of the range.
range_fn_transformation = \
Forall((f, g), Forall((i, j), Implies(Forall(k, Equals(fk, gk),
domain=Interval(i, j)),
Equals([f_i_to_j], [g_i_to_j])),
domain=Integer))
In [33]:
shift_equivalence = \
Forall(f, Forall(a, Forall((i, j, k, l),
shift_equiv,
conditions = [InSet(subtract(Add(j, one), i), Natural),
Equals(k, subtract(i, a)),
Equals(l, subtract(j, a))
]),
domain=Integer))
In [34]:
negated_shift_equivalence = Forall(f, Forall(a, Forall((i, j, k, l),
neg_shift_equiv,
conditions = [InSet(subtract(subtract(j, one), i), Natural),
Equals(k, subtract(i, a)),
Equals(l, subtract(j, a))
]),
domain=Integer))
In [35]:
shift_equivalence_both = \
Forall(f, Forall((a, b), Forall((i, j, k, l),
shift_equiv_both,
conditions = [InSet(subtract(Add(j, one), i), Natural),
Equals(Add(i, a), Add(k, b)),
Equals(Add(j, a), Add(l, b))
]),
domain=Integer))
In [36]:
negated_shift_equivalence_both = Forall(f, Forall((a, b), Forall((i, j, k, l),
neg_shift_equiv_both,
conditions = [InSet(subtract(Add(j, one), i), Natural),
Equals(Add(i, a), Add(k, b)),
Equals(Add(j, a), Add(l, b))
]),
domain=Integer))# only used for decreasing exprranges
In [37]:
tuple_eq_via_elem_eq = Forall(i, Forall((a_1_to_i, b_1_to_i),
Equals(ExprTuple(a_1_to_i), ExprTuple(b_1_to_i)),
conditions=[ExprRange(k, Equals(IndexedVar(a, k),
IndexedVar(b, k)),
one, i)]),
domain=NaturalPos)
In [38]:
tuple_neq_via_any_elem_neq = Forall(
i, Forall((a_1_to_i, b_1_to_i),
NotEquals(ExprTuple(a_1_to_i), ExprTuple(b_1_to_i)),
condition=Or(ExprRange(k, NotEquals(IndexedVar(a, k),
IndexedVar(b, k)),
one, i))),
domain=NaturalPos)
In [39]:
tuple_elem_substitution = Forall((i, k),
Forall((a_1_to_i, b, c_1_to_k, d),
Equals([a_1_to_i, b, c_1_to_k],
[a_1_to_i, d, c_1_to_k]).with_wrap_after_operator(),
condition=Equals(b, d)),
domain = Natural)
In [40]:
tuple_portion_substitution = Forall((i, j, k),
Forall((a_1_to_i, b_1_to_j, c_1_to_k, d_1_to_j),
Equals([a_1_to_i, b_1_to_j, c_1_to_k],
[a_1_to_i, d_1_to_j, c_1_to_k]).with_wrap_after_operator(),
condition=Equals([b_1_to_j], [d_1_to_j])),
domain = Natural)
In [41]:
%end theorems