Theorems (or conjectures) for the theory of proveit.numbers.numerals.decimals

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 ExprRange, ExprTuple, var_range, IndexedVar, Literal, Function
from proveit.logic import Forall, Equals, InSet, Set
from proveit.numbers import zero, one, two, three, four, five, six, seven, eight, nine
from proveit.numbers import (one, num, Add, subtract, Mult, Less,
                            Natural, NaturalPos, greater, greater_eq, LessEq, 
                             number_ordering)
from proveit.numbers.numerals.decimals import DecimalSequence
from proveit.numbers.numerals.decimals import Digits
#from proveit.numbers.numerals.decimals  import N_leq_9
from proveit.core_expr_types import Len
from proveit.core_expr_types import a_1_to_n, b_1_to_n, f_i_to_j
from proveit import a, b, c, d, e, f, g, h, i, j, k, m, n, x

%begin theorems

Defining theorems for theory 'proveit.numbers.numerals.decimals'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

md_nine_add_one = Forall((m, k), 
       Forall((var_range(a, one, m), b), 
              Equals(Add(DecimalSequence(var_range(a, one, m), b, ExprRange(i, nine, one, k)), one), 
                         DecimalSequence(var_range(a, one, m), Add(b, one), ExprRange(i, zero, one, k))), 
              domain=Digits, condition=Less(b, nine)), domain= Natural)

md_nine_add_one (conjecture without proof):

deci_sequence_reduction = Forall((m, n, k),
                                 Forall((var_range(a, one, m), var_range(b, one, n), c, var_range(d, one, k)),
                                       Equals(DecimalSequence(var_range(a, one, m), Add(var_range(b, one, n)), 
                                                              var_range(d, one, k)),
                                             DecimalSequence(var_range(a, one, m), c, var_range(d, one, k))),
                                       domain=Digits, 
                                        condition=Equals(Add(var_range(b, one, n)), c)), 
                                 domain=Natural)

deci_sequence_reduction (established theorem):

deci_sequence_reduction_ER = Forall((m, n, k),
                                 Forall((var_range(a, one, m), b, var_range(c, one, n), var_range(d, one, k)),
                                       Equals(DecimalSequence(var_range(a, one, m), ExprRange(i, b, one, n), 
                                                              var_range(d, one, k)),
                                             DecimalSequence(var_range(a, one, m), var_range(c, one, n), var_range(d, one, k))),
                                       domain=Digits, 
                                        condition=Equals(ExprTuple(ExprRange(i, b, one, n)), ExprTuple(var_range(c, one, n)))), 
                                 domain=Natural)

deci_sequence_reduction_ER (conjecture without proof):

deci_sequence_is_nat = Forall(n, Forall(a_1_to_n, 
                                             InSet(DecimalSequence(a_1_to_n), Natural),
                                            domain=Digits), domain=NaturalPos)

deci_sequence_is_nat (conjecture without proof):

deci_sequence_is_nat_pos = Forall(
    n, Forall((a, b_1_to_n), 
              InSet(DecimalSequence(a, b_1_to_n), NaturalPos),
              domain=Digits, condition=greater(a, zero)), 
    domain=Natural)

deci_sequence_is_nat_pos (conjecture without proof):

Number sets containing the digits (beyond 0):

nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9 = [InSet(num(n), Natural) for n in range(1, 10)]

nat1 (established theorem):

nat2 (conjecture with conjecture-based proof):

nat3 (conjecture without proof):

nat4 (conjecture without proof):

nat5 (conjecture without proof):

nat6 (conjecture without proof):

nat7 (conjecture without proof):

nat8 (conjecture without proof):

nat9 (conjecture without proof):

posnat1, posnat2, posnat3, posnat4, posnat5, posnat6, posnat7, posnat8, posnat9 = [InSet(num(n), NaturalPos) for n in range(1, 10)]

posnat1 (conjecture without proof):

posnat2 (conjecture without proof):

posnat3 (conjecture without proof):

posnat4 (conjecture without proof):

posnat5 (conjecture without proof):

posnat6 (conjecture without proof):

posnat7 (conjecture without proof):

