Demonstrations for the theory of proveit.numbers.number_sets.integers

In [1]:
import proveit
from proveit import a, b, c, d, n, x, ProofFailure
from proveit.logic import Boolean, NotEquals, InSet, NotInSet, Or
from proveit.numbers import Neg, Less, LessEq, greater, greater_eq, number_ordering
from proveit.numbers import (zero, one, two, three, four, five, six, seven,
                             eight, nine, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
                             Interval, Natural, NaturalPos)
%begin demonstrations

Natural Numbers $\mathbb{N}$, Positive Natural Numbers $\mathbb{N}^{+}$, & Integer Numbers $\mathbb{Z}$



UNDER CONSTRUCTION. Something here about the importance of having and using specifically pre-defined number sets such as the Natural number set ($\mathbb{N}$) and Integer number set ($\mathbb{Z}$), the axiomatic definitions, and perhaps the distinctiveness from the Real numbers ($\mathbb{R}$).

In [2]:
InSet(n, Natural).deduce_in_bool()
In [3]:
InSet(a, NaturalPos).deduce_in_bool()
In [4]:
InSet(nine, NaturalPos).prove().proof()
 step typerequirementsstatement
0conjecture  ⊢  
In [5]:
InSet(b, Integer).deduce_in_bool()

Miscellaneous Testing

The material below was developed to test various Integer and Integer Set-related methods. Some of this material could be integrated into the _demonstrations_ page eventually and/or deleted as development continues.

Some Example Domains For Testing

In [6]:
two_to_nine_interval, a_b_interval, c_d_interval = (
    Interval(two, nine), Interval(a, b), Interval(c, d))

Some Example Membership Claims For Testing

In [7]:
three_in_2_9_interval, x_in_a_b_interval = (
    InSet(three, two_to_nine_interval), InSet(x, a_b_interval))
In [8]:
# testing automation
InSet(three, two_to_nine_interval).prove()
In [9]:
    assumptions=[InSet(a, Integer), InSet(b, Integer), InSet(x, Integer),
                 number_ordering(LessEq(a, x), LessEq(x, b))])
, , ,  ⊢  

Define an Inset() expression involving an Interval class, then test some automation related to deductions about the element:

In [10]:
x_in_c_d_interval = InSet(x, c_d_interval)

Check that an IntervalMembership assumption is making its way into the IntervalMembership.side_effects() method and sub-methods:

In [11]:
# checking to see if the IntervalMembership assumption is making its way
# into the side_effects() method
x_in_c_d_interval.prove(assumptions = [x_in_c_d_interval, InSet(c, Integer), InSet(d, Integer)])

Check that an IntervalMembership assumption is producing the correct conclusions about Integer set membership and lower/upper bounds for the element:

In [12]:
# element should be an integer if Interval is properly defined:
InSet(x, Integer).prove(
    assumptions = [x_in_c_d_interval, InSet(c, Integer), InSet(d, Integer), LessEq(c, d)])
, ,  ⊢  
In [13]:
# element should be ≤ upper_bound of Interval
LessEq(x, d).prove(
    assumptions = [x_in_c_d_interval, InSet(c, Integer), InSet(d, Integer), LessEq(c, d)])
, ,  ⊢  
In [14]:
# element should be ≥ lower_bound of Interval
LessEq(c, x).prove(
    assumptions = [x_in_c_d_interval, InSet(c, Integer), InSet(d, Integer), LessEq(c, d)])
, ,  ⊢  
In [15]:
# the membership claim should itself be in Booleans (even without assumptions)
InSet(x_in_c_d_interval, Boolean).prove(assumptions=[InSet(c, Integer), InSet(d, Integer), LessEq(c, d)])

Also check that we can deduce an Interval element in positive naturals if the Interval lower_bound is known or assumed to be greater than 0:

In [16]:
InSet(x, NaturalPos).prove(
    assumptions = [x_in_c_d_interval, InSet(c, Integer),
                   InSet(d, Integer), greater(c, zero), LessEq(c, d)])
, , ,  ⊢  

Here is an interesting comparison case, comparing an attempted deduction when we assume that $x$ is in an Interval with explicit natural-number lower_- and upper_bounds, but where in one case the lower_bound ≤ the upper_bound as required and in the other case upper_bound ≤ lower_bound. The second, with “improper” bounds, is satisfied vacuously.

In [17]:
InSet(x, Integer).prove(assumptions = [InSet(x, Interval(two, four))])
In [18]:
InSet(x, Integer).prove(assumptions = [InSet(x, Interval(four, two))])

And here are other interesting test cases — where the Interval is created with “illegitimate” bounds (because the upper_bound < lower_bound), so we obtain vacuously true (and somewhat misleading-looking) conclusions: now it looks like we can simultaneously obtain $x \ge 4$ and $x \le 2$.

In [19]:
LessEq(four, x).prove(assumptions = [InSet(x, Interval(four, two))])
In [20]:
LessEq(x, two).prove(assumptions = [InSet(x, Interval(four, two))])

The following enters the interval_membership.side_effects() method as expected (although it will FAIL if we're still checking for lower_bound ≤ upper_bound in the side_effects() sub-methods).

In [21]:
InSet(x, NaturalPos).prove(assumptions = [InSet(x, Interval(one, two))])

Unfortunately, the following is also (vacuously) true, since the integer interval Interval(2, 1) is not valid:

In [22]:
InSet(x, Integer).prove(assumptions = [InSet(x, Interval(two, one))])

And to make things even more explicit, notice we can “appear” to prove that $8 \le 3$, but this judgment is vacuously true:

In [23]:
LessEq(eight, three).prove(assumptions = [InSet(x, Interval(eight, three))])

Testing Interval.deduce_cardinality() method

In [24]:
from proveit import t
from proveit.numbers import Exp
interval_3_to_8, interval_0_to_2_pow_t = (
    Interval(three, eight), Interval(zero, Exp(two, t)))
In [25]:
In [26]:
    assumptions=[InSet(Exp(two, t), NaturalPos), greater_eq(Exp(two, t), zero)])

