Theorems (or conjectures) for the theory of proveit.numbers.number_sets.integers

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 Operation, IndexedVar
from proveit import a, b, c, d, e, f, g, h, i, m, n, x, y, S, P
from proveit.core_expr_types import (y_1_to_n)
from proveit.logic import (And, Equals, Forall, Implies, in_bool, InSet, NotInSet, Set,
                           NotEquals, Or, ProperSubset, SubsetEq, SetEquiv, EmptySet)
from proveit.logic.sets import Card, Disjoint, x_equals_any_y
from proveit.numbers import zero, one, num, frac, Neg
from proveit.numbers import (ZeroSet, Natural, NaturalPos, 
                             Integer, IntegerNeg, IntegerNonZero, IntegerNonPos, Interval, Complex)
from proveit.numbers import Add, subtract, greater, greater_eq, Less, LessEq, number_ordering
from proveit.numbers import Pzero, Pone, Pm, P_mAddOne, Pn

%begin theorems

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

zero_is_int = InSet(zero, Integer)

zero_is_int (conjecture with conjecture-based proof):

zero_is_nonpos_int = InSet(zero, IntegerNonPos)

zero_is_nonpos_int (conjecture without proof):

zero_set_within_int = ProperSubset(ZeroSet, Integer)

zero_set_within_int (conjecture without proof):

zero_set_within_nonpos_int = ProperSubset(ZeroSet, IntegerNonPos)

zero_set_within_nonpos_int (conjecture without proof):

# In Progress
#successive_nats = Forall(n, InSet(Add(n, one), Natural), domain=Natural)

# induction_lemma = Forall(n, Forall(S, Implies(And(InSet(zero, S), Forall(x, InSet(Add(x,one), S), domain=S)), InSet(n, S))), domain=Natural)

# induction = Forall(P, Implies(And(Pzero, 
#                                   Forall(m, P_mAddOne, 
#                                          domain=Natural, condition=Pm)), 
#                               Forall(n, Pn, domain=Natural)))

'''
nat_pos_induction = Forall(P, Implies(And(Pone, 
                                        Forall(m, P_mAddOne, domain=NaturalPos, 
                                               condition=Pm)), 
                                    Forall(n, Pn, domain=NaturalPos)))
'''

nonneg_int_is_natural = Forall(a, InSet(a,Natural), 
                            domain=Integer, condition=greater_eq(a, zero))

nonneg_int_is_natural (conjecture without proof):

pos_int_is_natural_pos = Forall(a, InSet(a,NaturalPos), 
                            domain=Integer, condition=greater(a, zero))

pos_int_is_natural_pos (conjecture without proof):

nonzero_nat_is_natural_pos = Forall(a, InSet(a, NaturalPos), 
                                    domain=Natural, condition=NotEquals(a, zero))

nonzero_nat_is_natural_pos (conjecture without proof):

A note about Interval-related theorems involving subsets of the Integers.

Some Interval-related theorems involving subsets of the Integers might be found in the respective number_sets package instead of here in the number_sets/integers package. For example, the interval_is_nat theorem: $\forall_{a, b\in\mathbb{N}}\left[ \forall_{n\in\{a...b\}}\left(n\in\mathbb{N}\right)\right]$ can be found in the number_sets/natural_numbers package.

A note/warning about a possible unfold theorem for the integral Interval class.

Although it is tempting to establish an unfold theorem analogous to the unfold theorem for the enumerated set class EnumSet, along the lines of:

$\forall_{n\in\mathbb{N}}\left[\forall_{x, y_1, \ldots, y_n \rvert x\in\{y_1...y_n\}}\left((x=y_1)\lor\ldots\lor(x=y_n)\right)\right]$

the underlying structure (or lack of structural constraint) involving the integral Interval class would allow instantiations leading to false conclusions. For example, one might instantiate such a theorem with $\{n: 3, x:x, y:(2, 6, 3)\}$, leading to the false conclusion that $\left((x = 2)\lor(x = 6)\lor(x = 3)\right)$.

