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

import proveit
from proveit import ProofFailure
from proveit import a, b, c, n, r, x, y
from proveit.logic import Boolean, InSet, NotEquals, NotInSet, Or, ProperSubset
from proveit.numbers import Less, LessEq, greater, greater_eq, Neg, number_ordering
from proveit.numbers import (
    Complex, Rational, RationalNonZero, RationalPos, RationalNeg,
    RationalNonNeg, RationalNonPos, IntervalCC, IntervalCO, IntervalOC,
    IntervalOO, Real, RealNonZero, RealPos, RealNeg, RealNonNeg, RealNonPos)
from proveit.numbers import zero, one, two, three, four, five, six, seven, eight, nine
%begin demonstrations

Real Numbers and Real Intervals
$\mathbf{R}$, $\mathbf{R}^+$, $\mathbf{R}^-$, $\mathbf{R}^{\ge 0}$, $[a, b]$, $[a, b)$, $(a, b]$, $(a, b)$

Introduction
Simple Expressions involving the Real number sets and real number intervals $\mathbf{R}$, $[a, b]$, etc
Common Attributes of the Real number NumberSets and real number intervals
Axioms
Theorems
Further Demonstrations

$2\in(1, 3]$ and $2\in[1, 3]$
Proving $[1,2]\subseteq \mathbb{R}^{+}$
Proving $[1,4]\subset \mathbb{R}^{+}$

Misc Testing (temporary)

Introduction ¶

The real numbers (or more simply, the “reals”), symbolized by $\mathbb{R}$, consist of the set of all rational numbers, $\mathbb{Q}$, such as $-10$ or $\frac{4}{3}$, and the set of all irrational numbers, such as $\pi$ and $\sqrt{2}$.
The reals, various common subsets of the reals, and various open, closed, and half-open real intervals are ubiquitous in proofs and are easily represented and accessed in Prove-It.

Simple Expressions Involving Real NumberSets and Real Intervals ¶

The real numbers $\mathbb{R}$ and some standard real-valued subsets of the reals have standard names in Prove-It and can be imported and called upon as desired.

# The real numbers
Real

# The positive real numbers
RealPos

# The negative real numbers
RealNeg

# The non-negative real numbers [0, Inf]
RealNonNeg

# An example claim that x is a non-negative real number
InSet(x, RealNonNeg)

Open, closed, and half-open real intervals are also easy to express and easy to utilize in larger expressions, with the following constructions:

real interval	Prove-It construction
(a, b)	IntervalOO(a, b)
(a, b]	IntervalOC(a, b)
[a, b)	IntervalCO(a, b)
[a, b]	IntervalCC(a, b)

</font> For example:

# Claim that x is a real number in the open interval (a, b)
# Notice the IntervalOO uses two 'ohs', not zeros, standing
# for 'open' at each end
InSet(x, IntervalOO(a, b))

# Claim that y is a real number in the half-open interval (a, b]
# Notice the IntervalOC uses an 'ohs', not a zero, standing for
# 'open' on the left side
InSet(y, IntervalOC(a, b))

# Or simply define some intervals of interest
interval_C1bO, interval_C23C = (
    IntervalCO(one, b), IntervalCC(two, three))

Common Attributes of NumberSet and Interval expressions ¶

Let's look at some simple examples of real NumberSets and real Intervals, along with some of their attributesibutes.

example_set, interval_C1bO = RealPos, IntervalCO(one, b)

# The expression for our set of real positive numbers is simply a Literal
example_set.expr_info()

# The interval expression has more structure and each
# of the boundaries can be either a Literal or a Variable
interval_C1bO.expr_info()

We can access the left-hand and right-hand bounds of the interval combined as a simple tuple, or access each bound separately:

# the bounds extracted as a tuple
interval_C1bO.operands

# lower bound
interval_C1bO.lower_bound

# upper bound
interval_C1bO.upper_bound

Many simple interval membership claims can be deduced relatively easily via `IntervalXX` methods relying on related theorems:

# here is an unproven claim
two_in_O13C = InSet(two, IntervalOC(one, three))