Derive membership in restricted number sets.

First, via automation

In [27]:
InSet(x, Integer).prove(assumptions=[InSet(x, Interval(two, four))])
In [28]:
InSet(x, Natural).prove(assumptions=[InSet(x, Interval(two, four))])
In [29]:
InSet(x, NaturalPos).prove(assumptions=[InSet(x, Interval(two, four))])
In [30]:
InSet(x, NaturalPos).prove(
    assumptions = [x_in_c_d_interval, InSet(c, Integer),
                   InSet(d, Integer), greater(c, zero), LessEq(c, d)])
, , ,  ⊢  
In [31]:
Neg(three).deduce_in_number_set(IntegerNonPos, automation=False)
In [32]:
InSet(x, IntegerNonPos).prove(assumptions=[InSet(x, Interval(Neg(four), Neg(three)))])
In [33]:
InSet(x, IntegerNeg).prove(assumptions=[InSet(x, Interval(Neg(four), Neg(three)))])

Now done manually

In [34]:
InSet(x, Interval(two, four)).derive_element_in_integer(
    assumptions=[InSet(x, Interval(two, four))])
In [35]:
InSet(x, Interval(two, three)).derive_element_in_natural(
    assumptions=[InSet(x, Interval(two, three))])
In [36]:
InSet(x, Interval(three, four)).derive_element_in_natural_pos(
    assumptions=[InSet(x, Interval(three, four))])
In [37]:
InSet(x, Interval(a, b)).derive_element_in_integer_neg(
    assumptions=[InSet(a, Integer), InSet(b, Integer), Less(b, zero), InSet(x, Interval(a, b))])
, , ,  ⊢  
In [38]:
InSet(x, Interval(a, b)).derive_element_in_integer_nonpos(
    assumptions=[InSet(a, Integer), InSet(b, Integer), Less(b, zero), InSet(x, Interval(a, b))])
, , ,  ⊢  
In [ ]:
In [39]:
# A case I worry about:
# (1) If the deduce_element_in_restricted_number_set() method does a check for the
# lower_bound <= upper_bound, this fails as it should and we eventual enter
# the NumberMembership.conclude() method as expected.
# (2) BUT, if we first run the cell above, then this cell never seems to enter
# the IntervalMembership.side_effects() method, going only to the
# NumberMembership.conclude() method. Shouldn't it “evaluate” the assumptions?
# (3) If the deduce_element_in_restricted_number_set() method does NOT check for the
# lower_bound <= upper_bound, this goes through as it should using that side_effect.
# (4) BUT, if we first run the cell above, then this cell never enters
# the IntervalMembership.side_effects() method, nor the NumberMembership.conclude() method,
# because in performing the previous cell, the x \in NaturalPos under these assumptions
# was already established. Nothing mysterious!
# InSet(x, NaturalPos).prove(assumptions = [InSet(x, Interval(eight, three))]).proof()

Some brief testing of Interval non-membership.

In [40]:
NotInSet(three, Interval(four, seven)).prove()
In [41]:
NotInSet(eight, Interval(four, seven)).prove()
In [42]:
Or(Less(x, four), Less(seven, x)).prove(assumptions=[InSet(x, Integer), NotInSet(x, Interval(four, seven))])

Number set membership demonstrations

In [43]:
InSet(InSet(x, Integer), Boolean).prove()
In [44]:
InSet(InSet(x, IntegerNonZero), Boolean).prove()
In [45]:
InSet(InSet(x, IntegerNeg), Boolean).prove()
In [46]:
InSet(InSet(x, IntegerNonPos), Boolean).prove()
In [47]:
NotEquals(n, zero).prove(assumptions=[InSet(n, IntegerNonZero)], 
                         conclude_automation=False) # should be side-effect
In [48]:
Less(x, zero).prove(assumptions=[InSet(x, IntegerNeg)], 
                    conclude_automation=False) # should be side-effect
In [49]:
LessEq(x, zero).prove(assumptions=[InSet(x, IntegerNonPos)], 
                      conclude_automation=False) # should be side-effect
In [50]:
InSet(x, Natural).prove(assumptions=[InSet(x, Integer), greater_eq(x, zero)])
In [51]:
InSet(x, NaturalPos).prove(assumptions=[InSet(x, Integer), greater(x, zero)])
In [52]:
InSet(x, IntegerNonZero).prove(assumptions=[InSet(x, Integer), NotEquals(x, zero)])
In [53]:
InSet(x, IntegerNeg).prove(assumptions=[InSet(x, Integer), Less(x, zero)])
In [54]:
InSet(x, IntegerNonPos).prove(assumptions=[InSet(x, Integer), LessEq(x, zero)])
In [55]:
InSet(x, IntegerNonZero).prove(assumptions=[InSet(x, NaturalPos)])
In [56]:
InSet(x, Integer).prove(assumptions=[InSet(x, IntegerNonZero)])
In [57]:
InSet(x, Integer).prove(assumptions=[InSet(x, IntegerNeg)])
In [58]:
InSet(x, IntegerNonZero).prove(assumptions=[InSet(x, IntegerNeg)])
In [59]:
InSet(x, IntegerNonPos).prove(assumptions=[InSet(x, IntegerNeg)])
In [60]:
InSet(x, Integer).prove(assumptions=[InSet(x, IntegerNonPos)])
In [61]:
%end demonstrations