diff --git a/packages/proveit/logic/sets/comprehension/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/comprehension/_theory_nbs_/demonstrations.ipynb index 232a531c3957..92b3bb48ae5d 100644 --- a/packages/proveit/logic/sets/comprehension/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/logic/sets/comprehension/_theory_nbs_/demonstrations.ipynb @@ -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, diff --git a/packages/proveit/logic/sets/inclusion/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/inclusion/_theory_nbs_/demonstrations.ipynb index 121eaa4c7ae1..5d40be6efa40 100644 --- a/packages/proveit/logic/sets/inclusion/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/logic/sets/inclusion/_theory_nbs_/demonstrations.ipynb @@ -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" ] }, @@ -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)" ] }, { @@ -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()" ] }, { diff --git a/packages/proveit/logic/sets/inclusion/subset_eq.py b/packages/proveit/logic/sets/inclusion/subset_eq.py index c5f92c1a752c..fd029f910f56 100644 --- a/packages/proveit/logic/sets/inclusion/subset_eq.py +++ b/packages/proveit/logic/sets/inclusion/subset_eq.py @@ -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) @@ -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