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
Defining theorems for theory 'proveit.core_expr_types.tuples'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
singular_range_reduction = Forall((f, i, j), Equals(ExprTuple(f_i_to_j), 
                                           ExprTuple(Function(f, i))),
                                  conditions=[Equals(i, j)])
singular_range_reduction (established theorem):

In [4]:
tuple_len_0_typical_eq = Equals(Len([]), Len([ExprRange(a, a, one, zero)]))
tuple_len_0_typical_eq (conjecture without proof):

In [5]:
tuple_len = Forall(i, Forall(a_1_to_i, 
                             Equals(Len([a_1_to_i]), i)),
tuple_len (conjecture without proof):

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))
range_len (conjecture without proof):

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))
range_len_typical_eq (conjecture without proof):

In [8]:
range_len_is_nat = Forall((f, i, j), 
                           InSet(Len([f_i_to_j]), Natural),
                           conditions=InSet(i_to_j_len, Natural))
range_len_is_nat (conjecture without proof):

In [9]:
range_from1_len = Forall(i, Forall(f, Equals(Len([f_1_to_i]), i)),
range_from1_len (conjecture without proof):

In [10]:
range_from1_len_typical_eq = Forall(i, Forall(f, Equals(Len([f_1_to_i]), 
range_from1_len_typical_eq (conjecture without proof):

In [11]:
range_from1_len_is_nat = Forall(i, Forall(f, 
                                           InSet(Len([f_1_to_i]), Natural)),
range_from1_len_is_nat (conjecture without proof):

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)]))
extended_range_len (conjecture without proof):

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)]))
extended_range_len_typical_eq (conjecture without proof):

In [14]:
extended_range_from1_len = Forall(i, Forall((f, x), Equals(Len([f_1_to_i, x]), 
                                                           Add(i, one))),
extended_range_from1_len (conjecture without proof):

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)),
extended_range_from1_len_typical_eq (conjecture without proof):

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),
general_len (conjecture without proof):

In [17]:
len_of_ranges_with_repeated_indices = \
    Forall(n, Forall((f_1_to_n, i, j),
                           Mult(n, i_to_j_len)).with_wrap_before_operator(),
                     condition=InSet(i_to_j_len, Natural)),
len_of_ranges_with_repeated_indices (conjecture without proof):

In [18]:
len_of_ranges_with_repeated_indices_from_1 = \
    Forall(n, Forall((f_1_to_n, i),
                           Mult(n, i)).with_wrap_before_operator(),
                     condition=InSet(i, Natural)),
len_of_ranges_with_repeated_indices_from_1 (conjecture without proof):

In [19]:
len_of_empty_range_of_ranges = Forall((m, n), Forall((f, i, j),
                                domain=Natural, condition=Equals(Add(n, one), m))
len_of_empty_range_of_ranges (conjecture without proof):

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)])
n_repeats_reduction (conjecture without proof):

In [21]:
empty_inside_range_of_range = Forall((f, i, j, m, n), Equals(ExprTuple(ExprRange(a, ExprRange(b, fab, i, j), m, n)), 
                         conditions=[Equals(Add(j, one), i)])
empty_inside_range_of_range (conjecture without proof):

In [22]:
empty_outside_range_of_range = Forall((f, i, j, m, n), Equals(ExprTuple(ExprRange(a, ExprRange(b, fab, i, j), m, n)), 
                         conditions=[Equals(Add(n, one), m)])
empty_outside_range_of_range (conjecture without proof):

In [23]:
partition = \
    Forall((f, i, j, k), partition_equiv,
           conditions=[InSet(subtract(Add(j, one), i), Natural),
                       InSet(subtract(k, j), Natural)])
partition (conjecture without proof):

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))])
merge (conjecture without proof):

In [25]:
partition_front = Forall((f, i, j), partition_front_equiv,
                         conditions=[InSet(subtract(j, i),
partition_front (conjecture without proof):

In [26]:
merge_front = Forall((f, i, j, k), merge_front_equiv,
                     conditions=[InSet(subtract(k, i), Natural),
                                 Equals(j, Add(i, one))])
merge_front (conjecture without proof):

In [27]:
partition_back = Forall((f, i, j), partition_back_equiv,
                        conditions=[InSet(subtract(j, i),
partition_back (conjecture without proof):

In [28]:
merge_back = Forall((f, i, j, k), merge_back_equiv,
                    conditions=[InSet(subtract(k, i),
                                Equals(k, Add(j, one))])
merge_back (conjecture without proof):

In [29]:
merge_extension = Forall((f, i, j), iter_ext_equiv.reversed(),
merge_extension (conjecture without proof):

In [30]:
merge_pair = Forall((f, i, j), Equals(ExprTuple(fi, fj), 
                    conditions=[Equals(j, Add(i, one))])
merge_pair (conjecture without proof):

In [31]:
merge_series = Forall((f, i, j), Forall(x_0_to_jmi, 
                                        conditions = [merge_series_conditions]),
                      conditions=[InSet(subtract(j, i), Natural)])
merge_series (conjecture without proof):

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])),
range_fn_transformation (conjecture without proof):

In [33]:
shift_equivalence = \
    Forall(f, Forall(a, Forall((i, j, k, l), 
                               conditions = [InSet(subtract(Add(j, one), i), Natural),
                                             Equals(k, subtract(i, a)),
                                             Equals(l, subtract(j, a))
shift_equivalence (conjecture without proof):

In [34]:
negated_shift_equivalence = Forall(f, Forall(a, Forall((i, j, k, l), 
                               conditions = [InSet(subtract(subtract(j, one), i), Natural),
                                             Equals(k, subtract(i, a)),
                                             Equals(l, subtract(j, a))
negated_shift_equivalence (conjecture without proof):

In [35]:
shift_equivalence_both = \
    Forall(f, Forall((a, b), Forall((i, j, k, l), 
                                    conditions = [InSet(subtract(Add(j, one), i), Natural),
                                                  Equals(Add(i, a), Add(k, b)),
                                                  Equals(Add(j, a), Add(l, b))
shift_equivalence_both (conjecture without proof):

In [36]:
negated_shift_equivalence_both = Forall(f, Forall((a, b), Forall((i, j, k, l), 
                                    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
negated_shift_equivalence_both (conjecture without proof):

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)]),
tuple_eq_via_elem_eq (conjecture with conjecture-based proof):

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))),
tuple_neq_via_any_elem_neq (conjecture without proof):

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)
tuple_elem_substitution (conjecture without proof):

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)
tuple_portion_substitution (conjecture without proof):

In [41]:
%end theorems
These theorems may now be imported from the theory package: proveit.core_expr_types.tuples