posnat8 (conjecture without proof):

posnat9 (conjecture without proof):

digit0, digit1, digit2, digit3, digit4, digit5, digit6, digit7, digit8, digit9 = [InSet(num(n), Digits) for n in range(0, 10)] 

digit0 (conjecture without proof):

digit1 (conjecture without proof):

digit2 (conjecture without proof):

digit3 (conjecture without proof):

digit4 (conjecture without proof):

digit5 (conjecture without proof):

digit6 (conjecture without proof):

digit7 (conjecture without proof):

digit8 (conjecture without proof):

digit9 (conjecture without proof):

N_leq_9_enumSet = Equals(Digits, Set(zero, one, two, three, four, five, six, seven, eight, nine))

N_leq_9_enumSet (conjecture without proof):

digits_lower_bound = Forall(n, greater_eq(n, zero), domain=Digits)

digits_lower_bound (conjecture without proof):

digits_upper_bound = Forall(n, LessEq(n, nine), domain=Digits)

digits_upper_bound (conjecture without proof):

n_in_digits = Forall(n, InSet(n, Digits), 
                     conditions=[number_ordering(LessEq(zero, n), LessEq(n, nine))], 
                     domain=Natural)

n_in_digits (conjecture without proof):

Sorted order of the digits

less_0_1, less_1_2, less_2_3, less_3_4, less_4_5, less_5_6, less_6_7, less_7_8, less_8_9 = [Less(num(n), num(n+1)) for n in range(9)]

less_0_1 (conjecture without proof):

less_1_2 (conjecture without proof):

less_2_3 (conjecture without proof):

less_3_4 (conjecture without proof):

less_4_5 (conjecture without proof):

less_5_6 (conjecture without proof):

less_6_7 (conjecture without proof):

less_7_8 (conjecture without proof):

less_8_9 (conjecture without proof):

sorted_digits = number_ordering(*[Less(num(n), num(n+1)) for n in range(9)])

sorted_digits (conjecture without proof):

Adding digits

add_0_0, add_1_0, add_2_0, add_3_0, add_4_0, add_5_0, add_6_0, add_7_0, add_8_0, add_9_0 = [Equals(Add(num(n), num(0)), num(n+0)) for n in range(10)]

add_0_0 (conjecture without proof):

add_1_0 (conjecture without proof):

add_2_0 (conjecture without proof):

add_3_0 (conjecture without proof):

add_4_0 (conjecture without proof):

add_5_0 (conjecture without proof):

add_6_0 (conjecture without proof):

add_7_0 (conjecture without proof):

add_8_0 (conjecture without proof):

add_9_0 (conjecture without proof):

add_0_1, add_1_1, add_2_1, add_3_1, add_4_1, add_5_1, add_6_1, add_7_1, add_8_1, add_9_1 = [Equals(Add(num(n), num(1)), num(n+1)) for n in range(10)]

add_0_1 (conjecture without proof):

add_1_1 (conjecture without proof):

add_2_1 (conjecture without proof):

add_3_1 (conjecture without proof):

add_4_1 (conjecture without proof):

add_5_1 (conjecture without proof):

add_6_1 (conjecture without proof):

add_7_1 (conjecture without proof):

add_8_1 (conjecture without proof):

add_9_1 (conjecture without proof):

add_0_2, add_1_2, add_2_2, add_3_2, add_4_2, add_5_2, add_6_2, add_7_2, add_8_2, add_9_2 = [Equals(Add(num(n), num(2)), num(n+2)) for n in range(10)]

add_0_2 (conjecture without proof):

add_1_2 (conjecture without proof):

add_2_2 (conjecture without proof):

add_3_2 (conjecture without proof):

add_4_2 (conjecture without proof):

add_5_2 (conjecture without proof):

add_6_2 (conjecture without proof):

add_7_2 (conjecture without proof):

add_8_2 (conjecture without proof):

add_9_2 (conjecture without proof):

add_0_3, add_1_3, add_2_3, add_3_3, add_4_3, add_5_3, add_6_3, add_7_3, add_8_3, add_9_3 = [Equals(Add(num(n), num(3)), num(n+3)) for n in range(10)]

