Demonstrations for the theory of proveit.numbers.numerals.decimals¶
In [1]:
import proveit
from proveit import ExprRange, ExprTuple, var_range
from proveit.logic import Equals, InSet
from proveit.numbers import zero, one, two, three, four, five, six, seven, eight, nine
from proveit.numbers import (num, Add,
Natural, NaturalPos, subtract)
from proveit.numbers.numerals.decimals import DecimalSequence
from proveit.core_expr_types import Len
from proveit import A, a, b, c, d, e, f, g, h, i, j, k, m, n, x
from proveit.numbers.numerals.decimals import Digits
%begin demonstrations
Decimals are defined as numbers within the base-10 number system. That is, they use the numbers 0 through 9 for each digit. At the moment, only whole numbers are defined within Prove-It.
The digits 0 through 9 are individually defined literals that can be imported from proveit.numbers.
In [2]:
# each digit literal is defined as its linguistic counterpart. e.g. 1 is defined as "one"
zero
In order to create numbers larger than a single digit, create a DecimalSequence() object, or use the num() method.
In [3]:
# DecimalSequence() takes each digit as an argument
deci_sequence = DecimalSequence(one, zero, one)
deci_sequence: 
In [4]:
# the num() method takes in a python integer as an argument
num_def = num(101)
num_def:
In [5]:
Equals(deci_sequence, num_def).prove()
The set Digits is defined as the natural numbers from 0 to 9.
In [6]:
from proveit.numbers.numerals.decimals import N_leq_9_enumSet
N_leq_9_enumSet
In [7]:
InSet(one, Digits).prove()
Prove-It is also able to perform basic arithmetic involving decimal sequences.
In [8]:
Add(num(11), one).evaluation()
In [9]:
Add(num(999), one).evaluation()
In [10]:
Add(num(10), one).evaluation()
In [11]:
Len(ExprTuple(a, b, c, d, e, f, g, h, i, k, m)).evaluation()
In [12]:
Equals(Len(ExprTuple(a, b , c, d, e, f, g, h, i, k, m)),
Len(var_range(a, one, num(11)))
).prove()
In [13]:
Equals(Len(ExprTuple(a, b , c, d, e, f, g, h, i, k, m)), num(11)).prove()
In [14]:
Equals(Len(ExprTuple(a, b, c, d, e, f, g, h, i, k, m, n)), num(12)).prove()
In [15]:
nines = num(999999999)
nines: 
In [16]:
Add(nines, one).evaluation()
In [17]:
Add(num(99999), one).evaluation()
In [18]:
number = num(9999993)
number: 
In [19]:
Len(DecimalSequence(three, eight, six, seven, four, ExprRange(i, nine, one, four), five, seven, two).digits).computation()
In [20]:
%end demonstrations