Demonstrations for the theory of proveit.logic.sets.inclusion¶
import proveit
from proveit import free_vars, InstantiationFailure, ProofFailure, used_vars
from proveit import a, b, c, d, e, f, x, y, A, B, C, D, E, F, X, Y, Px
from proveit.logic import (Equals, Forall, Exists, Implies, InSet, Not,
NotEquals, NotInSet, Set)
from proveit.logic import (Intersect, SetEquiv, NotProperSubset,
SubsetEq, NotSubsetEq, not_superset_eq,
ProperSubset, proper_superset, not_proper_superset,
SubsetProper, StrictSubset, superset_eq)
from proveit.numbers import zero, one, two, three, four, five
from proveit.numbers import (Integer, Natural, NaturalPos, Real,
RealNeg, RealPos)
from proveit.numbers.number_sets.real_numbers import int_within_real
from proveit.logic.sets.inclusion import (
subset_eq_def, proper_subset_def, not_proper_subset_def, unfold_not_subset_eq)
from proveit.logic.sets.inclusion import fold_not_subset_eq, fold_subset_eq
%begin demonstrations
Inclusion $\in$, $\subset$, $\subseteq$, $\supset$, $\supseteq$¶
Simple Expressions involving Membership $(\in)$, Subsets $(\subset, \subseteq)$, and Supersets $(\supset, \supseteq )$
Common Attributes of the Subset $(\subseteq)$ Expression
Axioms
Theorems & Conjectures
Further Demonstrations
- $(x\in A)\wedge(A\subset B)\Rightarrow (x\in B)$
- $\forall_{x\in A}(x\in B) \Rightarrow (A \subseteq B)$
- $(x\in B)\wedge(A\supset B)\Rightarrow (x\in A)$
- $\forall_{x\in Y}(x\in X) \Rightarrow (X \supseteq Y)$
- Folding and Unfolding the Definitions of $\not\subseteq$ and $\not\supseteq$
- Containment Reversals (such as $A \subset B \Rightarrow B \supset A$)
- Deducing $\{1, 3\} \subset \{1, 2, 3, 4, 5\}$
- Manually Proving $\{1, 3, 5\} \subseteq \{1, 2, 3, 4, 5\}$
- Deducing quantification via inclusion
Introduction ¶
Set membership (*e.g.*, $x \in S$), subset ($A \subset B$), and superset ($B \supset A$) concepts are often critical in proofs, either as goals in themselves or as conditions or assumptions appearing in a proof. This ``_demonstrations_`` notebook explores subset ($\subset$, $\subseteq$), and superset ($\supset$, $\supseteq$) expressions and related methods. (Set membership ($\in$) itself is explored more thoroughly in its own ``_demonstrations_`` notebook in the ``proveit.logic.sets.membership`` theory.)
Simple Expressions Involving Membership ($\in$), Subsets ($\subset$, $\subseteq$), and Supersets ($\supset$, $\supseteq$) ¶
It is straightforward to construct membership, subset, and superset expressions. Here are some basic examples of such expressions:
# a simple set membership claim
InSet(x, A)
# proper subset claims, 3 different options
example_1, example_2, example_3 = ProperSubset(A, B), SubsetProper(A, B), StrictSubset(A, B)
# improper subset
SubsetEq(B, C)
# proper superset (a style variant of a ProperSubset)
proper_superset(C, B)
# improper superset (a style variant of SubsetEq)
superset_eq(C, B)
# not a proper subset
NotProperSubset(D, E)
# not a subset
NotSubsetEq(D, E)
# not a proper superset (a style variant of NotProperSubset)
not_proper_superset(D, E)
# not a superset (a style variant of NotSubsetEq)
not_superset_eq(D, E)
At the time of this writing, portions of Prove-It code might still have the more ambiguous `Subset` notation or terminology, but in general we will use `SubsetEq()` to form general or “improper” subset expressions (*e.g.*, $A \subseteq$ B) and `ProperSubset()` or `SubsetProper()` to form “proper” or “strict” subset expressions (such as $A \subset$ B), with similar notation used for the negations.
Common Attributes of a Subset expression ¶
Let's define a simple example subset expression, $(A \cap B) \subseteq B$, and look at some of its attributes. (The results should be similar for proper subset ($\subset$) and the various supersets ($\supset$, $\supseteq$) and their negations.)
# define a subset expression
A_intersect_B_subset_of_B = SubsetEq(Intersect(A, B), B)
We can look at the construction of such an expression by calling expr_info() to see the tabular representation of the expression's underlying directed acyclic graph (DAG) representation:</font>
A_intersect_B_subset_of_B.expr_info()
| core type | sub-expressions | expression | |
|---|---|---|---|
| 0 | Operation | operator: 1 operands: 2 | |
| 1 | Literal |  | |
| 2 | ExprTuple | 3, 7 |  |
| 3 | Operation | operator: 4 operands: 5 |  |
| 4 | Literal |  | |
| 5 | ExprTuple | 6, 7 |  |
| 6 | Variable |  | |
| 7 | Variable |  |
We can access the left-hand and right-hand sides of such expressions, as well as the specific operator:
A_intersect_B_subset_of_B.lhs
A_intersect_B_subset_of_B.rhs
A_intersect_B_subset_of_B.operator
We can get both sides of the expression simultaneously (the operands of the $\subseteq$ operator) as a tuple of expressions. We can also get a list of the variables and a separate list of the *free* variables in the expression (of course, in this expression, all the variables are also free variables):
A_intersect_B_subset_of_B.operands
used_vars(A_intersect_B_subset_of_B)
free_vars(A_intersect_B_subset_of_B)
By the way, notice that our expression $(A \cap B) \subseteq B$ is always true, and Prove-It can automatically prove this:
A_intersect_B_subset_of_B_judgment = A_intersect_B_subset_of_B.prove()
A peek at the proof shows that Prove-It has applied the fold_subset_eq theorem:
$\forall_{A,B} \left([\forall_{x\in A}(x\in B)] \implies (A \subseteq B)\right)$
by using a suitable instantiation to get something like this:
$[\forall_{x\in A\cap B}(x\in B)] \implies ((A\cap B) \subseteq B)$
See Line 3 in the proof below for the fold_subset_eq theorem, then Line 1 for the instantiation step.</font>
A_intersect_B_subset_of_B_judgment.proof()
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | instantiation | 1, 2 | ⊢ | |
: , : ,  :  | ||||
| 1 | theorem | ⊢  | ||
| proveit.logic.sets.inclusion.fold_subset_eq | ||||
| 2 | generalization | 3 | ⊢  | |
| 3 | instantiation | 4, 5 |  ⊢  | |
:  , : | ||||
| 4 | theorem | ⊢  | ||
| proveit.logic.booleans.conjunction.right_from_and | ||||
| 5 | instantiation | 6, 7, 8, 9 | ⊢  | |
 :  , : , : | ||||