add_0_3 (conjecture without proof):

add_1_3 (conjecture without proof):

add_2_3 (conjecture without proof):

add_3_3 (conjecture without proof):

add_4_3 (conjecture without proof):

add_5_3 (conjecture without proof):

add_6_3 (conjecture without proof):

add_7_3 (conjecture without proof):

add_8_3 (conjecture without proof):

add_9_3 (conjecture without proof):

add_0_4, add_1_4, add_2_4, add_3_4, add_4_4, add_5_4, add_6_4, add_7_4, add_8_4, add_9_4 = [Equals(Add(num(n), num(4)), num(n+4)) for n in range(10)]

add_0_4 (conjecture without proof):

add_1_4 (conjecture without proof):

add_2_4 (conjecture without proof):

add_3_4 (conjecture without proof):

add_4_4 (conjecture without proof):

add_5_4 (conjecture without proof):

add_6_4 (conjecture without proof):

add_7_4 (conjecture without proof):

add_8_4 (conjecture without proof):

add_9_4 (conjecture without proof):

add_0_5, add_1_5, add_2_5, add_3_5, add_4_5, add_5_5, add_6_5, add_7_5, add_8_5, add_9_5 = [Equals(Add(num(n), num(5)), num(n+5)) for n in range(10)]

add_0_5 (conjecture without proof):

add_1_5 (conjecture without proof):

add_2_5 (conjecture without proof):

add_3_5 (conjecture without proof):

add_4_5 (conjecture without proof):

add_5_5 (conjecture without proof):

add_6_5 (conjecture without proof):

add_7_5 (conjecture without proof):

add_8_5 (conjecture without proof):

add_9_5 (conjecture without proof):

add_0_6, add_1_6, add_2_6, add_3_6, add_4_6, add_5_6, add_6_6, add_7_6, add_8_6, add_9_6 = [Equals(Add(num(n), num(6)), num(n+6)) for n in range(10)]

add_0_6 (conjecture without proof):

add_1_6 (conjecture without proof):

add_2_6 (conjecture without proof):

add_3_6 (conjecture without proof):

add_4_6 (conjecture without proof):

add_5_6 (conjecture without proof):

add_6_6 (conjecture without proof):

add_7_6 (conjecture without proof):

add_8_6 (conjecture without proof):

add_9_6 (conjecture without proof):

add_0_7, add_1_7, add_2_7, add_3_7, add_4_7, add_5_7, add_6_7, add_7_7, add_8_7, add_9_7 = [Equals(Add(num(n), num(7)), num(n+7)) for n in range(10)]

add_0_7 (conjecture without proof):

add_1_7 (conjecture without proof):

add_2_7 (conjecture without proof):

add_3_7 (conjecture without proof):

add_4_7 (conjecture without proof):

add_5_7 (conjecture without proof):

add_6_7 (conjecture without proof):

add_7_7 (conjecture without proof):

add_8_7 (conjecture without proof):

add_9_7 (conjecture without proof):

add_0_8, add_1_8, add_2_8, add_3_8, add_4_8, add_5_8, add_6_8, add_7_8, add_8_8, add_9_8 = [Equals(Add(num(n), num(8)), num(n+8)) for n in range(10)]

add_0_8 (conjecture without proof):

add_1_8 (conjecture without proof):

add_2_8 (conjecture without proof):

add_3_8 (conjecture without proof):

add_4_8 (conjecture without proof):

add_5_8 (conjecture without proof):

add_6_8 (conjecture without proof):

add_7_8 (conjecture without proof):

add_8_8 (conjecture without proof):

add_9_8 (conjecture without proof):

add_0_9, add_1_9, add_2_9, add_3_9, add_4_9, add_5_9, add_6_9, add_7_9, add_8_9, add_9_9 = [Equals(Add(num(n), num(9)), num(n+9)) for n in range(10)]

add_0_9 (conjecture without proof):

add_1_9 (conjecture without proof):

add_2_9 (conjecture without proof):

add_3_9 (conjecture without proof):