interval_lower_bound = (
    Forall((a, b),
           Forall(n, LessEq(a, n), domain=Interval(a, b)), 
           domain=Integer))

interval_lower_bound (conjecture without proof):

interval_upper_bound = (
    Forall((a, b),
           Forall(n, LessEq(n, b), domain=Interval(a, b)), 
           domain=Integer))

interval_upper_bound (conjecture without proof):

vacuous_interval = Forall((a, b), Equals(Interval(a, b), EmptySet), condition=Less(b, a), domain=Integer)

vacuous_interval (conjecture without proof):

in_interval = Forall((a, b, n), InSet(n, Interval(a, b)), domain=Integer, 
                    conditions=[number_ordering(LessEq(a, n), LessEq(n, b))])

in_interval (conjecture without proof):

interval_cardinality = Forall(
    (a, b),
    Equals(Card(Interval(a, b)), Add(b, Neg(a), one)),
    domain=Integer,
    conditions=[LessEq(a, b)])

interval_cardinality (conjecture without proof):

interval_subset_eq = Forall(
    (a, b, c, d), SubsetEq(Interval(b, c), Interval(a, d)),
    domain=Integer,
    conditions=[number_ordering(LessEq(a, b), LessEq(b, c), LessEq(c, d))])

interval_subset_eq (conjecture without proof):

interval_subset = Forall(
    (a, b, c, d), ProperSubset(Interval(b, c), Interval(a, d)),
    domain=Integer,
    conditions=[number_ordering(Less(a, b), LessEq(b, c), Less(c, d))])

interval_subset (conjecture without proof):

int_interval_within_int = (
    Forall((a, b), ProperSubset(Interval(a, b), Integer),
           domain=Integer))

int_interval_within_int (conjecture without proof):

nat_interval_within_nat = (
    Forall((a, b), ProperSubset(Interval(a, b), Natural),
           domain=Natural))

nat_interval_within_nat (conjecture without proof):

natpos_interval_within_natpos = (
    Forall((a, b), ProperSubset(Interval(a, b), NaturalPos),
           domain=NaturalPos))

natpos_interval_within_natpos (conjecture without proof):

negint_interval_within_negint = (
    Forall((a, b), ProperSubset(Interval(a, b), IntegerNeg),
           domain=IntegerNeg))

negint_interval_within_negint (conjecture without proof):

nat_within_int = ProperSubset(Natural, Integer)

nat_within_int (conjecture without proof):

nat_pos_within_int = ProperSubset(NaturalPos, Integer)

nat_pos_within_int (conjecture without proof):

nat_pos_within_nonzero_int = ProperSubset(NaturalPos, IntegerNonZero)

nat_pos_within_nonzero_int (conjecture without proof):

nonzero_int_within_int = ProperSubset(IntegerNonZero, Integer)

nonzero_int_within_int (conjecture without proof):

neg_int_within_int = ProperSubset(IntegerNeg, Integer)

neg_int_within_int (conjecture without proof):

neg_int_within_nonzero_int = ProperSubset(IntegerNeg, IntegerNonZero)

neg_int_within_nonzero_int (conjecture without proof):

neg_int_within_nonpos_int = ProperSubset(IntegerNeg, IntegerNonPos)

neg_int_within_nonpos_int (conjecture without proof):

nonpos_int_within_int = ProperSubset(IntegerNonPos, Integer)

nonpos_int_within_int (conjecture without proof):

# Proven
zero_is_int = InSet(zero, Integer)

zero_is_int (conjecture with conjecture-based proof):

(alternate proof for zero_is_int)

nonzero_if_in_nonzero_int = Forall(a, NotEquals(a, zero), domain=IntegerNonZero)

nonzero_if_in_nonzero_int (conjecture without proof):

negative_if_in_neg_int = Forall(a, Less(a, zero), domain=IntegerNeg)

negative_if_in_neg_int (conjecture without proof):