| 6 | conjecture | ⊢  | ||
| proveit.logic.sets.intersection.membership_unfolding | ||||
| 7 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.posnat2 | ||||
| 8 | instantiation | 10 | ⊢  | |
 : ,  : | ||||
| 9 | assumption | ⊢ | ||
| 10 | conjecture | ⊢  | ||
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq | ||||
And we can ``unfold()`` the subset expression to produce an equivalent judgment in terms of set memberships. Notice here that the ``unfold()`` process *automatically* produces a Known Truth instead of just another expression (and it would have done this even if we had not previously proven the expression to be true):
# the original expression
A_intersect_B_subset_of_B
# unfold to express in terms of set memberships
A_intersect_B_subset_of_B.unfold()
# unfold to express in terms of set memberships
# and simultaneously change the instance variable
A_intersect_B_subset_of_B.unfold(elem_instance_var=y)
Axioms ¶
The ``axioms`` for containment establish the basic definitions of subset ($\subseteq$), proper subset ($\subset$), proper superset ($\supset$), *etc.* A few of the axioms are shown below as illustrations (the rest can be accessed on the [containment axioms](./_axioms_.ipynb) page.)
# def of (non-proper) subset
subset_eq_def
# def of (proper) subset
proper_subset_def
# negation of (proper) subset
not_proper_subset_def
Theorems & Conjectures¶
The `logic.sets.inclusion` theory already has a substantial number of related theorems and conjectures established, covering a wide range of containment-related concepts, most of which would typically be used implicitly behind-the-scenes when utilizing the various related containment class methods instead of being used directly and explicitly in theorem form. The theorems and conjectures cover topics such as transitivity of containment relations, folding/unfolding of containment definitions, relaxation of strict containments, and containment claims being in the Boolean set. Some illustrative examples of the theorems are shown below, and the remainder can be found in the [containment theorems notebook](./\_theorems\_.ipynb).
from proveit.logic.sets.inclusion import (
unfold_subset_eq, fold_subset_eq, subset_eq_reflexive,
relax_proper_subset, transitivity_subset_eq_subset_eq, proper_subset_is_bool)
# if A is a (non-strict) subset of B, then
# every element of A is also an element of B
unfold_subset_eq
# if every element of A is also an element of B,
# then A is a (non-strict) subset of B
fold_subset_eq
# a set is always a (non-strict) subset of itself
subset_eq_reflexive
# we can "relax" a strict subset claim into an improper subset claim
relax_proper_subset
# the subset relation is transitive
transitivity_subset_eq_subset_eq
# a subset claim is a Boolean value
proper_subset_is_bool
Demonstrations ¶
We begin with some simple expressions involving well-known numerical sets. Many standard subset and membership relationships involving common numerical sets are available as theorems, with many such theorems automatically imported and utilized. For example:
ProperSubset(NaturalPos, Natural).prove()
ProperSubset(Natural, Integer).prove()
ProperSubset(NaturalPos, Integer).prove()
InSet(one, Natural).prove()
Given that $1 \in \mathbb{N}$ and $\mathbb{N} \subset \mathbb{Z}$, we should be able to show that $1 \in \mathbb{Z}$, and Prove-It can do this automatically:
one_is_an_integer = InSet(one, Integer).prove()
In the detailed proof of that conclusion, Prove-It instantiates the unfold_subset_eq theorem
$\forall_{A,B\rvert A\subseteq B} \left[ \forall_{x \in A} (x \in B) \right]$
to eliminate both universal quantifiers by instantiating $A$ to $\mathbb{N^{+}}$, $B$ to $\mathbb{Z}$, and $x$ to $1$. The theorem appears in Line 1 in the proof below. The ''fold'' and ''unfold'' language often appears in theorems that ''fold'' or ''unfold'' axiomatic definitions, and here in the cases of subsets ($\subseteq$) and supersets ($\supseteq$) move between set-containment versus element-membership notation.
Notice also the relax_subset theorem cited on line 4 and instantiated on line 2, illustrating the use of another containment-related theorem in the proof process.
</font>
one_is_an_integer.proof()
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | instantiation | 1, 2, 3 | ⊢ | |
:  , :  , :  | ||||
| 1 | theorem | ⊢  | ||
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset | ||||
| 2 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.nat_within_int | ||||
| 3 | theorem | ⊢  | ||
| proveit.numbers.numerals.decimals.nat1 | ||||
As an exercise, we can obtain the result more generally for arbitrary sets $X$ and $Y$ any time we assume $X \subseteq Y$ and $x \in X$:
# Define some conditions
x_in_x, x_subset_eq_ofy, x_in_y = InSet(x, X), SubsetEq(X, Y), InSet(x, Y)
# bundle the first 2 conditions into a list of assumptions
demo_01_assumptions = [x_in_x, x_subset_eq_ofy]
# prove set membership based on the assumptions
x_in_y_k_t = x_in_y.prove(assumptions=demo_01_assumptions)
, ⊢ As an extra step, we can also re-express that result in terms of implications:
x_in_y_k_t.as_implication(hypothesis=SubsetEq(X, Y))
x_in_y_k_t.as_implication(hypothesis=InSet(x, X))
# define our conclusion
CSubsetOfD = SubsetEq(C, D)
# define our assumption (or perhaps this would be proven elsewhere first)
demo_02_assumptions = [Forall(x, InSet(x,D), domain=C)]
# prove the conclusion from the assumptions
CSubsetOfD.prove(assumptions=demo_02_assumptions)
And we can re-express that judgment as a logical implication:
CSubsetOfD.prove(assumptions=demo_02_assumptions).as_implication(*demo_02_assumptions)
Or we could have proven the implication form directly (shown here with new set variables $E$ and $F$ so as not to simply derive from the previous result):
an_implication = Implies(Forall(x, InSet(x,F), domain=E),SubsetEq(E,F))
from proveit import defaults
defaults.assumptions = an_implication.antecedent.conditions
an_implication.antecedent.instance_expr.readily_provable()
an_implication.prove()
This is a variant of Demo (1) above. When we know that $x$ is in $B$ and $A$ contains $B$, then $x$ must also be in $A$.
Let's define some useful expressions, let Prove-It prove the implication, then look at the proof:
# define some expressions
x_in_a, x_in_b, ASupersetOfB = InSet(x, A), InSet(x, B), proper_superset(A, B)
# establish the Known Truth
x_in_a_kt = x_in_a.prove(assumptions=[x_in_b, ASupersetOfB])
, ⊢ In the proof, we see the relaxation theorem taking $A \supset B$ to $A \supseteq B$, and then the reversal theorem taking $A \supseteq B$ to $B \subseteq A$, then proceeding as it would for the example in Demo (1) earlier:
# take a look at the proof:
x_in_a_kt.proof()
As in Demo 1, we can re-express our judgment as a logical implication:
# our judgment
x_in_a_kt
, ⊢
# one option for the implication
x_in_a_kt.as_implication(hypothesis=x_in_b)
# another option for the implication
x_in_a_kt.as_implication(hypothesis=ASupersetOfB)
When we know that $x$ is in $X$ whenever $x$ is in $Y$, we have $Y \subseteq X$ (i.e., $X$ contains $Y$ or $Y$ is a subset of $X$). That is a theorem in Prove-It that can be instantiated to prove a containment or superset relationship for two arbitrary sets given the right conditions:
# our fold_supset_eq theorem
fold_subset_eq
Forall(x, InSet(x, Y), domain=A)
# instantiate the fold_supset_eq theorem
fold_subset_eq_inst = fold_subset_eq.instantiate({A:Y, B:X}, assumptions=[Forall(x, InSet(x, X), domain=Y)])
⊢ 
fold_subset_eq_inst_rev = fold_subset_eq_inst.with_styles(direction='reversed')
⊢ 
fold_subset_eq_inst_rev.as_implication(hypothesis=Forall(x, InSet(x, X), domain=Y))
Alternatively we can prove the rhs of the implication given the antecedent as an assumption.
# peel off our desired conclusion:
XSupersetOfY = fold_subset_eq_inst.expr.with_styles(direction='reversed')
# prove our conclusion based on the antecedent
XSupersetOfY_jdgmt = XSupersetOfY.prove(
assumptions=[Forall(x, InSet(x, X), domain=Y)]).as_implication(
hypothesis=Forall(x, InSet(x, X), domain=Y))
We can also achieve the same thing quite directly (here using $C$ and $D$ to keep it analogous but distinct from our earlier work above):
superset_eq(C, D).prove(
assumptions=[Forall(x, InSet(x, C), domain=D)]).as_implication(
hypothesis=Forall(x, InSet(x, C), domain=D))
$\not\subseteq$ is axiomatically defined by $\forall_{A, B} (A\not\subseteq B) = \neg(A \subseteq B)$, and we have theorems to automatically fold and unfold the definition, allowing us to express and use the definition in a variety of ways. For example, we can automatically derive the statements that $\{C\not\subseteq D\} \vdash \neg(C\subseteq D)$, and $\{\neg(C\subseteq D)\} \vdash C\not\subseteq D$
# temp_expr = NotSubsetEq(C, D)
# unfold_not_subset_eq
# unfold_not_subset_eq.instantiate({A: C, B: D}, assumptions=[NotSubsetEq(C, D)], auto_simplify=False)
# unfold the definition to produce a new judgment
NotSubsetEq(C, D).unfold(assumptions=[NotSubsetEq(C, D)])
# or automatically fold the definition when deriving the alternative judgment
NotSubsetEqKT = NotSubsetEq(C, D).prove(assumptions=[Not(SubsetEq(C, D))])
⊢ 
In the proof for that second derivation, we see the use of the ``fold_not_subset_eq`` theorem, which we can manually invoke and instantiate to accomplish the same thing:
# the theorem
fold_not_subset_eq
# instantiation
fold_not_subset_eq_spec = fold_not_subset_eq.instantiate({A:C, B:D}, assumptions=[Not(SubsetEq(C, D))])
⊢ We can look at the proof resulting from the earlier automated ``prove()`` approach and see the same steps reflected in the automation:
NotSubsetEqKT.proof()
And of course we have similar fold and unfold theorems for the negated superset or negated containment relation $\not\supseteq$. For example:
# unfold the definition to produce a new judgment
not_superset_eq(C, D).unfold(assumptions=[not_superset_eq(C, D)])
# or automatically fold the definition when deriving the alternative judgment
NotSupersetEqKT = not_superset_eq(C, D).prove(assumptions=[Not(superset_eq(C, D))])
⊢ 
We have a theorem, ``int_within_real``, that the integer numbers are a proper subset of the real numbers: $\mathbb{Z} \subset \mathbb{R}$:
int_within_real
We can create the equivalent superset expression, $\mathbb{R} \supset \mathbb{Z}$, and its proof is the same as that of $\mathbb{Z} \supset \mathbb{R}$ because Prove-It regards these as the same expression but presented with a different style.
reals_contain_integer_kt = proper_superset(Real, Integer).prove()
reals_contain_integer_kt.proof()
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.real_numbers.int_within_real | ||||
set_13, set_12345 = Set(one, three), Set(one, two, three, four, five)
and define the proper subset relationship between them:
set_13_properSubset_set_12345 = ProperSubset(set_13, set_12345)
set_13_properSubset_set_12345.prove()
But the enumerated Set class has some special machinery to help us out:
NotInSet(two, set_13).prove()
set_12345.deduce_enum_proper_subset(subset=set_13)
And a membership claim such as $2\in\{1, 2, 3, 4, 5\}$ can be proven automatically:
InSet(two, set_12345).prove()
Enumerated Sets and related axioms, theorems, conjectures, and methods are discussed in much more detail in the set_theory/enumeration theory and the [enumeration demonstrations page](../enumeration/\_demonstrations\_.ipynb) page.
Although the enumerated Set class has machinery to make subset deductions fairly easy (as seen above in Demo 7), it can be a useful exercise to consider a more manual approach. So let's consider a possible alternative effort to prove that $\{1, 3, 5\} \subseteq \{1, 2, 3, 4, 5\}$.
We begin by defining our enumerated Sets and the subset relationship:
set_135, set_12345 = Set(one, three, five), Set(one, two, three, four, five)
demo_08_subset = SubsetEq(set_135, set_12345)
It turns out that Prove-It can automatically prove that subset relationship for us. We can just call the following, which we've temporarily left commented-out for pedagogical purposes so its proof doesn't interfere with our looking at an alternative manual approach further below:
# demo_08_subset.prove()
Instead of allowing the automation to do it for us, and instead of utilizing the direct Set.deduce_enum_subset_eq() method, consider the subset_eq_def axiom, which provides a definition of what it means to say that one set is a (non-strict) subset of another:
from proveit.logic.sets.inclusion import subset_eq_def
subset_eq_def
We can instantiate the subset_eq_def axiom for our particular case:
subset_eq_def_specialized = subset_eq_def.instantiate(
{A:set_135, B:set_12345})
If we can prove the rhs of that instantiated form, we can use the equality to conclude the lhs. To get there, we consider the equivalence() method for set membership, which unfolds a set membership claim into a disjunction of equalities, like this:
InSmallerSetDef = InSet(x, set_135).definition()
# replaced by the definition() method above
# InSmallerSetDef = InSet(x, set_135).equivalence()
InLargerSetDef = InSet(x, set_12345).definition()
# replaced by the definition() method above
# InLargerSetDef = InSet(x, set_12345).equivalence()
We can show that the smaller disjunction $((x=1)\lor (x=3)\lor (x=5))$ logically implies the larger disjunction $((x=1)\lor (x=2)\lor (x=3)\lor (x=4)\lor (x=5))$, and thus that membership in $\{1, 3, 5\}$ implies membership in $\{1, 2, 3, 4, 5\}$. To get there, we proceed as follows:
# notice we can grab the disjunction expressions from the equivalence expressions above:
display(InSmallerSetDef.rhs)
display(InLargerSetDef.rhs)
We use the Or.conclude_via_some method to show that the smaller conjunction allows the derivation of the larger conjunction:
small_disj_gives_larger_disj = InLargerSetDef.rhs.conclude_via_some(
InSmallerSetDef.rhs, assumptions=[InSmallerSetDef.rhs])
⊢ Then re-express that judgment as an implication:
small_disj_implies_larger_disj = small_disj_gives_larger_disj.as_implication(
hypothesis=InSmallerSetDef.rhs)
Now we use our earlier equivalence definitions to back-substitute:
small_membership_implies_larger_disj = InSmallerSetDef.sub_left_side_into(small_disj_implies_larger_disj)
InLargerSetDef.sub_left_side_into(small_membership_implies_larger_disj)
This gives Prove-It all it needs to prove the rhs of our earlier instantiated axiom, $\forall_{x\in\{1, 3, 5\} } (x\in\{1, 2, 3, 4, 5\})$:
subset_eq_def_specialized_rhs_kt = subset_eq_def_specialized.rhs.prove()
And finally we can substitute in for that universally quantified expression our desired subset expression:
subset_eq_def_specialized.sub_left_side_into(subset_eq_def_specialized_rhs_kt)
Et voila! Although a bit effortful, and although Prove-It can accomplish the same deduction automatically in this case, the exercise is useful in illustrating a number of common steps and strategies, including an interplay between manual steps and automation, the instantiation of axioms and theorems, and the use of substitutions (in this case via `sub_left_side_into()`) between established judgments.
Miscellaneous Testing¶
The material below was developed to test various containment-related methods. Some of this material could be integrated into the `_demonstrations_` page eventually and/or deleted as development continues.
Some Example Sets For Testing¶
from proveit.numbers import one, two, three, four, five, six, seven
# define some enumerated Sets for use in testing, containing literals
set_123, set_12345, set_1234567 = (
Set(one, two , three),
Set(one, two , three, four, five),
Set(one, two , three, four, five, six, seven))
from proveit import a, b, c, d, e
# define some enumerated Sets for use in testing, containing variables
set_abc, set_abcde = (
Set(a, b, c),
Set(a, b, c, d, e))
# recall some other basic sets already defined:
Integer, Natural, NaturalPos, Real
Testing the ProperSubset class methods¶
<font size =3>The ProperSubset class has the following class methods:
unfold(self, **defaults_config)
derive_relaxed(self, **defaults_config)
derive_superset_membership(self, element, **defaults_config)
apply_transitivity(self, other, **defaults_config)
deduce_in_bool(self, **defaults_config)
# define a few proper subset relations for testing
set_123_properSubset_set_12345, set_12345_properSubset_set_1234567 = (
ProperSubset(set_123, set_12345),
ProperSubset(set_12345, set_1234567))
# define a few proper subset relations for testing
set_abc_properSubset_set_abcde = ProperSubset(set_abc, set_abcde)
ProperSubset.reversed()¶
# if A is a proper subset of B, then B is a proper superset of A
set_12345.deduce_enum_proper_subset(subset=set_123)
set_123_properSubset_set_12345.reversed()
set_abcde.deduce_enum_proper_subset(subset=set_abc, assumptions=[NotInSet(d, set_abc)])
set_abc_properSubset_set_abcde.reversed()
ProperSubset.derive_relaxed()¶
set_123_properSubset_set_12345.derive_relaxed()
set_abc_properSubset_set_abcde.derive_relaxed(assumptions=[NotInSet(d, set_abc)])
# derive_relaxed() method only works for actual proper subsets.
# If the proper subset is not true or not provably true, derive_relaxed() will fail:
try:
ProperSubset(Set(a, b), Set(a, b, c)).derive_relaxed()
assert False, "Expecting a ProofFailure. Should not make it to this point."
except ProofFailure as the_error:
print("ProofFailure: {}".format(the_error))
# But if we first establish the proper subset as a judgment
# (with the appropriate assumptions) …
Set(a, b, c).deduce_enum_proper_subset(subset=Set(a, b), assumptions=[NotInSet(c, Set(a, b))])
# then we can relax as expected:
ProperSubset(Set(a, b), Set(a, b, c)).derive_relaxed(assumptions=[NotInSet(c, Set(a, b))])
ProperSubset.apply_transitivity()¶
# establish a proper subset judgement:
set_12345.deduce_enum_proper_subset(subset=set_123)
# establish a related proper subset judgement:
set_1234567.deduce_enum_proper_subset(subset=set_12345)
# use transitivity to go from first set to 3rd set:
set_123_properSubset_set_12345.apply_transitivity(set_12345_properSubset_set_1234567)
# This process can work more generally.
# First define some set relations for convenience:
A_properSubset_B, B_subset_eq_C, B_equiv_D, C_superset_eq_B, F_superset_B = (
ProperSubset(A, B), SubsetEq(B, C), SetEquiv(B, D),
superset_eq(C, B), proper_superset(F, B))
A_properSubset_B.apply_transitivity(
B_subset_eq_C, assumptions=[ProperSubset(A, B), SubsetEq(B, C)])
, ⊢ 
# transitivity when other relation is an equality
A_properSubset_B.apply_transitivity(
B_equiv_D, assumptions=[A_properSubset_B, B_equiv_D])
, ⊢ 
# transitivity when other relation is a SupersetEq
# ProperSubset(A, B) and SupersetEq(C, B)?
A_properSubset_B.apply_transitivity(
C_superset_eq_B, assumptions=[A_properSubset_B, C_superset_eq_B])
, ⊢
# transitivity when other relation is a Superse
# SubsetEq(A, B) and ProperSuperset(F, B)?
A_properSubset_B.apply_transitivity(
F_superset_B, assumptions=[A_properSubset_B, F_superset_B])
, ⊢ 
ProperSubset.deduce_in_bool()¶
# Proper subset claims are Boolean values
A_properSubset_B.deduce_in_bool()
# Proper subset claims are Boolean values
set_abc_properSubset_set_abcde.deduce_in_bool()
# False (or unknown verity) proper subset claims are also Boolean values
ProperSubset(Set(a, b, c, d, e), Set(a, b, c)).deduce_in_bool()
Testing the SubsetEq class methods¶
<font size =3>The SubsetEq class has the following class methods:
- reversed(self)
- conclude(self, assumptions=USE_DEFAULTS)
- conclude_via_equality(self, assumptions)
- unfold(self, elem_instance_var=x, assumptions=USE_DEFAULTS)
- derive_superset_membership(self, element, assumptions=USE_DEFAULTS)
- conclude_as_folded(self, elem_instance_var=x, assumptions=USE_DEFAULTS)
- apply_transitivity(self, other, assumptions=USE_DEFAULTS)
- deduce_in_bool(self, assumptions=USE_DEFAULTS)
SubsetEq.conclude()¶
# Very simple subset relations can be automatically concluded
SubsetEq(Set(one, two, four), Set(one, two, four)).conclude()
# Very simple subset relations can be automatically concluded
SubsetEq(A, A).conclude()
SubsetEq(Set(one, two, four), Set(one, two, three, four, five)).conclude_as_folded()
# Simple subset relation between two enumerated sets
SubsetEq(Set(one, two, four), Set(one, two, three, four, five)).conclude()
# Simple subset relation between two enumerated sets
SubsetEq(Set(c, b, a), Set(f, e, c, b, a)).conclude()
SubsetEq(Set(one, two), Set(a, b)).conclude(
assumptions=[Equals(Set(one, two), Set(a, b))])
# The example above works even if the order of elements
# is different for the two sets of values
SubsetEq(Set(one, two), Set(a, b)).conclude(
assumptions=[Equals(a, two), Equals(b, one)])
, 
⊢ 
# Some issue here involving SetOfAll sets;
# the set_of_all.py and sets/comprehension package must be updated
# from proveit.logic import NotEquals, SetOfAll
# non_zero_ints = SetOfAll(x, x, conditions=[NotEquals(x, zero)], domain=Integer)
# Some issue here involving SetOfAll sets;
# the set_of_all.py and sets/comprehension package must be updated
# SubsetEq(non_zero_ints, Integer).conclude()
SubsetEq.conclude_via_equality()¶
SubsetEq(A, B).conclude_via_equality(assumptions=[Equals(A, B)])
The ability to prove the following using 'simplify_with_known_evaluations' was lost when implementing readily_provable¶
Issue #296 (Equivalence classes with canonical forms) is perhaps the proper way to get these working again, and 'simplify_with_known_evaluations' would not be needed.
# SubsetEq(Set(one, two), Set(a, b)).conclude_via_equality(
# assumptions=[Equals(a, one), Equals(b, two)],
# simplify_with_known_evaluations=True)
# SubsetEq(Set(one, two), Set(a, b)).conclude_via_equality(
# assumptions=[Equals(a, two), Equals(b, one)],
# simplify_with_known_evaluations=True)
SubsetEq.conclude_via_equivalence()¶
SubsetEq(B, B).conclude_via_equivalence()
SubsetEq(Set(b, two, d), Set(b, two, d)).conclude_via_equivalence()
SubsetEq(A, B).conclude_via_equivalence(assumptions=[SetEquiv(A, B)])
# SubsetEq(Set(one, two), Set(a, b)).conclude_via_equivalence(
# assumptions=[Equals(a, one), Equals(b, two)],
# simplify_with_known_evaluations=True)
SubsetEq(Set(one, two), Set(a, b)).conclude_via_equivalence(
assumptions=[SetEquiv(Set(one, two), Set(a, b))])
SubsetEq.conclude_as_folded()¶
from proveit import g
SubsetEq(Set(b, g), Set(b, d, g)).conclude_as_folded(
assumptions=[Forall(x, InSet(x, Set(b, d, g)), domain=Set(b, g))])
SubsetEq(C, D).conclude_as_folded(
assumptions=[Forall(x, InSet(x, D), domain=C)])
SubsetEq(Set(b, g), Set(b, d, g)).conclude_as_folded(
assumptions=[Forall(x, InSet(x, Set(b, d, g)), domain=Set(b, g))])
SubsetEq(B, A).conclude_as_folded(
assumptions=[Forall(x, InSet(x, A), domain=B)])
SubsetEq.unfold()¶
SubsetEq(set_123, set_12345).unfold()
# Works, but often have to explicitly pre-establish that
# the subset_eq relationship is actually true
Set(a, one, b, c).deduce_enum_subset_eq(subset=Set(a, one, b))
SubsetEq(Set(a, one, b), Set(a, one, b, c)).unfold()
SubsetEq(Set(one, three, four), Set(six, one, four, three)).unfold()
SubsetEq(Set(a, one, b), Set(a, one, b, two)).unfold()
SubsetEq(Set(a, one, b), Set(b, a, one, c)).unfold()
SubsetEq.derive_superset_membership()¶
# given a known subset_eq relationship, and an element in the
# subset, derive the element as being in the superset
SubsetEq(set_123, set_12345).derive_superset_membership(two)
SubsetEq(Set(a, one, b), Set(a, one, b, c)).derive_superset_membership(a)
# and this works more generally, where we can assume an elem in the subset
from proveit import f
Set(a, b, c, d).deduce_enum_subset_eq(subset=set_abc)
SubsetEq(Set(a, b, c), Set(a, b, c, d)).derive_superset_membership(f, assumptions=[InSet(f, set_abc)])
SubsetEq.derive_subset_nonmembership()¶
# given a known SubsetEq relationship, and an element NOT in the superset,
# derive the element as NOT being in the subset
SubsetEq(set_123, set_12345).derive_subset_nonmembership(six)
SubsetEq(Set(a, one, b), Set(a, one, b, c)).derive_subset_nonmembership(
two, assumptions=[NotEquals(a, two), NotEquals(b, two), NotEquals(c, two)])
, 
, 
⊢ 
# and this works more generally, where we can assume some elem not in the superset
# which means it must not be in the subset
from proveit import f
Set(a, b, c, d).deduce_enum_subset_eq(subset=set_abc)
SubsetEq(Set(a, b, c), Set(a, b, c, d)).derive_subset_nonmembership(f, assumptions=[NotInSet(f, Set(a, b, c, d))])
SubsetEq.apply_transitivity()¶
# establish a subset_eq judgement:
set_123_subset_eq_set_12345 = set_12345.deduce_enum_subset_eq(subset=set_123)
# establish a related proper subset judgement:
set_12345_subset_eq_set_1234567 = set_1234567.deduce_enum_proper_subset(subset=set_12345)
# use transitivity to go from first set to 3rd set
# (even though using expressions, the expressions have to be true or provable)
SubsetEq(set_123, set_12345).apply_transitivity(SubsetEq(set_12345, set_1234567))
# this process can work more generally:
A_subset_eq_B, B_subset_eq_C, B_equals_D, D_equals_B, C_superset_eq_B, F_superset_B = (
SubsetEq(A, B), SubsetEq(B, C), Equals(B, D), Equals(D, B),
superset_eq(C, B), proper_superset(F, B))
A_subset_eq_B.apply_transitivity(
B_subset_eq_C, assumptions=[A_subset_eq_B, B_subset_eq_C])
, ⊢ 
A_subset_eq_B.apply_transitivity(
B_equals_D, assumptions=[A_subset_eq_B, B_equals_D])
, ⊢ 
A_subset_eq_B.apply_transitivity(
B_equiv_D, assumptions=[A_subset_eq_B, B_equiv_D])
, ⊢
A_subset_eq_B.apply_transitivity(
D_equals_B, assumptions=[A_subset_eq_B, D_equals_B])
, ⊢
# SubsetEq(A, B) and SupersetEq(C, B)?
A_subset_eq_B.apply_transitivity(
C_superset_eq_B, assumptions=[A_subset_eq_B, C_superset_eq_B])
, ⊢
# SubsetEq(A, B) and proper_superset(F, B)
A_subset_eq_B.apply_transitivity(
F_superset_B, assumptions=[A_subset_eq_B, F_superset_B])
, ⊢
SubsetEq.deduce_in_bool()¶
# A subset_eq B should be a Boolean
SubsetEq(A, B).deduce_in_bool()
SubsetEq(Set(a, b, c), Set(a, b, c, d)).deduce_in_bool()
# And the SubsetEq claim is Boolean regardless of whether it's True or not
SubsetEq(Set(a, b, c, d), Set(a, b, c)).deduce_in_bool()
Testing the ProperSubset class methods in the proper_superset style¶
<font size =3>Again, the ProperSubset class has the following class methods:
- reversed(self)
- derive_relaxed(self, assumptions=USE_DEFAULTS)
- apply_transitivity(self, other, assumptions=USE_DEFAULTS)
- deduce_in_bool(self, assumptions=USE_DEFAULTS)
# define a few proper superset relations for testing
set_13, set_134, set_1346 = (
Set(one, three), Set(one, three, four), Set(one, three, four, six))
set_134_properSuperset_set_13, set_1346_properSuperset_set_134 = (
proper_superset(set_134, set_13), proper_superset(set_1346, set_134))
# define a few proper superset relations for testing
from proveit import g
set_bc, set_bcf, set_bcdfg = Set(b, c), Set(b, c, f), Set(b, c, d, f, g)
set_bcf_properSuperset_set_bc, set_bcdfg_properSuperset_set_bcf = (
proper_superset(set_bcf, set_bc), proper_superset(set_bcdfg, set_bcf))
# define a few subset relations for testing (when a reverse is desired)
from proveit import g
set_bc, set_bcf, set_bcdfg = Set(b, c), Set(b, c, f), Set(b, c, d, f, g)
set_bc_properSubset_set_bcf, set_bcf_subset_eq_set_bcdfg = (
ProperSubset(set_bc, set_bcf), SubsetEq(set_bcf, set_bcdfg))
proper_superset.unfold()¶
# here we feed the (True) superset relation in as an assumption
proper_superset(Set(six, four, two), Set(two, six)).unfold(
assumptions=[proper_superset(Set(six, four, two), Set(two, six))],
auto_simplify=False)
# but we could first manually establish the relation as proven:
Set(six, four, two).deduce_as_proper_superset_of(subset=Set(two, six))
# then the unfold can occur without the extra assumption:
proper_superset(Set(six, four, two), Set(two, six)).unfold(auto_simplify=False)
# more generally
proper_superset(Set(a, one, b, two), Set(a, one, b)).unfold(
assumptions=[proper_superset(Set(a, one, b, two), Set(a, one, b))],
auto_simplify=False)
# more generally
proper_superset(Set(a, one, b, c), Set(a, one, b)).unfold(
assumptions=[proper_superset(Set(a, one, b, c), Set(a, one, b))],
auto_simplify=False)
proper_superset.derive_relaxed()¶
# Notice that the relaxed relation maintains the superset
# notation rather than reverting to the subset notation
set_1346_properSuperset_set_134.derive_relaxed(
assumptions=[set_1346_properSuperset_set_134])
# Notice that the relaxed relation maintains the superset
# notation rather than reverting to the subset notation
set_bcdfg_properSuperset_set_bcf.derive_relaxed(
assumptions=[set_bcdfg_properSuperset_set_bcf])
proper_superset.derive_superset_membership()¶
proper_superset(B, A).derive_superset_membership(a, assumptions=[proper_superset(B, A), InSet(a, A)])
, 
⊢ 
proper_superset(set_12345, set_123).derive_superset_membership(two)
proper_superset.apply_transitivity()¶
set_12345_ProperSuperset_set_13 = set_12345.deduce_as_proper_superset_of(subset=Set(one, three))
set_1234567_ProperSuperset_set_12345 = set_1234567.deduce_as_proper_superset_of(subset=set_12345)
# use transitivity to go from largest set to smallest set
# (even though using expressions, the expressions have to be true or provable)
set_1234567_ProperSuperset_set_12345.apply_transitivity(set_12345_ProperSuperset_set_13.expr)
# this process can work more generally:
A_properSuperset_B, B_properSuperset_C, B_equals_D, C_properSubset_B, C_subset_eq_D = (
proper_superset(A, B), proper_superset(B, C), Equals(B, D),
ProperSubset(C, B), SubsetEq(C, D))
A_properSuperset_B.apply_transitivity(
B_properSuperset_C, assumptions=[A_properSuperset_B, B_properSuperset_C])
, ⊢ 
A_properSuperset_B.apply_transitivity(
B_equals_D, assumptions=[A_properSuperset_B, B_equals_D])
, ⊢ 
A_properSuperset_B.apply_transitivity(
D_equals_B, assumptions=[A_properSuperset_B, D_equals_B])
, ⊢
# Also works when the 'other' needs reversed
A_properSuperset_B.apply_transitivity(
C_properSubset_B, assumptions=[A_properSuperset_B, C_properSubset_B])
, ⊢
proper_superset.deduce_in_bool()¶
# proper_superset claims are Boolean values
proper_superset(A, B).deduce_in_bool()
# superset_eq claims are Boolean values
proper_superset(set_abcde, set_abc).deduce_in_bool()
# superset_eq claims are Boolean values despite being False
proper_superset(set_123, set_abcde).deduce_in_bool()
Testing the SubsetEq class methods in the superset_eq style¶
<font size =3>The superset_eq class (which is just a style variant of the SubsetEq class) has the following class methods:
- conclude(self, **defaults_config)
- conclude_via_equality(self, **defaults_config)
- conclude_via_equivalence(self, **defaults_config)
- unfold(self, elem_instance_var=x, **defaults_config)
- derive_superset_membership(self, element, **defaults_config)
- conclude_as_folded(self, elem_instance_var=x, **defaults_config)
- apply_transitivity(self, other, **defaults_config)
- deduce_in_bool(self, **defaults_config)
# define a few proper subset relations for testing
set_13, set_134, set_1346 = Set(one, three), Set(one, three, four), Set(one, three, four, six)
set_134_superset_eq_set_13, set_1346_superset_eq_set_134 = (
superset_eq(set_134, set_13), superset_eq(set_1346, set_134))
# define a few proper superset relations for testing
from proveit import g
set_bc, set_bcf, set_bcdfg = Set(b, c), Set(b, c, f), Set(b, c, d, f, g)
set_bcf_superset_eq_set_bc, set_bcdfg_superset_eq_set_bcf = (
superset_eq(set_bcf, set_bc), superset_eq(set_bcdfg, set_bcf))
superset_eq.conclude()¶
set_134_superset_eq_set_13.conclude()
set_bcf_superset_eq_set_bc.conclude()
superset_eq(Set(one, two), Set(a, b)).conclude(
assumptions=[Equals(a, one), Equals(b, two)])
, 
⊢ 
# The example above works even if the set element
# values occur in a different order
superset_eq(Set(one, two), Set(a, b)).conclude(
assumptions=[Equals(a, two), Equals(b, one)])
, ⊢
superset_eq.conclude_via_equality()¶
superset_eq(Set(one, two), Set(a, b)).conclude_via_equality(
assumptions=[Equals(Set(one, two), Set(a, b))])
# superset_eq(Set(one, two), Set(c, d)).conclude_via_equality(
# assumptions=[Equals(c, one), Equals(d, two)],
# simplify_with_known_evaluations=True)
# superset_eq(Set(one, two), Set(c, d)).conclude_via_equality(
# assumptions=[Equals(c, two), Equals(d, one)],
# simplify_with_known_evaluations=True)
superset_eq(B, B).conclude_via_equality()
superset_eq(Set(b, two, d), Set(b, two, d)).conclude_via_equality()
superset_eq.conclude_via_equivalence()¶
superset_eq(Set(one, two), Set(a, b)).conclude_via_equivalence(
assumptions=[SetEquiv(Set(one, two), Set(a, b))])
superset_eq(B, B).conclude_via_equivalence()
superset_eq(Set(b, two, d), Set(b, two, d)).conclude_via_equivalence()
superset_eq.conclude_as_folded()¶
SubsetEq(C, D).conclude_as_folded(
assumptions=[Forall(x, InSet(x, D), domain=C)])
superset_eq(Set(b, d, g), Set(b, g)).conclude_as_folded(
assumptions=[Forall(x, InSet(x, Set(b, d, g)), domain=Set(b, g))])
superset_eq(B, A).conclude_as_folded(
assumptions=[Forall(x, InSet(x, B), domain=A)])
superset_eq.unfold()¶
superset_eq(set_1346, set_134).unfold()
superset_eq(Set(a, one, b, two), Set(a, one, b)).unfold()
superset_eq(Set(a, one, b, c), Set(a, one, b)).unfold()
superset_eq.derive_superset_membership()¶
# given a known superset_eq relationship, and an element in the
# subset, derive the element as being in the superset
superset_eq(set_12345, set_123).derive_superset_membership(two)
superset_eq(Set(a, one, b, c), Set(a, one, b)).derive_superset_membership(a)
# and this works more generally, where we can assume an elem in the subset
from proveit import f
Set(a, b, c, d).deduce_enum_subset_eq(subset=set_abc)
superset_eq(Set(a, b, c, d), Set(a, b, c)).derive_superset_membership(f, assumptions=[InSet(f, set_abc)])
superset_eq.derive_subset_nonmembership()¶
# given a known superset_eq relationship, and an element NOT in the superset,
# derive the element as NOT being in the subset
superset_eq(set_12345, set_123).derive_subset_nonmembership(six)
superset_eq(Set(a, one, b, c), Set(a, one, b)).derive_subset_nonmembership(
two, assumptions=[NotEquals(a, two), NotEquals(b, two), NotEquals(c, two)])
, , ⊢
# and this works more generally, where we can assume some elem not in the superset
# which means it must not be in the subset
from proveit import f
Set(a, b, c, d).deduce_enum_subset_eq(subset=set_abc)
superset_eq(Set(a, b, c, d), Set(a, b, c)).derive_subset_nonmembership(f, assumptions=[NotInSet(f, Set(a, b, c, d))])
superset_eq.apply_transitivity()¶
# establish a SubsetEq judgement:
set_13_subset_eq_set_12345 = set_12345.deduce_enum_subset_eq(subset=set_13)
# establish the superset_eq relation by reversing:
set_12345_superset_eq_set_13 = set_13_subset_eq_set_12345.reversed().prove()
set_12345_superset_eq_set_13.expr
# establish a related proper subset judgement:
set_12345_subset_eq_set_1234567 = set_1234567.deduce_enum_subset_eq(subset=set_12345)
set_1234567_superset_eq_set_12345 = set_12345_subset_eq_set_1234567.reversed().prove()
# use transitivity to go from largest set to smallest set
# (even though using expressions, the expressions have to be true or provable)
set_1234567_superset_eq_set_12345.apply_transitivity(set_12345_superset_eq_set_13.expr)
# this process can work more generally:
A_superset_eq_B, B_superset_eq_C, B_equals_D, C_properSubset_B, D_subset_eq_B = (
superset_eq(A, B), superset_eq(B, C), Equals(B, D), ProperSubset(C, B), SubsetEq(D, B))
A_superset_eq_B.apply_transitivity(
B_superset_eq_C, assumptions=[A_superset_eq_B, B_superset_eq_C])
, ⊢ 
A_superset_eq_B.apply_transitivity(
B_equals_D, assumptions=[A_superset_eq_B, B_equals_D])
, ⊢ 
A_superset_eq_B.apply_transitivity(
D_equals_B, assumptions=[A_superset_eq_B, D_equals_B])
, ⊢
A_superset_eq_B.apply_transitivity(
C_properSubset_B, assumptions=[A_superset_eq_B, C_properSubset_B])
, ⊢
A_superset_eq_B.apply_transitivity(
D_subset_eq_B, assumptions=[A_superset_eq_B, D_subset_eq_B])
, ⊢
# And this shouldn't work if no transitive relation:
try:
A_superset_eq_B.apply_transitivity(
SubsetEq(B, D), assumptions=[A_superset_eq_B, SubsetEq(B, D)])
assert False, "Expecting a ValueError. Should not make it to this point."
except ValueError as the_error:
print("Value Error: {}".format(the_error))
superset_eq.deduce_in_bool()¶
# superset_eq claims are Boolean values
A_superset_eq_B.deduce_in_bool()
# superset_eq claims are Boolean values
superset_eq(set_abcde, set_abc).deduce_in_bool()
Testing the NotProperSubset and NotSubsetEq class methods¶
<font size =3>The NotProperSubset and NotSubsetEqclasses have the following class methods:
- derive_side_effects(self, known_truth)
- conclude(self, assumptions=USE_DEFAULTS)
- unfold(self, assumptions=USE_DEFAULTS)
- conclude_as_folded(self, assumptions=USE_DEFAULTS)
- deduce_in_bool(self, assumptions=USE_DEFAULTS)
# NPS_jdgmt = NotProperSubset(Set(one, two, three, four), Set(one, two, three)).prove(
# assumptions=[NotProperSubset(Set(one, two, three, four), Set(one, two, three))])
NotProperSubset.conclude(), NotSubsetEq.conclude()¶
The conclude() method, called on a NotProperSubset expression such as $A\not\subset B$, derives the NotProperSubset as a judgment from the unfolded Not(ProperSubset()) relationship $\neg(A\subset B)$, if the unfolded version is known or assumed to be true. This works similarly for a NotSubsetEq expression.
set_1234, set_123 = Set(one, two, three, four), Set(one, two, three)
NotProperSubset(set_1234, set_123).conclude(assumptions=[Not(ProperSubset(set_1234, set_123))])
NotSubsetEq(set_1234, set_123).conclude(assumptions=[Not(SubsetEq(set_1234, set_123))])
NotProperSubset.unfold(), NotSubsetEq.unfold()¶
The unfold() method, called on a NotProperSubset expression such as $A\not\subset B$, derives the “unfolded” version $\neg(A\subset B)$ as a judgment, if the original (self) folded version is known or assumed to be true. The method works similarly for NotSubsetEq expressions.
NotProperSubset(set_1234, set_123).unfold(assumptions=[NotProperSubset(set_1234, set_123)])
NotProperSubset(B, A).unfold(assumptions=[NotProperSubset(B, A)])
NotSubsetEq(set_1234, set_123).unfold(assumptions=[NotSubsetEq(set_1234, set_123)])
NotSubsetEq(B, A).unfold(assumptions=[NotSubsetEq(B, A)])
NotProperSubset.conclude_as_folded(), NotSubsetEq.conclude_as_folded()¶
The conclude_as_folded() method, called on a NotProperSubset expression such as $A\not\subset B$, derives the (self) “folded” version $A\not\subset B$, from the unfolded version $\neg(A\subset B)$ being known or assumed to be true. This method is also being called from the conclude() method. The method works similarly for the NotSubsetEq class.</font>
NotProperSubset(set_1234, set_123).conclude_as_folded(assumptions=[Not(ProperSubset(set_1234, set_123))])
NotSubsetEq(set_1234, set_123).conclude_as_folded(assumptions=[Not(SubsetEq(set_1234, set_123))])
not_proper_subset.deduce_in_bool(), NotSubsetEq.deduce_in_bool()¶
The deduce_in_bool() method, called on a NotProperSubset expression such as $A\not\subset B$, derives the fact that $A\not\subset B \in \mathbb{B}$ --- i.e. such subset claims are Boolean values. The method works similarly for the NotSubsetEq class.
# NotProperSubset claims (correct or not) are Boolean values:
NotProperSubset(A, B).deduce_in_bool()
NotProperSubset(Set(a, b, c, d), Set(a, b, c)).deduce_in_bool()
# NotSubsetEq claims (correct or not) are Boolean values:
NotSubsetEq(A, B).deduce_in_bool()
NotSubsetEq(Set(a, b, c), Set(a, b, c, d)).deduce_in_bool()
Testing Some Subset/Superset Automation¶
A number of basic subset/superset identities (such as containment reversals, relaxations, and transitivity) should be accessible through automation. The following cells test the proof automation for a variety of these simple containment identities.
# subset reversal to superset
proper_superset(B,A).prove(assumptions=[ProperSubset(A,B)])
# subset_eq reversal to superset_eq
superset_eq(B,A).prove(assumptions=[SubsetEq(A,B)])
# superset reversal to subset
ProperSubset(B,A).prove(assumptions=[proper_superset(A,B)])
# superset_eq reversal to subset_eq
SubsetEq(B,A).prove(assumptions=[superset_eq(A,B)])
# subset relaxation to subset_eq
SubsetEq(A,B).prove(assumptions=[ProperSubset(A,B)])
# superset relaxation to superset_eq
superset_eq(A,B).prove(assumptions=[proper_superset(A,B)])
# equivalence relax to subset_eq
SubsetEq(A,B).prove(assumptions=[SetEquiv(A, B)])
# equality relax to subset_eq
SubsetEq(A,B).prove(assumptions=[Equals(A, B)])
# equivalence relax to superset_eq
superset_eq(A,B).prove(assumptions=[SetEquiv(A,B)])
# equality relax to superset_eq
superset_eq(A,B).prove(assumptions=[Equals(A,B)])
Deducing quantification via inclusion ¶
We can prove some $\forall_{x \in B} P(x)$ given $\forall_{x \in A} P(x)$ and $A \supseteq B$ and we can prove some $\exists_{x \in B} P(x)$ given $\exists_{x \in A} P(x)$ and $A \subseteq B$.
superset_eq(A, B).prove(assumptions=[superset_eq(A, B)])
SubsetEq.known_left_sides[B]
Forall(x, Px, domain=B).prove(assumptions=[Forall(x, Px, domain=A), superset_eq(A, B)])
, ⊢ 
Exists(x, Px, domain=B).prove(assumptions=[Exists(x, Px, domain=A), SubsetEq(A, B)])
, ⊢ 
These can also be done manually (e.g., to understand why the automation fails when something is wrong):
Forall(x, Px, domain=B).conclude_via_domain_inclusion(A, assumptions=[Forall(x, Px, domain=A), superset_eq(A, B)])
, ⊢
Exists(x, Px, domain=B).conclude_via_domain_inclusion(A, assumptions=[Exists(x, Px, domain=A), SubsetEq(A, B)])
, ⊢
%end demonstrations