Skip to content

Updated SubsetEq.conclude() to better accommodate basic SetOfAll() #358

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wdcraft01 wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Updated SubsetEq.conclude() to better accommodate basic SetOfAll() #358

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions packages/proveit/logic/sets/comprehension/_theory_nbs_/demonstrations.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,15 @@
"squares_of_unit_interval.conditions"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"squares_of_unit_interval.explicit_conditions()"
]
},
{
"cell_type": "code",
"execution_count": null,
Expand Down
99 changes: 87 additions & 12 deletions packages/proveit/logic/sets/inclusion/_theory_nbs_/demonstrations.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,21 @@
"source": [
"import proveit\n",
"from proveit import free_vars, InstantiationFailure, ProofFailure, used_vars\n",
"from proveit import a, b, c, d, e, f, x, y, A, B, C, D, E, F, X, Y, Px\n",
"from proveit import a, b, c, d, e, f, x, y, z, A, B, C, D, E, F, X, Y, Px\n",
"from proveit.logic import (Equals, Forall, Exists, Implies, InSet, Not,\n",
" NotEquals, NotInSet, Set)\n",
"from proveit.logic import (Intersect, SetEquiv, NotProperSubset,\n",
" SubsetEq, NotSubsetEq, not_superset_eq,\n",
" ProperSubset, proper_superset, not_proper_superset,\n",
" SubsetProper, StrictSubset, superset_eq)\n",
"from proveit.numbers import zero, one, two, three, four, five\n",
" SubsetEq, NotEquals, NotSubsetEq, not_superset_eq,\n",
" Or, ProperSubset, proper_superset, not_proper_superset,\n",
" SetOfAll, SubsetProper, StrictSubset, superset_eq)\n",
"from proveit.numbers import zero, one, two, three, four, five, greater, Less, LessEq, num\n",
"from proveit.numbers import (Integer, Natural, NaturalPos, Real,\n",
" RealNeg, RealPos)\n",
"from proveit.numbers.number_sets.real_numbers import int_within_real\n",
"from proveit.logic.sets.inclusion import (\n",
" subset_eq_def, proper_subset_def, not_proper_subset_def, unfold_not_subset_eq)\n",
"from proveit.logic.sets.inclusion import fold_not_subset_eq, fold_subset_eq\n",
"\n",
"%begin demonstrations"
]
},
Expand Down Expand Up @@ -1861,16 +1862,92 @@
" assumptions=[Equals(a, two), Equals(b, one)])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"#### `SubsetEq().conclude()` Examples Involving `SetOfAll()` Constructions"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"non_zero_ints = SetOfAll(x, x, conditions=[NotEquals(x, zero)], domain=Integer)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"SubsetEq(non_zero_ints, Integer).conclude()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"ints_1_thru_9 = SetOfAll(x, x, conditions=[LessEq(one, x), LessEq(x, num(9))], domain=Integer)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"SubsetEq(ints_1_thru_9, Integer).conclude()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"all_the_ints = SetOfAll(x, x, domain=Integer)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"SubsetEq(all_the_ints, Integer).conclude()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"pos_100_z = SetOfAll(z, z, conditions = [greater(z, zero), LessEq(z, num(100))], domain = Integer)"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"SubsetEq(pos_100_z, Integer).conclude()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"# Some issue here involving SetOfAll sets;\n",
"# the set_of_all.py and sets/comprehension package must be updated\n",
"# from proveit.logic import NotEquals, SetOfAll\n",
"# non_zero_ints = SetOfAll(x, x, conditions=[NotEquals(x, zero)], domain=Integer)"
"non_zero_z_using_or = SetOfAll(z, z, conditions = [Or(Less(z, zero), greater(z, zero))], domain = Integer)"
]
},
{
Expand All @@ -1879,9 +1956,7 @@
"metadata": {},
"outputs": [],
"source": [
"# Some issue here involving SetOfAll sets;\n",
"# the set_of_all.py and sets/comprehension package must be updated\n",
"# SubsetEq(non_zero_ints, Integer).conclude()"
"SubsetEq(non_zero_z_using_or, Integer).conclude()"
]
},
{
Expand Down
28 changes: 18 additions & 10 deletions packages/proveit/logic/sets/inclusion/subset_eq.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
from proveit import (as_expression, Literal, Operation,
from proveit import (as_expression, Function, Literal, Operation,
free_vars, safe_dummy_var,
Judgment, UnsatisfiedPrerequisites,
defaults, USE_DEFAULTS, prover, relation_prover)
Expand Down Expand Up @@ -86,21 +86,29 @@ def conclude(self, **defaults_config):
if SetEquiv(*self.operands.entries).proven():
return self.conclude_via_equivalence()

# Check for special case of set comprehension
# [{x | Q*(x)}_{x \in S}] \subseteq S
# Check for special case of basic set comprehension
# [{x | Q(x)}_{x \in S}] \subseteq S
if isinstance(self.subset, SetOfAll):

from proveit import y, ExprTuple
from proveit.logic import And
from proveit.logic.sets.comprehension import (
comprehension_is_subset)
set_of_all = self.subset
if (len(set_of_all.all_instance_vars()) == 1 and
set_of_all.instance_element == set_of_all.all_instance_vars()[0] and
set_of_all.domain == self.superset):

if (len(set_of_all.all_instance_vars()) == 1
and (set_of_all.instance_element
== set_of_all.all_instance_vars()[0])
and set_of_all.domain == self.superset):

Q_op, Q_op_sub = (
Operation(Q, set_of_all.all_instance_vars()),
set_of_all.conditions)
Function(Q, set_of_all.all_instance_vars()),
And(*set_of_all.explicit_conditions()))
_y_sub = set_of_all.all_instance_vars()[0]

concluded = comprehension_is_subset.instantiate(
{S: set_of_all.domain, Q_op: Q_op_sub},
relabel_map={x: set_of_all.all_instance_vars()[0]})
{S: set_of_all.domain, y:_y_sub, Q_op: Q_op_sub})

return concluded

_A, _B = self.operands.entries
Expand Down