add_4_9 (conjecture without proof):

add_5_9 (conjecture without proof):

add_6_9 (conjecture without proof):

add_7_9 (conjecture without proof):

add_8_9 (conjecture without proof):

add_9_9 (conjecture without proof):

md_only_nine_add_one = Forall(k, Equals(Add(DecimalSequence(ExprRange(i, nine, one, k)), one), 
                         DecimalSequence(one, ExprRange(i, zero, one, k))), 
              domain= NaturalPos)

md_only_nine_add_one (conjecture without proof):

Multiplying digits

mult_0_0, mult_1_0, mult_2_0, mult_3_0, mult_4_0, mult_5_0, mult_6_0, mult_7_0, mult_8_0, mult_9_0 = [Equals(Mult(num(n), num(0)), num(n*0)) for n in range(10)]

mult_0_0 (conjecture without proof):

mult_1_0 (conjecture without proof):

mult_2_0 (conjecture without proof):

mult_3_0 (conjecture without proof):

mult_4_0 (conjecture without proof):

mult_5_0 (conjecture without proof):

mult_6_0 (conjecture without proof):

mult_7_0 (conjecture without proof):

mult_8_0 (conjecture without proof):

mult_9_0 (conjecture without proof):

mult_0_1, mult_1_1, mult_2_1, mult_3_1, mult_4_1, mult_5_1, mult_6_1, mult_7_1, mult_8_1, mult_9_1 = [Equals(Mult(num(n), num(1)), num(n*1)) for n in range(10)]

mult_0_1 (conjecture without proof):

mult_1_1 (conjecture without proof):

mult_2_1 (conjecture without proof):

mult_3_1 (conjecture without proof):

mult_4_1 (conjecture without proof):

mult_5_1 (conjecture without proof):

mult_6_1 (conjecture without proof):

mult_7_1 (conjecture without proof):

mult_8_1 (conjecture without proof):

mult_9_1 (conjecture without proof):

mult_0_2, mult_1_2, mult_2_2, mult_3_2, mult_4_2, mult_5_2, mult_6_2, mult_7_2, mult_8_2, mult_9_2 = [Equals(Mult(num(n), num(2)), num(n*2)) for n in range(10)]

mult_0_2 (conjecture without proof):

mult_1_2 (conjecture without proof):

mult_2_2 (conjecture without proof):

mult_3_2 (conjecture without proof):

mult_4_2 (conjecture without proof):

mult_5_2 (conjecture without proof):

mult_6_2 (conjecture without proof):

mult_7_2 (conjecture without proof):

mult_8_2 (conjecture without proof):

mult_9_2 (conjecture without proof):

mult_0_3, mult_1_3, mult_2_3, mult_3_3, mult_4_3, mult_5_3, mult_6_3, mult_7_3, mult_8_3, mult_9_3 = [Equals(Mult(num(n), num(3)), num(n*3)) for n in range(10)]

mult_0_3 (conjecture without proof):

mult_1_3 (conjecture without proof):

mult_2_3 (conjecture without proof):

mult_3_3 (conjecture without proof):

mult_4_3 (conjecture without proof):

mult_5_3 (conjecture without proof):

mult_6_3 (conjecture without proof):

mult_7_3 (conjecture without proof):

mult_8_3 (conjecture without proof):

mult_9_3 (conjecture without proof):

mult_0_4, mult_1_4, mult_2_4, mult_3_4, mult_4_4, mult_5_4, mult_6_4, mult_7_4, mult_8_4, mult_9_4 = [Equals(Mult(num(n), num(4)), num(n*4)) for n in range(10)]

mult_0_4 (conjecture without proof):

mult_1_4 (conjecture without proof):

mult_2_4 (conjecture without proof):

mult_3_4 (conjecture without proof):

mult_4_4 (conjecture without proof):

mult_5_4 (conjecture without proof):

mult_6_4 (conjecture without proof):

mult_7_4 (conjecture without proof):

mult_8_4 (conjecture without proof):

mult_9_4 (conjecture without proof):

