345 alternative exists unfolding

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.logic import Exists, Equals\n",
-    "from proveit.numbers import Add, two, three, five, NaturalPos"
+    "from proveit import a, b, c, x, defaults, Px, Rx\n",
+    "from proveit.logic import Exists, Equals, Not, NotEquals\n",
+    "from proveit.numbers import one, two, three, four, 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,135 @@
     "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",
+    "    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,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "# add this as a default assumption so later judgments work out:\n",
+    "defaults.assumptions = [Exists(x, Px), Exists(x, Not(Rx))]"
+   ]
+  },
+  {
+   "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(), # 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",
+    "]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "# check to verify the judgments look correct and as-expected:\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": "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,

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 <a class=\"ProveItLink\" href=\"../../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">booleans</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">quantification</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">existence</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#exists_not_eq_not_forall\">exists_not_eq_not_forall</a> 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
+}

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 <a class=\"ProveItLink\" href=\"../../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">booleans</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">quantification</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">existence</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#exists_not_folding\">exists_not_folding</a> 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
+}

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 <a class=\"ProveItLink\" href=\"../../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">booleans</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">quantification</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">existence</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#exists_not_unfolding\">exists_not_unfolding</a> 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
+}

packages/proveit/logic/booleans/quantification/existence/_theory_nbs_/theorems.ipynb

@@ -114,6 +114,45 @@
     "                       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,
+   "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": {},