two_in_O13C.prove()

Prove-It will not automatically prove our assertion that $2\in (1, 3]$:

# try:
#     two_in_O13C.prove()
# except ProofFailure as e:
#     print("ProofFailure. {}".format(e))

But we can manually prompt Prove-It to prove that $2\in (1, 3]$ utilizing an explicit `Interval` method:

# # deduce the claim as a judgment
# IntervalOC(one, three).deduce_elem_in_set(two)

Axioms ¶

The current axioms for the `number/sets/real` theory consist of definitions of what it means for something to be an element of a real interval. For example, when we write $x\in (a, b)$ for $a \le b$ and $a,b\in \mathbb{R}$, that is equivalent to saying $x\in\mathbb{R}$ and $a < x < b$.
The axiom for open intervals is shown below (and the related axioms can be found in the [axioms notebook](./\_axioms\_.ipynb)):

from proveit.numbers.number_sets.real_numbers  import in_IntervalOO_def
in_IntervalOO_def

Theorems ¶

There are already a good number of basic theorems established in the `number/sets/real` theory. Some examples are shown explicitly below, and the remainder can be found in the [theorems Jupyter Python notebook](./\_theorems\_.ipynb). Most such theorems are typically not acccessed directly but are instead used behind-the-scenes when calling various related class methods.

from proveit.numbers.number_sets.real_numbers import (
        all_in_interval_oc__is__real, in_IntervalOO,
        interval_cc_lower_bound,
        nat_within_real_nonneg, not_int_if_between_successive_int)

# The natural numbers are a proper subset of the non-negative reals
nat_within_real_nonneg

# all elems of a real interval are real numbers
all_in_interval_oc__is__real

# all elements in [a, b] are ≥ a
interval_cc_lower_bound

# reals greater than a but less than b are in the interval (a, b)
in_IntervalOO

# a real value between successive integers is not itself an integer
not_int_if_between_successive_int

Demonstrations ¶

1. $2\in(1,3]$ and $2\in[1,3]$

We begin with a simple demonstration deriving the judgment $\vdash 2\in(1, 3]$, and then also deriving as a judgment the fact that $2\in[1, 3]$ using an `IntervalOC` method based on a relaxation theorem.

First we define a real number interval of interest:

interval_O1_3C = IntervalOC(one, three)

We can automatically deduce that $2\in(1,3]$.

interval_O1_3C.deduce_elem_in_set(two)

Then we consider the closed real interval $[1,3]$:

interval_C1_3C = IntervalCC(one, three)

The underlying machinery will not automatically prove that $2$ is also in this closed interval $[1, 3]$, despite the fact that we have the judgment $2\in(1,3]$: YES IT WILL NOW, SO CHANGE THIS

InSet(two, IntervalCC(one, three)).prove()

# from proveit import ProofFailure
# try:
#     InSet(two, IntervalCC(one, three)).prove()
#     assert False, "Expecting a ProofFailure error; should not make it to this point"
# except ProofFailure as e:
#     print("EXPECTED ERROR:", e)

We could instead use the `deduce_elem_in_set()` Interval class method, or we can use the `deduce_relaxed_membership()` method variation, and because we have previously shown that $2\in(1,3]$ we don't need to provide that fact as an assumption for the deduction:

two_in_O1_3C = interval_O1_3C.deduce_relaxed_membership(two)

The proof that Prove-It produces involves a number of steps dealing with the elements 1, 2, and 3 being positive naturals (important in this case as a subset of the reals), and the definition of $2\in(1,3]$, all of which eventually lead to the instantiation of a relaxation theorem (see rows 0–4):

two_in_O1_3C.proof()

2. Proving $[1,2]\subseteq \mathbb{R}^{+}$

The set of real numbers in the closed interval $[1, 2]$ is clearly a subset (and thus also an improper subset) of the positive real numbers $\mathbb{R}^{+}$. Prove-It will not automatically prove this, however:

from proveit.logic import SubsetEq
try:
    SubsetEq(IntervalCC(one, two), RealPos).prove()
except ProofFailure as e:
    print("Proof failure. {}".format(e))

