# Demonstrations for the theory of proveit.logic.sets.comprehension¶

In [1]:
import proveit
from proveit import a, b, x, y, Q, Function
from proveit.logic import And, Forall, InSet, NotEquals, SetOfAll
from proveit.numbers import (
zero, one, two, Exp, frac, greater, greater_eq, LessEq, Integer, Real)
%begin demonstrations

Just some formatting checks below. Nothing important. Remove them when we put in something serious.

In [2]:
SetOfAll((a, b), frac(a, b), conditions=[NotEquals(b, zero)], domain=Integer)
In [3]:
SetOfAll((a, b), frac(a, b), conditions=[NotEquals(b, zero)], domains=(Integer, Real))
In [4]:
Forall((a, b), frac(a, b), domains=(Integer, Real))

Some example expressions to use for testing:

In [5]:
positive_reals = SetOfAll(x, x, condition=greater(x, zero), domain=Real)
positive_reals:
In [6]:
squares_of_unit_interval = SetOfAll(x, Exp(x, two), conditions=[greater_eq(x, zero), LessEq(x, one)], domain=Real)
squares_of_unit_interval:

Grabbing pieces of the comprehension:

In [7]:
squares_of_unit_interval.instance_var
In [8]:
# instance_vars is no longer an attribute, but all_instance_vars() will work
squares_of_unit_interval.all_instance_vars()
In [9]:
squares_of_unit_interval.instance_param_or_params
In [10]:
squares_of_unit_interval.all_conditions()
In [11]:
squares_of_unit_interval.conditions
In [12]:
positive_reals.conditions
In [13]:
positive_reals.domain
In [14]:
len(positive_reals.explicit_conditions())
1
In [15]:
And(*squares_of_unit_interval.explicit_conditions())
In [16]:
positive_reals.effective_condition()
In [17]:
squares_of_unit_interval.all_domains()
In [18]:
len(squares_of_unit_interval.all_instance_vars())
1
In [19]:
squares_of_unit_interval.instance_element
In [20]:
Function(Q, squares_of_unit_interval.all_instance_vars())

### Testing SetOfAll.unfold_membership() method¶

In [21]:
InSet(a, positive_reals)
In [22]:
# still developing the unfold_membership() method
try:
positive_reals.unfold_membership(a, assumptions=[InSet(a, positive_reals)])
except Exception as the_error:
print("Exception: {}".format(the_error))
(1) SetOfAll.unfold_membership(): inside first if.
_Q_op =
_Q_op_sub =
SetOfAll.unfold_membership(): end
Exception: @prover method <function SetOfAll.unfold_membership at 0x7f4199096ae8> is expected to return a proven Judgment, not None of type <class 'NoneType'>.
In [ ]:

In [23]:
%end demonstrations