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

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 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
In [2]:
%begin theorems
Defining theorems for theory 'proveit.numbers.numerals.decimals'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
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)

In [4]:
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,
domain=Natural)
deci_sequence_reduction (established theorem):

In [5]:
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):

In [6]:
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):

In [7]:
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):¶

In [8]:
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):

In [9]:
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):

In [10]:
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):

In [11]:
N_leq_9_enumSet = Equals(Digits, Set(zero, one, two, three, four, five, six, seven, eight, nine))
N_leq_9_enumSet (conjecture without proof):

In [12]:
digits_lower_bound = Forall(n, greater_eq(n, zero), domain=Digits)
digits_lower_bound (conjecture without proof):

In [13]:
digits_upper_bound = Forall(n, LessEq(n, nine), domain=Digits)
digits_upper_bound (conjecture without proof):

In [14]:
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¶

In [15]:
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):

In [16]:
sorted_digits = number_ordering(*[Less(num(n), num(n+1)) for n in range(9)])
sorted_digits (conjecture without proof):

In [17]:

In [18]:

In [19]:

In [20]:

In [21]:

In [22]:

In [23]:

In [24]:

In [25]:

In [26]:

In [27]:
DecimalSequence(one, ExprRange(i, zero, one, k))),
domain= NaturalPos)

### Multiplying digits¶

In [28]:
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):

In [29]:
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):

In [30]:
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):

In [31]:
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):

In [32]:
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):

In [33]:
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):

In [34]:
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):

In [35]:
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):

In [36]:
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):

In [37]:
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¶

In [38]:
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):

In [39]:
reduce_0_repeats = Forall(x, Equals([ExprRange(i, x, one, zero)], ExprTuple()))
reduce_0_repeats (conjecture without proof):

In [40]:
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):

In [41]:
# 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):

In [42]:
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):

In [43]:
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):

In [44]:
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):

In [45]:
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):

In [46]:
%end theorems
These theorems may now be imported from the theory package: proveit.numbers.numerals.decimals