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

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¶

Introduction
Simple Expressions involving the Natural numbers $\mathbb{N}$ and the Integer numbers $\mathbb{Z}$
Common Attributes of NumberSet classes
Axioms
Further Demonstrations

Demo 1
Demo 2
Demo 3

Introduction ¶

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}$).

InSet(n, Natural).deduce_in_bool()

InSet(a, NaturalPos).deduce_in_bool()

InSet(nine, NaturalPos).prove().proof()

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

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

three_in_2_9_interval, x_in_a_b_interval = (
    InSet(three, two_to_nine_interval), InSet(x, a_b_interval))

# testing automation
InSet(three, two_to_nine_interval).prove()

x_in_a_b_interval.prove(
    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:

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:

# 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:

# 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)])

# 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)])

# 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)])

# 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:

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.

InSet(x, Integer).prove(assumptions = [InSet(x, Interval(two, four))])

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$.

LessEq(four, x).prove(assumptions = [InSet(x, Interval(four, two))])

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).

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:

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:

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

Testing `Interval.deduce_cardinality()` method¶

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)))

interval_3_to_8.deduce_cardinality()

interval_0_to_2_pow_t.deduce_cardinality(
    assumptions=[InSet(Exp(two, t), NaturalPos), greater_eq(Exp(two, t), zero)])

Derive membership in restricted number sets.¶

First, via automation

InSet(x, Integer).prove(assumptions=[InSet(x, Interval(two, four))])

InSet(x, Natural).prove(assumptions=[InSet(x, Interval(two, four))])

InSet(x, NaturalPos).prove(assumptions=[InSet(x, Interval(two, four))])

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

Neg(three).deduce_in_number_set(IntegerNonPos, automation=False)

InSet(x, IntegerNonPos).prove(assumptions=[InSet(x, Interval(Neg(four), Neg(three)))])

InSet(x, IntegerNeg).prove(assumptions=[InSet(x, Interval(Neg(four), Neg(three)))])

Now done manually

InSet(x, Interval(two, four)).derive_element_in_integer(
    assumptions=[InSet(x, Interval(two, four))])

InSet(x, Interval(two, three)).derive_element_in_natural(
    assumptions=[InSet(x, Interval(two, three))])

InSet(x, Interval(three, four)).derive_element_in_natural_pos(
    assumptions=[InSet(x, Interval(three, four))])

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))])

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))])

# 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.

NotInSet(three, Interval(four, seven)).prove()

NotInSet(eight, Interval(four, seven)).prove()

Or(Less(x, four), Less(seven, x)).prove(assumptions=[InSet(x, Integer), NotInSet(x, Interval(four, seven))])

Number set membership demonstrations¶

InSet(InSet(x, Integer), Boolean).prove()

InSet(InSet(x, IntegerNonZero), Boolean).prove()

InSet(InSet(x, IntegerNeg), Boolean).prove()

InSet(InSet(x, IntegerNonPos), Boolean).prove()

NotEquals(n, zero).prove(assumptions=[InSet(n, IntegerNonZero)], 
                         conclude_automation=False) # should be side-effect

Less(x, zero).prove(assumptions=[InSet(x, IntegerNeg)], 
                    conclude_automation=False) # should be side-effect

LessEq(x, zero).prove(assumptions=[InSet(x, IntegerNonPos)], 
                      conclude_automation=False) # should be side-effect

InSet(x, Natural).prove(assumptions=[InSet(x, Integer), greater_eq(x, zero)])

InSet(x, NaturalPos).prove(assumptions=[InSet(x, Integer), greater(x, zero)])

InSet(x, IntegerNonZero).prove(assumptions=[InSet(x, Integer), NotEquals(x, zero)])

InSet(x, IntegerNeg).prove(assumptions=[InSet(x, Integer), Less(x, zero)])

InSet(x, IntegerNonPos).prove(assumptions=[InSet(x, Integer), LessEq(x, zero)])

InSet(x, IntegerNonZero).prove(assumptions=[InSet(x, NaturalPos)])

InSet(x, Integer).prove(assumptions=[InSet(x, IntegerNonZero)])

InSet(x, Integer).prove(assumptions=[InSet(x, IntegerNeg)])

InSet(x, IntegerNonZero).prove(assumptions=[InSet(x, IntegerNeg)])

InSet(x, IntegerNonPos).prove(assumptions=[InSet(x, IntegerNeg)])

InSet(x, Integer).prove(assumptions=[InSet(x, IntegerNonPos)])

%end demonstrations

	step type	requirements	statement
0	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat9

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