From 63b184753d13934c8e4177ffb7fbd7d79526a189 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Thu, 6 Nov 2025 10:06:36 -0700 Subject: [PATCH] Update SubsetEq.conclude() Update SubsetEq.conclude() method to deal more correctly with the special case of "basic" SetOfAll set comprehensions. Errors has been recently encountered due to some older code in the conclude() method. The use of SetOfAll.explicit_conditions() (instead of the more general .conditions()) and wrapping conditions in a logical And() seems to have corrected the most basic problems. Commit also includes updated related demonstrations ntoebook in logic/sets/inclusion and minor addition to demonstrations notebook in logic/sets/comprehension. --- .../_theory_nbs_/demonstrations.ipynb | 9 ++ .../_theory_nbs_/demonstrations.ipynb | 99 ++++++++++++++++--- .../proveit/logic/sets/inclusion/subset_eq.py | 28 ++++-- 3 files changed, 114 insertions(+), 22 deletions(-) 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