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

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.

SetOfAll((a, b), frac(a, b), conditions=[NotEquals(b, zero)], domain=Integer)

SetOfAll((a, b), frac(a, b), conditions=[NotEquals(b, zero)], domains=(Integer, Real))

Forall((a, b), frac(a, b), domains=(Integer, Real))

Some example expressions to use for testing:

positive_reals = SetOfAll(x, x, condition=greater(x, zero), domain=Real)

positive_reals:

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:

squares_of_unit_interval.instance_var

# instance_vars is no longer an attribute, but all_instance_vars() will work
squares_of_unit_interval.all_instance_vars()

squares_of_unit_interval.instance_param_or_params

squares_of_unit_interval.all_conditions()

squares_of_unit_interval.conditions

positive_reals.conditions

positive_reals.domain

len(positive_reals.explicit_conditions())

1

And(*squares_of_unit_interval.explicit_conditions())

positive_reals.effective_condition()

squares_of_unit_interval.all_domains()

len(squares_of_unit_interval.all_instance_vars())

1

squares_of_unit_interval.instance_element

Function(Q, squares_of_unit_interval.all_instance_vars())

Testing SetOfAll.unfold_membership() method

InSet(a, positive_reals)

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

%end demonstrations