mult_0_5, mult_1_5, mult_2_5, mult_3_5, mult_4_5, mult_5_5, mult_6_5, mult_7_5, mult_8_5, mult_9_5 = [Equals(Mult(num(n), num(5)), num(n*5)) for n in range(10)]

mult_0_5 (conjecture without proof):

mult_1_5 (conjecture without proof):

mult_2_5 (conjecture without proof):

mult_3_5 (conjecture without proof):

mult_4_5 (conjecture without proof):

mult_5_5 (conjecture without proof):

mult_6_5 (conjecture without proof):

mult_7_5 (conjecture without proof):

mult_8_5 (conjecture without proof):

mult_9_5 (conjecture without proof):

mult_0_6, mult_1_6, mult_2_6, mult_3_6, mult_4_6, mult_5_6, mult_6_6, mult_7_6, mult_8_6, mult_9_6 = [Equals(Mult(num(n), num(6)), num(n*6)) for n in range(10)]

mult_0_6 (conjecture without proof):

mult_1_6 (conjecture without proof):

mult_2_6 (conjecture without proof):

mult_3_6 (conjecture without proof):

mult_4_6 (conjecture without proof):

mult_5_6 (conjecture without proof):

mult_6_6 (conjecture without proof):

mult_7_6 (conjecture without proof):

mult_8_6 (conjecture without proof):

mult_9_6 (conjecture without proof):

mult_0_7, mult_1_7, mult_2_7, mult_3_7, mult_4_7, mult_5_7, mult_6_7, mult_7_7, mult_8_7, mult_9_7 = [Equals(Mult(num(n), num(7)), num(n*7)) for n in range(10)]

mult_0_7 (conjecture without proof):

mult_1_7 (conjecture without proof):

mult_2_7 (conjecture without proof):

mult_3_7 (conjecture without proof):

mult_4_7 (conjecture without proof):

mult_5_7 (conjecture without proof):

mult_6_7 (conjecture without proof):

mult_7_7 (conjecture without proof):

mult_8_7 (conjecture without proof):

mult_9_7 (conjecture without proof):

mult_0_8, mult_1_8, mult_2_8, mult_3_8, mult_4_8, mult_5_8, mult_6_8, mult_7_8, mult_8_8, mult_9_8 = [Equals(Mult(num(n), num(8)), num(n*8)) for n in range(10)]

mult_0_8 (conjecture without proof):

mult_1_8 (conjecture without proof):

mult_2_8 (conjecture without proof):

mult_3_8 (conjecture without proof):

mult_4_8 (conjecture without proof):

mult_5_8 (conjecture without proof):

mult_6_8 (conjecture without proof):

mult_7_8 (conjecture without proof):

mult_8_8 (conjecture without proof):

mult_9_8 (conjecture without proof):

mult_0_9, mult_1_9, mult_2_9, mult_3_9, mult_4_9, mult_5_9, mult_6_9, mult_7_9, mult_8_9, mult_9_9 = [Equals(Mult(num(n), num(9)), num(n*9)) for n in range(10)]

mult_0_9 (conjecture without proof):

mult_1_9 (conjecture without proof):

mult_2_9 (conjecture without proof):

mult_3_9 (conjecture without proof):

mult_4_9 (conjecture without proof):

mult_5_9 (conjecture without proof):

mult_6_9 (conjecture without proof):

mult_7_9 (conjecture without proof):

mult_8_9 (conjecture without proof):

mult_9_9 (conjecture without proof):

Tuple lengths and length reductions for 1-9

def count_from_one(count):
    return [num(k) for k in range(1, count+1)]
count_to_2_range, count_to_3_range, count_to_4_range, count_to_5_range, count_to_6_range, count_to_7_range, count_to_8_range, count_to_9_range = \
    [Equals(count_from_one(count), [ExprRange(k, k, one, num(count))]) for count in range(2, 10)]

count_to_2_range (conjecture without proof):

count_to_3_range (conjecture without proof):

count_to_4_range (conjecture without proof):

count_to_5_range (conjecture without proof):

count_to_6_range (conjecture without proof):

count_to_7_range (conjecture without proof):

count_to_8_range (conjecture without proof):

