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

In [1]:
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 ¶

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.

In [2]:
# The real numbers
Real

In [3]:
# The positive real numbers
RealPos

In [4]:
# The negative real numbers
RealNeg

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

In [6]:
# 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:

In [7]:
# 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))

In [8]:
# 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))

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

interval_C1bO:
interval_C23C:

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

In [10]:
example_set, interval_C1bO = RealPos, IntervalCO(one, b)

example_set:
interval_C1bO:
In [11]:
# The expression for our set of real positive numbers is simply a Literal
example_set.expr_info()

core typesub-expressionsexpression
0Literal
In [12]:
# The interval expression has more structure and each
# of the boundaries can be either a Literal or a Variable
interval_C1bO.expr_info()

core typesub-expressionsexpression
0Operationoperator: 1
operands: 2
1Literal
2ExprTuple3, 4
3Literal
4Variable

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

In [13]:
# the bounds extracted as a tuple
interval_C1bO.operands

In [14]:
# lower bound
interval_C1bO.lower_bound

In [15]:
# upper bound
interval_C1bO.upper_bound


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

In [16]:
# here is an unproven claim
two_in_O13C = InSet(two, IntervalOC(one, three))

two_in_O13C:
In [17]:
two_in_O13C.prove()


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

In [18]:
# 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:

In [19]:
# # 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)):

In [20]:
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.

In [21]:
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)

In [22]:
# The natural numbers are a proper subset of the non-negative reals
nat_within_real_nonneg

In [23]:
# all elems of a real interval are real numbers
all_in_interval_oc__is__real

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

In [25]:
# reals greater than a but less than b are in the interval (a, b)
in_IntervalOO

In [26]:
# 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:

In [27]:
interval_O1_3C = IntervalOC(one, three)

interval_O1_3C:

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

In [28]:
interval_O1_3C.deduce_elem_in_set(two)


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

In [29]:
interval_C1_3C = IntervalCC(one, three)

interval_C1_3C:

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

In [30]:
InSet(two, IntervalCC(one, three)).prove()

In [31]:
# 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:

In [32]:
two_in_O1_3C = interval_O1_3C.deduce_relaxed_membership(two)

two_in_O1_3C:

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

In [33]:
two_in_O1_3C.proof()

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

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:

In [34]:
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>

In [35]:
# define our interval of interest
interval_12 = IntervalCC(one, two)

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

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

In [38]:
# 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$:

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

x_in_interval_then_xPos:

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

In [40]:
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:

In [41]:
# 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:

In [42]:
# 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:

In [43]:
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:
In [44]:
c_in_pos_interval.derive_element_in_restricted_number_set()

In [45]:
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:
In [46]:
c_in_nonneg_interval.derive_element_in_restricted_number_set()

In [47]:
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])

c_in_neg_interval:
In [48]:
Less(two, five).conclude_from_similar_bound(Less(zero, one))

In [49]:
Less(Neg(five), Neg(two)).conclude_from_similar_bound(Less(zero, one))

In [50]:
Less(Neg(five), Neg(two)).readily_provable()

True
In [51]:
Less(Neg(two), zero).prove()

In [52]:
Less(Neg(five), Neg(two)).prove()

In [53]:
c_in_neg_interval

In [54]:
c_in_neg_interval.derive_element_in_restricted_number_set()

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

c_in_nonpos_interval:
In [56]:
zero.deduce_in_number_set(RealNonPos, conclude_automation=False)

In [57]:
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¶

In [58]:
one_is__real_pos_implies_one_greater_zero = InSet(one, RealPos).derive_element_lower_bound()

one_is__real_pos_implies_one_greater_zero:
In [59]:
InSet(Neg(two), RealNeg).prove()

In [60]:
InSet(Neg(two), RealNeg).derive_element_upper_bound()

In [61]:
InSet(two, RealNonNeg).derive_element_lower_bound()


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

In [62]:
# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, three)).derive_element_lower_bound()


alternate way

In [63]:
IntervalOO(one, three).deduce_member_lower_bound(two)