So we do a little work first to lead Prove-It to a proof. (See Demonstration #3 below for an alternative approach.)

First we define our interval of interest and use some basic IntervalCC methods to derive that an element of $[1,2]$ is real, greater than or equal to 1, and greater than 0:</font>

# define our interval of interest
interval_12 = IntervalCC(one, two)

# if x is in [1, 2] x must be real
interval_12.deduce_member_in_real(x, assumptions=[InSet(x, interval_12)])

# and of course if x is in [1, 2] then 1 ≤ x
interval_12.deduce_member_lower_bound(x, assumptions=[InSet(x, interval_12)])

# x being real and x ≥ 1 also means x > 0
from proveit.numbers import greater
greater(x, zero).conclude_via_transitivity(assumptions=[InSet(x, interval_12)])

Trivially, $x \in \mathbb{R}^+$ if $x \in [1, 2]$ since we know $x > 0$:

x_in_interval_then_xPos = InSet(x, RealPos).prove(assumptions=[InSet(x, interval_12)])

If we jump the gun a bit here and ask Prove-It to now complete the proof, we still get an error message:

from proveit.logic import SubsetEq
try:
    SubsetEq(IntervalCC(one, two), RealPos).prove()
except ProofFailure as e:
    print("Proof failure. {}".format(e))

But the error message is instructive: apparently Prove-It is trying to apply modus ponens to a known implication, and we just need to modify our earlier result to make it more obviously applicable. So we generalize the previous judgment that $\{x\in [1, 2]\}\vdash x \in \mathbb{R}^{+}$ as follows:

# generalize
x_in_interval_then_xPos.generalize(x, conditions=[InSet(x, interval_12)])

And now Prove-It has the pieces it needs to establish the desired judgment:

# The previous generalization result allows the instantiation of
# a conditional theorem definition of improper subset
SubsetEq(interval_12, RealPos).prove()

It turns out it takes quite a bit more work to take the further step and conclude that $[1, 2] \subset \mathbb{R}^{+}$ (i.e., using a strict subset instead of an improper subset). Such proper subset relationships have been formulated as theorems, as demonstrated below in the next example.

3. Proving $[1,4]\subset \mathbb{R}^{+}$

The set of real numbers in the closed interval $[1, 4]$ is clearly a subset of the positive real numbers $\mathbb{R}^{+}$. We prove this subset relationship by instantiation of a general theorem:

c_in_pos_interval = InSet(c, IntervalCC(one, four))
c_in_pos_interval = c_in_pos_interval.prove(assumptions=[c_in_pos_interval])

c_in_pos_interval.derive_element_in_restricted_number_set()

c_in_nonneg_interval = InSet(c, IntervalCC(zero, four))
c_in_nonneg_interval = c_in_nonneg_interval.prove(assumptions=[c_in_nonneg_interval])

c_in_nonneg_interval.derive_element_in_restricted_number_set()

c_in_neg_interval = InSet(c, IntervalCC(Neg(five), Neg(two)))
c_in_neg_interval = c_in_neg_interval.prove(assumptions=[c_in_neg_interval])

Less(two, five).conclude_from_similar_bound(Less(zero, one))

Less(Neg(five), Neg(two)).conclude_from_similar_bound(Less(zero, one))

Less(Neg(five), Neg(two)).readily_provable()

True

Less(Neg(two), zero).prove()

Less(Neg(five), Neg(two)).prove()

c_in_neg_interval

c_in_neg_interval.derive_element_in_restricted_number_set()

c_in_nonpos_interval = InSet(c, IntervalCC(Neg(five), zero))
c_in_nonpos_interval = c_in_nonpos_interval.prove(assumptions=[c_in_nonpos_interval])

zero.deduce_in_number_set(RealNonPos, conclude_automation=False)

c_in_nonpos_interval.derive_element_in_restricted_number_set()

Misc Testing ¶

The material below was developed to test the various methods related to the real number NumberSet classes and the Interval classes. Some or all of this material could eventually be integrated into the `demonstrations` page and/or deleted as development continues.

Testing the `derive_element_lower_bound()` and `deduce_element_upper_bound()` methods for Real sets¶

one_is__real_pos_implies_one_greater_zero = InSet(one, RealPos).derive_element_lower_bound()

InSet(Neg(two), RealNeg).prove()

InSet(Neg(two), RealNeg).derive_element_upper_bound()

InSet(two, RealNonNeg).derive_element_lower_bound()

Testing the `derive_element_lower_bound()` and `deduce_element_upper_bound()` methods for real intervals¶

# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, three)).derive_element_lower_bound()

alternate way

IntervalOO(one, three).deduce_member_lower_bound(two)

# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, three)).derive_element_upper_bound()

# Variable Element in an Open Interval (1,3)
InSet(c, IntervalOO(one, three)).derive_element_upper_bound(
    assumptions=[InSet(c, IntervalOO(one, three))])

# Element in a Half-Open Interval (1,3]
InSet(two, IntervalOC(one, three)).derive_element_lower_bound()

# Element in a Half-Open Interval (1,3]
InSet(two, IntervalOC(one, three)).derive_element_upper_bound()

# Element in a Half-Open Interval [1,3)
InSet(two, IntervalCO(one, three)).derive_element_lower_bound()

# Element in a Half-Open Interval [1,3)
InSet(two, IntervalCO(one, three)).derive_element_upper_bound()

# Element in a Closed Interval [1,3]
InSet(two, IntervalCC(one, three)).derive_element_lower_bound()

# Element in a Closed Interval [1,3]
InSet(two, IntervalCC(one, three)).derive_element_upper_bound()

Testing the `Interval.deduce_member_in_real()` methods¶

# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, three)).derive_element_in_real()

alternate way

IntervalOO(one, three).deduce_member_in_real(two)

# Variable Element in an Open Interval (1,3)
InSet(c, IntervalOO(one, three)).derive_element_in_real(
    assumptions=[InSet(c, IntervalOO(one, three))])

# Element in an Half-Open Interval (1,3]
InSet(two, IntervalOC(one, three)).derive_element_in_real(
    assumptions=[InSet(two, IntervalOC(one, three))])

# Variable Element in an Half-Open Interval (1,3]
InSet(c, IntervalOC(one, three)).derive_element_in_real(
        assumptions=[InSet(c, IntervalOC(one, three))])

# Element in an Half-Open Interval [1,3)
InSet(two, IntervalCO(one, three)).derive_element_in_real()

# Variable Element in an Half-Open Interval [1,3)
InSet(c, IntervalCO(one, three)).derive_element_in_real(
    assumptions=[InSet(c, IntervalCO(one, three))])

# Element in an Closed Interval [1,3)
InSet(two, IntervalCC(one, three)).derive_element_in_real()

# Variable Element in an Closed Interval [1,3)
# (do this slightly differently this time just to show we can)
InSet(c, IntervalCC(one, three)).prove(
    assumptions=[InSet(c, IntervalCC(one, three))]).derive_element_in_real()

Testing the `Interval.deduce_elem_in_set()` methods¶

# Element in an Open Interval (1,3)
IntervalOO(one, three).deduce_elem_in_set(two)

# but this should NOT work for a discluded endpoint
try:
    IntervalOO(one, three).deduce_elem_in_set(one)
except ProofFailure as e:
    print("Proof failure: {}".format(e))

Proof failure: Proof step failed:
Attempting to instantiate |- forall_{a, b, x in Real | a < x < b} (x in (a,b)) with {a: 1, b: 3, x: 1}:
Unsatisfied condition: 1 < 1 < 3. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# Element in Half-Open Interval (1,4]
IntervalOC(one, four).deduce_elem_in_set(three)

# this should also work for the included (right) endpoint as well
IntervalOC(one, four).deduce_elem_in_set(four)

# but this should NOT work for the discluded (left) endpoint
try:
    IntervalOC(one, four).deduce_elem_in_set(one)
except ProofFailure as e:
    print("Proof failure: {}".format(e))

Proof failure: Proof step failed:
Attempting to instantiate |- forall_{a, b, x in Real | a < x <= b} (x in (a,b]) with {a: 1, b: 4, x: 1}:
Unsatisfied condition: 1 < 1 <= 4. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# Element in Half-Open Interval [2,4)
IntervalCO(two, four).deduce_elem_in_set(three)

# this should also work for the included (left) endpoint as well
IntervalCO(two, four).deduce_elem_in_set(two)

# but this should NOT work for the discluded (right) endpoint
try:
    IntervalCO(two, four).deduce_elem_in_set(four)
except ProofFailure as e:
    print("Proof failure: {}".format(e))

Proof failure: Proof step failed:
Attempting to instantiate |- forall_{a, b, x in Real | a <= x < b} (x in [a,b)) with {a: 2, b: 4, x: 4}:
Unsatisfied condition: 2 <= 4 < 4. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# Element in a Closed Interval [1,3]
IntervalCC(one, three).deduce_elem_in_set(two)

# this should also work for the included left endpoint
IntervalCC(one, three).deduce_elem_in_set(one)

# this should also work for the included right endpoint
IntervalCC(one, three).deduce_elem_in_set(three)

# but this should NOT work for a value outside the interval
try:
    IntervalCC(one, three).deduce_elem_in_set(four)
except ProofFailure as e:
    print("Proof failure: {}".format(e))

Proof failure: Proof step failed:
Attempting to instantiate |- forall_{a, b, x in Real | a <= x <= b} (x in [a,b]) with {a: 1, b: 3, x: 4}:
Unsatisfied condition: 1 <= 4 <= 3. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

Testing the `derive_rescaled_membership()` methods for real intervals¶

# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, four)).derive_rescaled_membership(two)

alternate way

# Element in an Open Interval (1,3)
IntervalOO(one, four).deduce_rescaled_membership(two, two)

# Element in an Half-Open Interval (1,3]
InSet(two, IntervalOC(one, three)).derive_rescaled_membership(three)

# Element in an Half-Open Interval [1,3)
InSet(two, IntervalCO(one, three)).derive_rescaled_membership(four)

# Element in an Closed Interval [1,3]
InSet(three, IntervalCC(zero, four)).derive_rescaled_membership(two)

Testing the `deduce_left/right_relaxed_membership()` methods for real intervals¶

# Element in open interval (1,4) means element in half-open interval [1,4)
InSet(c, IntervalOO(one, four)).derive_left_relaxed_membership(
    assumptions=[InSet(c, IntervalOO(one, four))])

# Element in open interval (1,4) means element in half-open interval (1,4]
InSet(c, IntervalOO(one, four)).derive_right_relaxed_membership(
    assumptions=[InSet(c, IntervalOO(one, four))])

# Element in open interval (1,4) means element in half-open interval (1,4]
InSet(c, IntervalOO(one, four)).derive_fully_relaxed_membership(
    assumptions=[InSet(c, IntervalOO(one, four))])

# Element in half-open interval (0,3] means element in closed interval [0,3]
InSet(c, IntervalOC(zero, three)).derive_relaxed_membership(
        assumptions=[InSet(c, IntervalOC(zero, three))])

# Element in half-open interval [0,3) means element in closed interval [0,3]
InSet(c, IntervalCO(zero, three)).derive_relaxed_membership(
        assumptions=[InSet(c, IntervalCO(zero, three))])

Testing the `InSet.deduce_in_bool()` methods
(indirectly testing the NumberSet.deduce_membership_in_bool() methods)

InSet(x, Real).deduce_in_bool()

InSet(y, RealPos).deduce_in_bool()

InSet(a, RealNeg).deduce_in_bool()

InSet(b, RealNonNeg).deduce_in_bool()

InSet(b, RealNonNeg).deduce_in_bool()

Misc Testing ¶

Testing automation methods
(indirectly testing the `RealIntervalMembership.conclude()` and `RealIntervalMembership.side_effects()` methods)

First, define a few real intervals:

o_one_five_o, o_two_four_o  = IntervalOO(one, five), IntervalOO(two, four)

And some membership claims:

two_in_o_one_five_o, x_in_o_two_four_o = InSet(two, o_one_five_o), InSet(x, o_two_four_o)

Testing (indirectly) the RealIntervalMembership.conclude() method:

two_in_o_one_five_o.prove()

x_in_o_two_four_o.prove(assumptions=[InSet(x, Real), number_ordering(Less(two, x), Less(x, four))])

Testing (indirectly) the RealIntervalMembership.side_effects() method:

… some set membership deductions and lower bounds

InSet(x, Real).prove(assumptions=[InSet(x, IntervalOO(two, three))])

InSet(x, Real).prove(assumptions=[InSet(x, IntervalOC(three, four))])

InSet(x, Real).prove(assumptions=[InSet(x, IntervalCO(zero, eight))])

InSet(x, Real).prove(assumptions=[InSet(x, IntervalCC(four, five))])

# if we don't have enough information about the nature of the endpts
# then x \in IntervalXX(a, b) still leaves us adrift
try:
    InSet(x, Real).prove(assumptions=[InSet(x, IntervalCC(a, b))])
except Exception as e:
    print("Exception: {}".format(e))

Exception: Unable to prove x in Real assuming {x in [a,b]}:
x has no 'readily_provable_number_set' method

# but if know the endpts are Real, then the IntervalXX is know to be legitimate:
InSet(x, Real).prove(assumptions=[InSet(a, Real), InSet(b, Real), InSet(x, IntervalCC(a, b))])

… some deductions of lower bounds

Less(three, x).prove(assumptions=[InSet(x, IntervalOO(three, five))])

Less(two, x).prove(assumptions=[InSet(x, IntervalOO(three, five))])

LessEq(five, x).prove(assumptions=[InSet(x, IntervalOC(five, eight))])

LessEq(three, x).prove(assumptions=[InSet(x, IntervalCO(three, seven))])

LessEq(zero, x).prove(assumptions=[InSet(x, IntervalCC(zero, two))])

… some upper bounds

Less(x, five).prove(assumptions=[InSet(x, IntervalOO(three, five))])

LessEq(x, six).prove(assumptions=[InSet(x, IntervalOC(four, six))])

Less(x, nine).prove(assumptions=[InSet(x, IntervalCO(seven, nine))])

LessEq(x, six).prove(assumptions=[InSet(x, IntervalCC(one, six))])

Testing the `RealIntervalMembership.deduce_in_bool()` method¶

InSet(x, IntervalOO(three, five)).deduce_in_bool()

InSet(x, IntervalOC(four, six)).deduce_in_bool()

InSet(x, IntervalCO(seven, nine)).deduce_in_bool()

InSet(x, IntervalCC(one, six)).deduce_in_bool()

Testing the `RealIntervalNonmembership.deduce_in_bool()` method¶

NotInSet(x, IntervalOO(three, five)).deduce_in_bool()

NotInSet(x, IntervalOC(four, six)).deduce_in_bool()

NotInSet(x, IntervalCO(seven, nine)).deduce_in_bool()

NotInSet(x, IntervalCC(one, six)).deduce_in_bool()

Testing the `RealIntervalNonmembership.deduce_real_element_bounds()` method¶

NotInSet(x, IntervalOO(three, five)).deduce_real_element_bounds(assumptions=[InSet(x, Real), NotInSet(x, IntervalOO(three, five))])

NotInSet(x, IntervalCO(four, six)).deduce_real_element_bounds(assumptions=[InSet(x, Real), NotInSet(x, IntervalCO(four, six))])

NotInSet(x, IntervalOC(seven, nine)).deduce_real_element_bounds(assumptions=[InSet(x, Real), NotInSet(x, IntervalOC(seven, nine))])

NotInSet(x, IntervalCC(one, six)).deduce_real_element_bounds(assumptions=[InSet(x, Real), NotInSet(x, IntervalCC(one, six))])

# more generally
NotInSet(x, IntervalCC(a, b)).deduce_real_element_bounds(assumptions=[InSet(x, Real), InSet(a, Real), InSet(b, Real), NotInSet(x, IntervalCC(a, b))])

Some direct deductions of non-membership-related bounds¶

Or(Less(x, two), Less(three, x) ).prove(assumptions=[InSet(x, Real), NotInSet(x, IntervalCC(two, three))])

Or(LessEq(x, three), LessEq(six, x) ).prove(assumptions=[InSet(x, Real), NotInSet(x, IntervalOO(three, six))])

Testing the automation for RealIntervalNonmembership¶

NotInSet(x, IntervalCC(one, six)).prove(assumptions=[NotInSet(x, Real), InSet(x, Complex)])

NotInSet(x, IntervalOO(one, six)).prove(assumptions= [InSet(x, Real), LessEq(x, one)])

NotInSet(x, IntervalCC(one, six)).prove(assumptions= [InSet(x, Real), Less(six, x)])

NotInSet(x, IntervalCO(three, eight)).prove(assumptions= [InSet(x, Real), Less(x, three)])

Testing the automation for real IntervalXX subset relationships¶

SubsetEq(IntervalOO(three, four), IntervalOO(two, five)).prove()

Currently, Prove-It will not be able to automatically deduce a proper subset relationship between two real intervals:

try:
    ProperSubset(IntervalOO(three, four), IntervalOO(two, five)).prove()
except Exception as e:
    print("Exception: {}".format(e))

Exception: Unable to prove (3,4) proper_subset (2,5):
'conclude' method not implemented for proof automation

Number set membership demonstrations¶

InSet(InSet(r, Real), Boolean).prove()

InSet(InSet(r, RealNonZero), Boolean).prove()

InSet(InSet(r, RealPos), Boolean).prove()

InSet(InSet(r, RealNeg), Boolean).prove()

InSet(InSet(r, RealNonNeg), Boolean).prove()

InSet(InSet(r, RealNonPos), Boolean).prove()

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

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

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

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

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

InSet(r, RealNonZero).prove(assumptions=[InSet(r, Real), NotEquals(r, zero)])

InSet(r, RealPos).prove(assumptions=[InSet(r, Real), greater(r, zero)])

InSet(r, RealNeg).prove(assumptions=[InSet(r, Real), Less(r, zero)])

InSet(r, RealNonNeg).prove(assumptions=[InSet(r, Real), greater_eq(r, zero)])

InSet(r, RealNonPos).prove(assumptions=[InSet(r, Real), LessEq(r, zero)])

InSet(r, Real).prove(assumptions=[InSet(r, Rational)])

InSet(r, RealNonZero).prove(assumptions=[InSet(r, RationalNonZero)])

InSet(r, RealPos).prove(assumptions=[InSet(r, RationalPos)])

InSet(r, RealNeg).prove(assumptions=[InSet(r, RationalNeg)])

InSet(r, RealNonNeg).prove(assumptions=[InSet(r, RationalNonNeg)])

InSet(r, RealNonPos).prove(assumptions=[InSet(r, RationalNonPos)])

InSet(r, Real).prove(assumptions=[InSet(r, RealNonZero)])

InSet(r, Real).prove(assumptions=[InSet(r, RealPos)])

InSet(r, RealNonZero).prove(assumptions=[InSet(r, RealPos)])

InSet(r, RealNonNeg).prove(assumptions=[InSet(r, RealPos)])

InSet(r, Real).prove(assumptions=[InSet(r, RealNeg)])

InSet(r, RealNonZero).prove(assumptions=[InSet(r, RealNeg)])

InSet(r, RealNonPos).prove(assumptions=[InSet(r, RealNeg)])

InSet(r, Real).prove(assumptions=[InSet(r, RealNonNeg)])

InSet(r, Real).prove(assumptions=[InSet(r, RealNonPos)])

%end demonstrations

	core type	sub-expressions
0	Operation	operator: 1 operands: 2
1	Literal
2	ExprTuple	3, 4
3	Literal
4	Variable

	step type	requirements	statement
0	instantiation	1, 2, 3, 4	⊢
	: , : , :
1	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.relax_IntervalOC
2	reference	6	⊢
3	reference	7	⊢
4	instantiation	5, 6, 7, 8, 9	⊢
	: , : , :
5	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOC
6	instantiation	25, 12, 10	⊢
	: , : , :
7	instantiation	25, 12, 11	⊢
	: , : , :
8	instantiation	25, 12, 13	⊢
	: , : , :
9	instantiation	14, 15, 16	⊢
	: , :
10	instantiation	25, 19, 17	⊢
	: , : , :
11	instantiation	25, 19, 18	⊢
	: , : , :
12	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
13	instantiation	25, 19, 20	⊢
	: , : , :
14	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
15	conjecture		⊢
	proveit.numbers.numerals.decimals.less_1_2
16	instantiation	21, 22	⊢
	: , :
17	instantiation	25, 26, 23	⊢
	: , : , :
18	instantiation	25, 26, 24	⊢
	: , : , :
19	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
20	instantiation	25, 26, 27	⊢
	: , : , :
21	conjecture		⊢
	proveit.numbers.ordering.relax_less
22	conjecture		⊢
	proveit.numbers.numerals.decimals.less_2_3
23	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
24	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
25	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
26	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
27	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2

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

Real Numbers and Real Intervals$\mathbf{R}$, $\mathbf{R}^+$, $\mathbf{R}^-$, $\mathbf{R}^{\ge 0}$, $[a, b]$, $[a, b)$, $(a, b]$, $(a, b)$

Introduction ¶

Simple Expressions Involving Real NumberSets and Real Intervals¶

Common Attributes of NumberSet and Interval expressions ¶

Axioms ¶

Theorems¶

Demonstrations ¶

Misc Testing ¶

Testing the derive_element_lower_bound() and deduce_element_upper_bound() methods for Real sets¶

Testing the derive_element_lower_bound() and deduce_element_upper_bound() methods for real intervals¶

Testing the Interval.deduce_member_in_real() methods¶

Testing the Interval.deduce_elem_in_set() methods¶

Testing the derive_rescaled_membership() methods for real intervals¶

Testing the deduce_left/right_relaxed_membership() methods for real intervals¶

Testing the InSet.deduce_in_bool() methods(indirectly testing the NumberSet.deduce_membership_in_bool() methods)

Misc Testing ¶

Testing automation methods(indirectly testing the RealIntervalMembership.conclude() and RealIntervalMembership.side_effects() methods)

Testing the RealIntervalMembership.deduce_in_bool() method¶

Testing the RealIntervalNonmembership.deduce_in_bool() method¶

Testing the RealIntervalNonmembership.deduce_real_element_bounds() method¶

Some direct deductions of non-membership-related bounds¶

Testing the automation for RealIntervalNonmembership¶

Testing the automation for real IntervalXX subset relationships¶

Number set membership demonstrations¶

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

Real Numbers and Real Intervals
$\mathbf{R}$, $\mathbf{R}^+$, $\mathbf{R}^-$, $\mathbf{R}^{\ge 0}$, $[a, b]$, $[a, b)$, $(a, b]$, $(a, b)$

Simple Expressions Involving Real NumberSets and Real Intervals ¶

Theorems ¶

Testing the `derive_element_lower_bound()` and `deduce_element_upper_bound()` methods for Real sets¶

Testing the `derive_element_lower_bound()` and `deduce_element_upper_bound()` methods for real intervals¶

Testing the `Interval.deduce_member_in_real()` methods¶

Testing the `Interval.deduce_elem_in_set()` methods¶

Testing the `derive_rescaled_membership()` methods for real intervals¶

Testing the `deduce_left/right_relaxed_membership()` methods for real intervals¶

Testing the `InSet.deduce_in_bool()` methods
(indirectly testing the NumberSet.deduce_membership_in_bool() methods)

Testing automation methods
(indirectly testing the `RealIntervalMembership.conclude()` and `RealIntervalMembership.side_effects()` methods)

Testing the `RealIntervalMembership.deduce_in_bool()` method¶

Testing the `RealIntervalNonmembership.deduce_in_bool()` method¶

Testing the `RealIntervalNonmembership.deduce_real_element_bounds()` method¶