nonpos_if_in_nonpos_int = Forall(a, LessEq(a, zero), domain=IntegerNonPos)

nonpos_if_in_nonpos_int (conjecture without proof):

nonzero_int_is_int_nonzero = Forall(
        a, InSet(a, IntegerNonZero), condition=NotEquals(a, zero),
        domain=Integer)

nonzero_int_is_int_nonzero (conjecture without proof):

neg_int_is_int_neg = Forall(
        a, InSet(a, IntegerNeg), condition=Less(a, zero),
        domain=Integer)

neg_int_is_int_neg (conjecture without proof):

nonzero_nonpos_int_is_neg_int = Forall(
        a, InSet(a, IntegerNeg), condition=NotEquals(a, zero),
        domain=IntegerNonPos)

nonzero_nonpos_int_is_neg_int (conjecture without proof):

nonpos_int_is_int_nonpos = Forall(
        a, InSet(a, IntegerNonPos), condition=LessEq(a, zero),
        domain=Integer)

nonpos_int_is_int_nonpos (conjecture without proof):

A set of in_bool theorems, which are accessed by the respective NumberSets to implement their deduce_membership_in_bool() methods:

# For Integer numbers
int_membership_is_bool = Forall(x, in_bool(InSet(x, Integer)))

int_membership_is_bool (conjecture without proof):

neg_int_membership_is_bool = Forall(x, in_bool(InSet(x, IntegerNeg)))

neg_int_membership_is_bool (conjecture without proof):

nonzero_int_membership_is_bool = Forall(x, in_bool(InSet(x, IntegerNonZero)))

nonzero_int_membership_is_bool (conjecture without proof):

nonpos_int_membership_is_bool = Forall(x, in_bool(InSet(x, IntegerNonPos)))

nonpos_int_membership_is_bool (conjecture without proof):

# For integer Intervals -- check w/WW about this (domain(s)?)
interval_membership_is_bool = (
    Forall((a, b),
           Forall(x, in_bool(InSet(x, Interval(a, b)))),
           domain=Integer))

interval_membership_is_bool (conjecture without proof):

difference_is_nat = Forall((a, b), InSet(subtract(a, b), Natural),
                              domain=Integer, 
                              conditions=[LessEq(b, a)])

difference_is_nat (conjecture without proof):

difference_is_nat_pos = \
    Forall((a, b), InSet(subtract(a, b), NaturalPos),
           domain=Integer, 
           conditions=[Less(b, a)])

difference_is_nat_pos (conjecture without proof):

Some Analogous Non-IntervalMembership Theorems

# interval_nonmembership
not_int_not_in_interval = (
    Forall((a, b),
           Forall(x, NotInSet(x, Interval(a, b)), domain=Complex, condition=NotInSet(x, Integer)),
           domain=Integer))

not_int_not_in_interval (conjecture without proof):

int_not_in_interval = (
    Forall((a, b, x),
           NotInSet(x, Interval(a, b)),
           domain=Integer,
           conditions=[Or(Less(x, a), Less(b, x))]))

int_not_in_interval (conjecture without proof):

bounds_for_int_not_in_interval = (
    Forall((a, b, x),
           Or(Less(x, a), Less(b, x)),
           domain=Integer,
           conditions=[NotInSet(x, Interval(a, b))]))

bounds_for_int_not_in_interval (conjecture without proof):

# For non-membership in integer Intervals -- check w/WW about this (domain(s)?)
interval_nonmembership_is_bool = (
    Forall((a, b),
           Forall(x, in_bool(NotInSet(x, Interval(a, b)))),
           domain=Integer))

interval_nonmembership_is_bool (conjecture without proof):

disjoint_intervals = (
    Forall((a, b, c, d),
           Disjoint(Interval(a, b), Interval(c, d)),
           domain=Integer,
           condition=number_ordering(LessEq(a, b), Less(b, c), LessEq(c, d))
          ))

disjoint_intervals (conjecture without proof):

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.number_sets.integers