From 8b57d7e2da669bc44a460b88e547715cbc840ee9 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Wed, 13 Aug 2025 16:34:01 -0600 Subject: [PATCH 1/8] Update Exists().unfold() method, fix related bug(s) Update the Exists().unfold() method and in the process fix some buggy code that seemed to assume that an Exists() object always has one or more explicit conditions. For now, the old code has been left in place, commented out, for comparison. Also update the logic/booleans/quantification/existence demonstrations.ipynb notebook with related testing of the new Exists().unfold() method. --- .../_theory_nbs_/demonstrations.ipynb | 94 ++++++++++++++++++- .../quantification/existence/exists.py | 49 ++++++++-- 2 files changed, 133 insertions(+), 10 deletions(-) diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb index 4959e022b8dd..37c220681607 100644 --- a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb @@ -17,9 +17,9 @@ "import proveit\n", "%begin demonstrations\n", "\n", - "from proveit import a, b\n", + "from proveit import a, b, c, x, defaults, Px\n", "from proveit.logic import Exists, Equals\n", - "from proveit.numbers import Add, two, three, five, NaturalPos" + "from proveit.numbers import one, two, three, five, Add, greater_eq, Integer, LessEq, NaturalPos" ] }, { @@ -37,7 +37,7 @@ "metadata": {}, "outputs": [], "source": [ - "Exists((a, b), Equals(Add(a, b), five)).conclude_via_example((two, three))" + "exists_a_b_st_sum_is_5 = Exists((a, b), Equals(Add(a, b), five)).conclude_via_example((two, three))" ] }, { @@ -49,6 +49,94 @@ "Exists((a, b), Equals(Add(a, b), five), domain=NaturalPos).conclude_via_example((two, three))" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Testing" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Generate some existential test cases, each quite simple but varying across the collection in terms of the presence/absence of explicit conditions and domain(s)." + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# some Exists() expressions\n", + "exists_test_exprs = [\n", + " Exists((a, b), Equals(Add(a, b), five)), # no conditions at all\n", + " Exists((a, b), Equals(Add(a, b), five), domain=NaturalPos), # single domain spec\n", + " Exists((a, b), Equals(Add(a, b), five), domains=[NaturalPos, Integer]), # two domains\n", + " Exists((a, b), Equals(Add(a, b), five), conditions = [LessEq(a, five), LessEq(b, five)]), # explicit conditions\n", + " Exists((a, b), Equals(Add(a, b), five), conditions = [LessEq(a, five), LessEq(b, five)], domain = Integer), # conditions + domain\n", + " Exists((a, b, c), LessEq(Add(a, b, c), five), conditions = [greater_eq(a, one), greater_eq(b, one), greater_eq(c, one)], domain = Integer), # conditions + domain\n", + " Exists(x, Px) # archetype case\n", + "]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# add this as a default assumption so later judgments work out:\n", + "defaults.assumptions = [Exists(x, Px)]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# some Exists() judgments\n", + "exists_test_judgments = [\n", + " exists_test_exprs[0].conclude_via_example((two, three)),\n", + " exists_test_exprs[1].conclude_via_example((two, three)),\n", + " exists_test_exprs[2].conclude_via_example((two, three)),\n", + " exists_test_exprs[3].conclude_via_example((two, three)),\n", + " exists_test_exprs[4].conclude_via_example((two, three)),\n", + " exists_test_exprs[5].conclude_via_example((one, two, one)),\n", + " exists_test_exprs[6].prove()\n", + "]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# checking to verify these look correct\n", + "for j in exists_test_judgments:\n", + " display(j)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Now a test of the Exists().unfold() method" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "for j in exists_test_judgments:\n", + " display(j.unfold())" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/logic/booleans/quantification/existence/exists.py b/packages/proveit/logic/booleans/quantification/existence/exists.py index cb21c94ab3e4..4c590c12e39d 100644 --- a/packages/proveit/logic/booleans/quantification/existence/exists.py +++ b/packages/proveit/logic/booleans/quantification/existence/exists.py @@ -196,19 +196,54 @@ def eliminate(skolem_constants, judgment, **defaults_config): y_1_to__n: existential.instance_params}, preserve_all=True).derive_consequent() + # Modified version further below; keep this version here + # temporarily until further testing implemented. + # @prover + # def unfold(self, **defaults_config): + # ''' + # From this existential quantifier, derive the "unfolded" + # version according to its definition (the negation of + # a universal quantification). + # ''' + # from proveit.logic.booleans.quantification.existence \ + # import exists_unfolding + # _x = _y = self.instance_params + # _n = _x.num_elements() + # _P = Lambda(_x, self.operand.body.value) + # _Q = Lambda(_x, self.operand.body.condition) + # return exists_unfolding.instantiate( + # {n: _n, P: _P, Q: _Q, x: _x, y: _y}).derive_consequent() + @prover def unfold(self, **defaults_config): ''' - From this existential quantifier, derive the "unfolded" - version according to its definition (the negation of - a universal quantification). + From this existential quantifier, and knowing or assuming + self to be TRUE, derive the "unfolded" version according + to its definition, producing the negation of a universal + quantification. For example, given + + A = |- Exists((a,b), (a+b = 5), domain = NaturalPos), + + A.unfold() produces: + + |- Not(Forall((a, b in NaturalPos), [(a+b = 5) != T])). + + As explained in the existence axioms notebook, the format here + (and the awkwardness of the conclusion) arises from the effort + to avoid the assumption that the operation always returns a + Boolean. + ''' - from proveit.logic.booleans.quantification.existence \ - import exists_unfolding + from proveit.logic import TRUE + from proveit.logic.booleans.quantification.existence import ( + exists_unfolding) _x = _y = self.instance_params _n = _x.num_elements() - _P = Lambda(_x, self.operand.body.value) - _Q = Lambda(_x, self.operand.body.condition) + _P = Lambda(_x, self.instance_expr) + if hasattr(self, 'condition'): + _Q = Lambda(_x, self.condition) + else: + _Q = Lambda(_x, TRUE) return exists_unfolding.instantiate( {n: _n, P: _P, Q: _Q, x: _x, y: _y}).derive_consequent() From 3ec1a41fc0db4a9b9b90dbc57b5e1b8ddd365682 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Wed, 13 Aug 2025 20:19:04 -0600 Subject: [PATCH 2/8] Update Exists().definition() method, fix related bug(s) Update the Exists().definition() method and in the process fix some buggy code that seemed to assume that an Exists() object always has one or more explicit conditions. Also update the logic/booleans/quantification/existence demonstrations.ipynb notebook with related testing of the new Exists().definition() method. --- .../_theory_nbs_/demonstrations.ipynb | 18 +++++++++++ .../quantification/existence/exists.py | 31 ++++++++++++++++--- 2 files changed, 45 insertions(+), 4 deletions(-) diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb index 37c220681607..577622b838af 100644 --- a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb @@ -137,6 +137,24 @@ " display(j.unfold())" ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "#### Testing the Exists().definition() method" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# we can do this on the exprs or the judgments\n", + "for j in exists_test_exprs:\n", + " display(j.definition())" + ] + }, { "cell_type": "code", "execution_count": null, diff --git a/packages/proveit/logic/booleans/quantification/existence/exists.py b/packages/proveit/logic/booleans/quantification/existence/exists.py index 4c590c12e39d..e1a741b3517e 100644 --- a/packages/proveit/logic/booleans/quantification/existence/exists.py +++ b/packages/proveit/logic/booleans/quantification/existence/exists.py @@ -254,14 +254,37 @@ def definition(self, **defaults_config): equation with this existential quantifier on the left and a negated universal quantification on the right. ''' + from proveit import defaults + from proveit.logic import Forall, Not, NotEquals, TRUE from proveit.logic.booleans.quantification.existence \ import exists_def _x = _y = self.instance_params _n = _x.num_elements() - _P = Lambda(_x, self.operand.body.value) - _Q = Lambda(_x, self.operand.body.condition) - return exists_def.instantiate( - {n: _n, P: _P, Q: _Q, x: _x, y: _y}, preserve_expr=self) + _P = Lambda(_x, self.instance_expr) + if hasattr(self, 'condition'): + _Q = Lambda(_x, self.condition) + else: + _Q = Lambda(_x, TRUE) + # try constructing the rhs to preserve + if hasattr(self, 'condition'): + rhs_to_preserve = ( + Not(Forall(_x, + NotEquals(self.instance_expr, TRUE), + conditions = [self.condition]))) + else: + rhs_to_preserve = ( + Not(Forall(_x, + NotEquals(self.instance_expr, TRUE), + ))) + temp_exprs_to_preserve = set([self, rhs_to_preserve]) + defaults.preserved_exprs.update(temp_exprs_to_preserve) + result = exists_def.instantiate( + # {n: _n, P: _P, Q: _Q, x: _x, y: _y}, preserve_expr=self) + {n: _n, P: _P, Q: _Q, x: _x, y: _y} + ) + # revert preserved_exprs set to original + defaults.preserved_exprs.difference_update(temp_exprs_to_preserve) + return result @prover def deduce_not_exists(self, **defaults_config): From d50e684400c348aae1f213c8b089aaa21ab86190 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Thu, 14 Aug 2025 09:12:16 -0600 Subject: [PATCH 3/8] Add two basic theorems to logic/booleans/quantification/existence sub-theory pkg Add two basic theorems to logic/booleans/quantification/existence sub-theory pkg, namely `exists_not_unfolding` and `exists_not_unfolding`, to complement/supplement the theorems already there and make it a little easier to go between an existence such that Not(P) and Not(Forall(P)). Corresponding Exists() methods or method updates not yet implemented. --- .../proofs/exists_not_folding/thm_proof.ipynb | 47 +++++++++++++++++++ .../exists_not_unfolding/thm_proof.ipynb | 47 +++++++++++++++++++ .../existence/_theory_nbs_/theorems.ipynb | 26 ++++++++++ 3 files changed, 120 insertions(+) create mode 100644 packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_folding/thm_proof.ipynb create mode 100644 packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_unfolding/thm_proof.ipynb diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_folding/thm_proof.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_folding/thm_proof.ipynb new file mode 100644 index 000000000000..d53e4e1cb36b --- /dev/null +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_folding/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.logic.booleans.quantification.existence.exists_not_folding theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving exists_not_folding" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_unfolding/thm_proof.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_unfolding/thm_proof.ipynb new file mode 100644 index 000000000000..a619ac794048 --- /dev/null +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_unfolding/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.logic.booleans.quantification.existence.exists_not_unfolding theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving exists_not_unfolding" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb index 7412d3fc149a..e2e02cfc313d 100644 --- a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb @@ -114,6 +114,32 @@ " domain=NaturalPos)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "exists_not_unfolding = Forall(n,\n", + "Forall((P, Q), \n", + " Implies(general_exists_notPx_st_Qx,\n", + " Not(general_forall_Py_if_Qy)).with_wrap_after_operator()),\n", + "domain=NaturalPos)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "exists_not_folding = Forall(n,\n", + "Forall((P, Q),\n", + " general_exists_notPx_st_Qx ,\n", + "condition=Not(general_forall_Py_if_Qy)),\n", + "domain=NaturalPos)" + ] + }, { "cell_type": "markdown", "metadata": {}, From 38fe2d7bd909d69ab5655048457cf7522eaffd8e Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Sun, 17 Aug 2025 22:26:21 -0700 Subject: [PATCH 4/8] Establish exists_not_eq_not_forall thm in existence sub-theory pkg Establish the exists_not_eq_not_forall theorem in logic/booleans/quantification/existence sub-theory package, being the Exists(x, Not(P(x))) analog to the Exists(x, P(x)) `exists_def' axiom. --- .../exists_not_eq_not_forall/thm_proof.ipynb | 47 +++++++++++++++++++ .../existence/_theory_nbs_/theorems.ipynb | 13 +++++ 2 files changed, 60 insertions(+) create mode 100644 packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_eq_not_forall/thm_proof.ipynb diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_eq_not_forall/thm_proof.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_eq_not_forall/thm_proof.ipynb new file mode 100644 index 000000000000..8299ee007096 --- /dev/null +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/proofs/exists_not_eq_not_forall/thm_proof.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Proof of proveit.logic.booleans.quantification.existence.exists_not_eq_not_forall theorem\n", + "========" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import proveit\n", + "theory = proveit.Theory() # the theorem's theory" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "%proving exists_not_eq_not_forall" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + } + }, + "nbformat": 4, + "nbformat_minor": 0 +} diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb index e2e02cfc313d..101f3a9d68cd 100644 --- a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb @@ -114,6 +114,19 @@ " domain=NaturalPos)" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "exists_not_eq_not_forall = Forall(n,\n", + "Forall((P, Q), \n", + " Equals(general_exists_notPx_st_Qx,\n", + " Not(general_forall_Py_if_Qy)).with_wrap_after_operator()),\n", + "domain=NaturalPos)" + ] + }, { "cell_type": "code", "execution_count": null, From db94b6b86b07fdecfd5522deefc223a9032587a0 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Sun, 17 Aug 2025 22:30:58 -0700 Subject: [PATCH 5/8] Augment Exists().unfold() and Exists().definition() methods Augment Exists().unfold() and Exists().definition() methods to also deal with the cases of Exists(x, Not(P(x))) instead of just the Exists(x, P(x)) cases, and establish some minimal testing of the methods in the existence demonstrations notebook. The augmentations utilize the alternative existential unfolding, folding, and equality theorems in recent previous commits. --- .../_theory_nbs_/demonstrations.ipynb | 12 +-- .../quantification/existence/exists.py | 88 ++++++++++++++----- 2 files changed, 75 insertions(+), 25 deletions(-) diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb index 577622b838af..fdfdfa84cd93 100644 --- a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb @@ -17,8 +17,8 @@ "import proveit\n", "%begin demonstrations\n", "\n", - "from proveit import a, b, c, x, defaults, Px\n", - "from proveit.logic import Exists, Equals\n", + "from proveit import a, b, c, x, defaults, Px, Rx\n", + "from proveit.logic import Exists, Equals, Not\n", "from proveit.numbers import one, two, three, five, Add, greater_eq, Integer, LessEq, NaturalPos" ] }, @@ -77,7 +77,8 @@ " Exists((a, b), Equals(Add(a, b), five), conditions = [LessEq(a, five), LessEq(b, five)]), # explicit conditions\n", " Exists((a, b), Equals(Add(a, b), five), conditions = [LessEq(a, five), LessEq(b, five)], domain = Integer), # conditions + domain\n", " Exists((a, b, c), LessEq(Add(a, b, c), five), conditions = [greater_eq(a, one), greater_eq(b, one), greater_eq(c, one)], domain = Integer), # conditions + domain\n", - " Exists(x, Px) # archetype case\n", + " Exists(x, Px), # archetype case\n", + " Exists(x, Not(Rx)) # archetype case\n", "]" ] }, @@ -88,7 +89,7 @@ "outputs": [], "source": [ "# add this as a default assumption so later judgments work out:\n", - "defaults.assumptions = [Exists(x, Px)]" + "defaults.assumptions = [Exists(x, Px), Exists(x, Not(Rx))]" ] }, { @@ -105,7 +106,8 @@ " exists_test_exprs[3].conclude_via_example((two, three)),\n", " exists_test_exprs[4].conclude_via_example((two, three)),\n", " exists_test_exprs[5].conclude_via_example((one, two, one)),\n", - " exists_test_exprs[6].prove()\n", + " exists_test_exprs[6].prove(),\n", + " exists_test_exprs[7].prove()\n", "]" ] }, diff --git a/packages/proveit/logic/booleans/quantification/existence/exists.py b/packages/proveit/logic/booleans/quantification/existence/exists.py index e1a741b3517e..deb8bfab2dce 100644 --- a/packages/proveit/logic/booleans/quantification/existence/exists.py +++ b/packages/proveit/logic/booleans/quantification/existence/exists.py @@ -231,57 +231,105 @@ def unfold(self, **defaults_config): As explained in the existence axioms notebook, the format here (and the awkwardness of the conclusion) arises from the effort to avoid the assumption that the operation always returns a - Boolean. + Boolean. On the other hand, if we have: + + B = |- Exists(x, Not(P(x))), + + then B.unfold() produces: + + |- Not(Forall(x, P(x))) ''' - from proveit.logic import TRUE + from proveit.logic import Not, TRUE from proveit.logic.booleans.quantification.existence import ( - exists_unfolding) + exists_not_unfolding, exists_unfolding) _x = _y = self.instance_params _n = _x.num_elements() - _P = Lambda(_x, self.instance_expr) + + # distinguish between Exists(x, P(x)) vs Exists(x, Not(P(x))) + _case_not = False + if isinstance(self.instance_expr, Not): + _case_not = True + _P = Lambda(_x, self.instance_expr.operand) + else: + _P = Lambda(_x, self.instance_expr) + # distinguish between cases with and w/out conditions if hasattr(self, 'condition'): _Q = Lambda(_x, self.condition) else: _Q = Lambda(_x, TRUE) + if _case_not: + return exists_not_unfolding.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y}).derive_consequent() return exists_unfolding.instantiate( {n: _n, P: _P, Q: _Q, x: _x, y: _y}).derive_consequent() + # NEXT: update definition() method to also deal with the alternative + # existential Exists(x, Not(P(x))) 20250817 + @prover def definition(self, **defaults_config): ''' Return definition of this existential quantifier as an equation with this existential quantifier on the left - and a negated universal quantification on the right. + and a negated universal quantification on the right. This + handles two separate cases (along with cases with and w/out + conditions): + Exists(x, P(x)) vs. Exists(x, Not(P(x))), + which return: + Not(Forall(x, P(x) != T)) and Not(Forall(x, P(x))), + respectively. ''' from proveit import defaults from proveit.logic import Forall, Not, NotEquals, TRUE - from proveit.logic.booleans.quantification.existence \ - import exists_def + from proveit.logic.booleans.quantification.existence import ( + exists_def, exists_not_eq_not_forall) _x = _y = self.instance_params _n = _x.num_elements() - _P = Lambda(_x, self.instance_expr) + + # distinguish between Exists(x, P(x)) vs Exists(x, Not(P(x))) + _case_not = False + if isinstance(self.instance_expr, Not): + _case_not = True + _P = Lambda(_x, self.instance_expr.operand) + else: + _P = Lambda(_x, self.instance_expr) + # distinguish between cases with and w/out conditions if hasattr(self, 'condition'): _Q = Lambda(_x, self.condition) else: _Q = Lambda(_x, TRUE) # try constructing the rhs to preserve if hasattr(self, 'condition'): - rhs_to_preserve = ( - Not(Forall(_x, - NotEquals(self.instance_expr, TRUE), - conditions = [self.condition]))) + if _case_not: + rhs_to_preserve = ( + Not(Forall(_x, self.instance_expr.operand, + conditions = [self.condition]))) + else: + rhs_to_preserve = ( + Not(Forall(_x, + NotEquals(self.instance_expr, TRUE), + conditions = [self.condition]))) else: - rhs_to_preserve = ( - Not(Forall(_x, - NotEquals(self.instance_expr, TRUE), - ))) + if _case_not: + rhs_to_preserve = ( + Not(Forall(_x, self.instance_expr.operand, + ))) + else: + rhs_to_preserve = ( + Not(Forall(_x, + NotEquals(self.instance_expr, TRUE), + ))) temp_exprs_to_preserve = set([self, rhs_to_preserve]) defaults.preserved_exprs.update(temp_exprs_to_preserve) - result = exists_def.instantiate( - # {n: _n, P: _P, Q: _Q, x: _x, y: _y}, preserve_expr=self) - {n: _n, P: _P, Q: _Q, x: _x, y: _y} - ) + if _case_not: + result = exists_not_eq_not_forall.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y} + ) + else: + result = exists_def.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y} + ) # revert preserved_exprs set to original defaults.preserved_exprs.difference_update(temp_exprs_to_preserve) return result From 1faf65405de0ca3330560da2c317bb861b63ca98 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Fri, 22 Aug 2025 11:06:58 -0600 Subject: [PATCH 6/8] Update exists.py Update exists.py, settling on the use of a preserve_all = True approach in the Exists().definition() method and cleaning out older code and comments. --- .../quantification/existence/exists.py | 61 +++---------------- 1 file changed, 8 insertions(+), 53 deletions(-) diff --git a/packages/proveit/logic/booleans/quantification/existence/exists.py b/packages/proveit/logic/booleans/quantification/existence/exists.py index deb8bfab2dce..ecbe31fa539e 100644 --- a/packages/proveit/logic/booleans/quantification/existence/exists.py +++ b/packages/proveit/logic/booleans/quantification/existence/exists.py @@ -196,24 +196,6 @@ def eliminate(skolem_constants, judgment, **defaults_config): y_1_to__n: existential.instance_params}, preserve_all=True).derive_consequent() - # Modified version further below; keep this version here - # temporarily until further testing implemented. - # @prover - # def unfold(self, **defaults_config): - # ''' - # From this existential quantifier, derive the "unfolded" - # version according to its definition (the negation of - # a universal quantification). - # ''' - # from proveit.logic.booleans.quantification.existence \ - # import exists_unfolding - # _x = _y = self.instance_params - # _n = _x.num_elements() - # _P = Lambda(_x, self.operand.body.value) - # _Q = Lambda(_x, self.operand.body.condition) - # return exists_unfolding.instantiate( - # {n: _n, P: _P, Q: _Q, x: _x, y: _y}).derive_consequent() - @prover def unfold(self, **defaults_config): ''' @@ -264,9 +246,6 @@ def unfold(self, **defaults_config): return exists_unfolding.instantiate( {n: _n, P: _P, Q: _Q, x: _x, y: _y}).derive_consequent() - # NEXT: update definition() method to also deal with the alternative - # existential Exists(x, Not(P(x))) 20250817 - @prover def definition(self, **defaults_config): ''' @@ -299,40 +278,16 @@ def definition(self, **defaults_config): _Q = Lambda(_x, self.condition) else: _Q = Lambda(_x, TRUE) - # try constructing the rhs to preserve - if hasattr(self, 'condition'): - if _case_not: - rhs_to_preserve = ( - Not(Forall(_x, self.instance_expr.operand, - conditions = [self.condition]))) - else: - rhs_to_preserve = ( - Not(Forall(_x, - NotEquals(self.instance_expr, TRUE), - conditions = [self.condition]))) - else: - if _case_not: - rhs_to_preserve = ( - Not(Forall(_x, self.instance_expr.operand, - ))) - else: - rhs_to_preserve = ( - Not(Forall(_x, - NotEquals(self.instance_expr, TRUE), - ))) - temp_exprs_to_preserve = set([self, rhs_to_preserve]) - defaults.preserved_exprs.update(temp_exprs_to_preserve) + + # now ready to instantiate thm based on _case_not if _case_not: - result = exists_not_eq_not_forall.instantiate( - {n: _n, P: _P, Q: _Q, x: _x, y: _y} - ) + return exists_not_eq_not_forall.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y}, + preserve_all = True) else: - result = exists_def.instantiate( - {n: _n, P: _P, Q: _Q, x: _x, y: _y} - ) - # revert preserved_exprs set to original - defaults.preserved_exprs.difference_update(temp_exprs_to_preserve) - return result + return exists_def.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y}, + preserve_all = True) @prover def deduce_not_exists(self, **defaults_config): From a22f6fc7d6a3f8f25d0213ca46f414277800e602 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Fri, 22 Aug 2025 11:09:13 -0600 Subject: [PATCH 7/8] Update existence demonstrations nb Update the logic/booleans/quantification/existence demonstrations notebook, adding some example Exists() expressions to test and demonstrate recent updates to the existential theorems and related Exists() methods. --- .../_theory_nbs_/demonstrations.ipynb | 31 ++++++++++++++++--- 1 file changed, 26 insertions(+), 5 deletions(-) diff --git a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb index fdfdfa84cd93..f96222c0f87c 100644 --- a/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb +++ b/packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/demonstrations.ipynb @@ -18,8 +18,8 @@ "%begin demonstrations\n", "\n", "from proveit import a, b, c, x, defaults, Px, Rx\n", - "from proveit.logic import Exists, Equals, Not\n", - "from proveit.numbers import one, two, three, five, Add, greater_eq, Integer, LessEq, NaturalPos" + "from proveit.logic import Exists, Equals, Not, NotEquals\n", + "from proveit.numbers import one, two, three, four, five, Add, greater_eq, Integer, LessEq, NaturalPos" ] }, { @@ -78,10 +78,26 @@ " Exists((a, b), Equals(Add(a, b), five), conditions = [LessEq(a, five), LessEq(b, five)], domain = Integer), # conditions + domain\n", " Exists((a, b, c), LessEq(Add(a, b, c), five), conditions = [greater_eq(a, one), greater_eq(b, one), greater_eq(c, one)], domain = Integer), # conditions + domain\n", " Exists(x, Px), # archetype case\n", + " Exists((a, b), Not(Equals(Add(a, b), five))), # no conditions at all\n", + " Exists((a, b), Not(Equals(Add(a, b), five)), domain = NaturalPos), # single domain spec\n", + " Exists((a, b), Not(Equals(Add(a, b), five)), domains = [NaturalPos, Integer]), # two domains\n", + " Exists((a, b), Not(Equals(Add(a, b), five)), conditions = [LessEq(a, five), LessEq(b, five)]), # explicit conditions\n", + " Exists((a, b), Not(Equals(Add(a, b), five)), conditions = [LessEq(a, five), LessEq(b, five)], domain = Integer), # conditions + domain\n", " Exists(x, Not(Rx)) # archetype case\n", "]" ] }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# check to verify these look correct\n", + "for i, expr in enumerate(exists_test_exprs):\n", + " display(i, expr)" + ] + }, { "cell_type": "code", "execution_count": null, @@ -106,8 +122,13 @@ " exists_test_exprs[3].conclude_via_example((two, three)),\n", " exists_test_exprs[4].conclude_via_example((two, three)),\n", " exists_test_exprs[5].conclude_via_example((one, two, one)),\n", - " exists_test_exprs[6].prove(),\n", - " exists_test_exprs[7].prove()\n", + " exists_test_exprs[6].prove(), # proof by assumption\n", + " exists_test_exprs[7].conclude_via_example((two, four)),\n", + " exists_test_exprs[8].conclude_via_example((two, four)),\n", + " exists_test_exprs[9].conclude_via_example((two, four)),\n", + " exists_test_exprs[10].conclude_via_example((two, four)),\n", + " exists_test_exprs[11].conclude_via_example((two, four)),\n", + " exists_test_exprs[12].prove() # proof by assumption\n", "]" ] }, @@ -117,7 +138,7 @@ "metadata": {}, "outputs": [], "source": [ - "# checking to verify these look correct\n", + "# check to verify the judgments look correct and as-expected:\n", "for j in exists_test_judgments:\n", " display(j)" ] From de6ef419ba6418329aa9a43c358ba39573186eb9 Mon Sep 17 00:00:00 2001 From: Warren Craft Date: Sat, 23 Aug 2025 22:29:23 -0600 Subject: [PATCH 8/8] Update Exists().definition() to use more specific expr preservation approach Update the Exists().definition() method to use a more specific expression-preservation approach instead of the 'preserve_all = True' approach. The 'preserve_all = True' leaves preserved the "empty" condition cases which then show up as a redundant 'T' in the eventual expression result; this more precise preservation method constructs the expected rhs expression and explicitly preserves that instead. This performs well in a handful of examples in the existence demonstrations notebook. --- .../quantification/existence/exists.py | 43 +++++++++++++++---- 1 file changed, 34 insertions(+), 9 deletions(-) diff --git a/packages/proveit/logic/booleans/quantification/existence/exists.py b/packages/proveit/logic/booleans/quantification/existence/exists.py index ecbe31fa539e..8c2b3abece48 100644 --- a/packages/proveit/logic/booleans/quantification/existence/exists.py +++ b/packages/proveit/logic/booleans/quantification/existence/exists.py @@ -278,16 +278,41 @@ def definition(self, **defaults_config): _Q = Lambda(_x, self.condition) else: _Q = Lambda(_x, TRUE) - - # now ready to instantiate thm based on _case_not - if _case_not: - return exists_not_eq_not_forall.instantiate( - {n: _n, P: _P, Q: _Q, x: _x, y: _y}, - preserve_all = True) + + # Construct the rhs result to preserve (using + # 'preserve_all = TRUE' in the instantiation step further + # below tends to preserve too much, in particular preserving + # the "empty" condition _Q = Lambda(_x, TRUE) when we'd like + # it to be simplified away entirely). + if hasattr(self, 'condition'): + if _case_not: + rhs_to_preserve = ( + Not(Forall(_x, self.instance_expr.operand, + conditions = [self.condition]))) + else: + rhs_to_preserve = ( + Not(Forall(_x, + NotEquals(self.instance_expr, TRUE), + conditions = [self.condition]))) else: - return exists_def.instantiate( - {n: _n, P: _P, Q: _Q, x: _x, y: _y}, - preserve_all = True) + if _case_not: + rhs_to_preserve = ( + Not(Forall(_x, self.instance_expr.operand))) + else: + rhs_to_preserve = ( + Not(Forall(_x, + NotEquals(self.instance_expr, TRUE)))) + + # now ready to instantiate thm based on _case_not, and + # explicitly preserving the expected rhs of the resulting eq. + with defaults.temporary() as temp_defaults: + temp_defaults.preserved_exprs = {self, rhs_to_preserve} + if _case_not: + return exists_not_eq_not_forall.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y}) + else: + return exists_def.instantiate( + {n: _n, P: _P, Q: _Q, x: _x, y: _y}) @prover def deduce_not_exists(self, **defaults_config):