In [64]:
# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, three)).derive_element_upper_bound()

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

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

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

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

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

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

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


### Testing the Interval.deduce_member_in_real() methods¶

In [72]:
# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, three)).derive_element_in_real()


alternate way

In [73]:
IntervalOO(one, three).deduce_member_in_real(two)

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

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

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

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

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

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

In [80]:
# 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¶

In [81]:
# Element in an Open Interval (1,3)
IntervalOO(one, three).deduce_elem_in_set(two)

In [82]:
# 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.

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

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

In [85]:
# 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.

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

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

In [88]:
# 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.

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

In [90]:
# this should also work for the included left endpoint
IntervalCC(one, three).deduce_elem_in_set(one)

In [91]:
# this should also work for the included right endpoint
IntervalCC(one, three).deduce_elem_in_set(three)

In [92]:
# 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¶

In [93]:
# Element in an Open Interval (1,3)
InSet(two, IntervalOO(one, four)).derive_rescaled_membership(two)


alternate way

In [94]:
# Element in an Open Interval (1,3)
IntervalOO(one, four).deduce_rescaled_membership(two, two)

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

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

In [97]:
# 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¶

In [98]:
# 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))])

In [99]:
# 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))])

In [100]:
# 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))])

In [101]:
# 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))])

In [102]:
# 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)

In [103]:
InSet(x, Real).deduce_in_bool()

In [104]:
InSet(y, RealPos).deduce_in_bool()

In [105]:
InSet(a, RealNeg).deduce_in_bool()

In [106]:
InSet(b, RealNonNeg).deduce_in_bool()

In [107]:
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:

In [108]:
o_one_five_o, o_two_four_o  = IntervalOO(one, five), IntervalOO(two, four)

o_one_five_o:
o_two_four_o:

And some membership claims:

In [109]:
two_in_o_one_five_o, x_in_o_two_four_o = InSet(two, o_one_five_o), InSet(x, o_two_four_o)

two_in_o_one_five_o:
x_in_o_two_four_o:

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

In [110]:
two_in_o_one_five_o.prove()

In [111]:
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

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

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

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

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

In [116]:
# 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]}:

In [117]:
# 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

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

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

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

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

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


… some upper bounds

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

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

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

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


### Testing the RealIntervalMembership.deduce_in_bool() method¶

In [127]:
InSet(x, IntervalOO(three, five)).deduce_in_bool()

In [128]:
InSet(x, IntervalOC(four, six)).deduce_in_bool()

In [129]:
InSet(x, IntervalCO(seven, nine)).deduce_in_bool()

In [130]:
InSet(x, IntervalCC(one, six)).deduce_in_bool()


### Testing the RealIntervalNonmembership.deduce_in_bool() method¶

In [131]:
NotInSet(x, IntervalOO(three, five)).deduce_in_bool()

In [132]:
NotInSet(x, IntervalOC(four, six)).deduce_in_bool()

In [133]:
NotInSet(x, IntervalCO(seven, nine)).deduce_in_bool()

In [134]:
NotInSet(x, IntervalCC(one, six)).deduce_in_bool()


### Testing the RealIntervalNonmembership.deduce_real_element_bounds() method¶

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

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

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

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

In [139]:
# 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))])

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

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


### Testing the automation for RealIntervalNonmembership¶

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

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

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

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


### Testing the automation for real IntervalXX subset relationships¶

In [146]:
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:

In [147]:
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

In [ ]:



### Number set membership demonstrations¶

In [148]:
InSet(InSet(r, Real), Boolean).prove()

In [149]:
InSet(InSet(r, RealNonZero), Boolean).prove()

In [150]:
InSet(InSet(r, RealPos), Boolean).prove()

In [151]:
InSet(InSet(r, RealNeg), Boolean).prove()

In [152]:
InSet(InSet(r, RealNonNeg), Boolean).prove()

In [153]:
InSet(InSet(r, RealNonPos), Boolean).prove()

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

In [179]:
%end demonstrations