count_to_9_range (conjecture without proof):

reduce_0_repeats = Forall(x, Equals([ExprRange(i, x, one, zero)], ExprTuple()))

reduce_0_repeats (conjecture without proof):

def listvar(count):
    return [x for k in range(1, count+1)]
reduce_2_repeats, reduce_3_repeats, reduce_4_repeats, reduce_5_repeats, reduce_6_repeats, reduce_7_repeats, reduce_8_repeats, reduce_9_repeats = \
    [Forall(x, Equals([ExprRange(i, x, one, num(count))], listvar(count))) for count in range(2, 10)]

reduce_2_repeats (conjecture without proof):

reduce_3_repeats (conjecture without proof):

reduce_4_repeats (conjecture without proof):

reduce_5_repeats (conjecture without proof):

reduce_6_repeats (conjecture without proof):

reduce_7_repeats (conjecture without proof):

reduce_8_repeats (conjecture without proof):

reduce_9_repeats (conjecture without proof):

# This first case is special because we cannot represent an
# ExprRange that is trivially singular (that is, "(1, ..., 1)"
# is immediately reduced to "(1)").
tuple_len_1_typical_eq = Forall(a, Equals(Len([a]), Len([one])))

tuple_len_1_typical_eq (conjecture without proof):

cur_vars = vars()
def nvars(count):
    return [cur_vars[chr(ord('a')+k)] for k in range(count)]
tuple_len_2_typical_eq, tuple_len_3_typical_eq, tuple_len_4_typical_eq, tuple_len_5_typical_eq, tuple_len_6_typical_eq, tuple_len_7_typical_eq, tuple_len_8_typical_eq, tuple_len_9_typical_eq = \
    [Forall(nvars(count), Equals(Len(nvars(count)), Len([ExprRange(k, k, one, num(count))]))) for count in range(2, 10)]

tuple_len_2_typical_eq (conjecture without proof):

tuple_len_3_typical_eq (conjecture without proof):

tuple_len_4_typical_eq (conjecture without proof):

tuple_len_5_typical_eq (conjecture without proof):

tuple_len_6_typical_eq (conjecture without proof):

tuple_len_7_typical_eq (conjecture without proof):

tuple_len_8_typical_eq (conjecture without proof):

tuple_len_9_typical_eq (conjecture without proof):

tuple_len_1, tuple_len_2, tuple_len_3, tuple_len_4, tuple_len_5, tuple_len_6, tuple_len_7, tuple_len_8, tuple_len_9 = \
    [Forall(nvars(count), Equals(Len(nvars(count)), num(count))) for count in range(1, 10)]

tuple_len_1 (conjecture without proof):

tuple_len_2 (conjecture with conjecture-based proof):

tuple_len_3 (conjecture with conjecture-based proof):

tuple_len_4 (conjecture with conjecture-based proof):

tuple_len_5 (conjecture with conjecture-based proof):

tuple_len_6 (conjecture without proof):

tuple_len_7 (conjecture without proof):

tuple_len_8 (conjecture without proof):

tuple_len_9 (conjecture without proof):

range_1_expansion = Forall(
        (f, i, j),
        Equals(ExprTuple(f_i_to_j),[Function(f, i)]),
        conditions=[Equals(j, i)])

range_1_expansion (conjecture without proof):

range_2_expansion, range_3_expansion, range_4_expansion, range_5_expansion, range_6_expansion, range_7_expansion, range_8_expansion, range_9_expansion = \
        [Forall((f, i, j),
                Equals(ExprTuple(f_i_to_j),
                       [Function(f, i)]+[Function(f, Add(i, num(a))) for a in list(range(1, n))]),
                conditions=[Equals(j, Add(i, num(n-1)))]) for n in range(2,10)]

range_2_expansion (conjecture without proof):

range_3_expansion (conjecture without proof):

range_4_expansion (conjecture without proof):

range_5_expansion (conjecture without proof):

range_6_expansion (conjecture without proof):

range_7_expansion (conjecture without proof):

range_8_expansion (conjecture without proof):

range_9_expansion (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.numerals.decimals