356 create prime number set

packages/proveit/numbers/__init__.py

@@ -1,16 +1,17 @@
 # Arithmetic and number theory concepts.
 
 from .number_sets import (
-    ZeroSet, Natural, NaturalPos,
-    Integer, IntegerEven, IntegerNonZero, IntegerNeg, IntegerNonPos,
-    IntegerOdd, Rational, RationalNonZero, RationalPos, RationalNeg,
+    ZeroSet, Natural, NaturalPos, Integer, IntegerEven,
+    IntegerNonZero, IntegerNeg, IntegerNonPos, IntegerOdd,
+    Prime, Rational, RationalNonZero, RationalPos, RationalNeg,
     RationalNonNeg, RationalNonPos,
     Real, RealNonZero, RealNeg, RealPos, RealNonNeg, RealNonPos,
     Complex, ComplexNonZero, Conjugate,
     complex_polar_coordinates, 
     unit_length_complex_polar_angle)
 
-from .number_sets import Interval, RealInterval, IntervalOO, IntervalCC, IntervalCO, IntervalOC
+from .number_sets import (
+        Interval, RealInterval, IntervalOO, IntervalCC, IntervalCO, IntervalOC)
 from .number_sets import e, pi, i, infinity
 from .number_operation import (NumberOperation, readily_factorable,
                                deduce_in_number_set,
@@ -36,7 +37,8 @@
                        less_eq_numeric_rationals,
                        not_equal_numeric_rationals,
                        deduce_not_equal_numeric_rationals)
-from .numerals import zero, one, two, three, four, five, six, seven, eight, nine, hexa, hexb, hexc, hexd, hexe, hexf
+from .numerals import (zero, one, two, three, four, five, six, seven,
+        eight, nine, hexa, hexb, hexc, hexd, hexe, hexf)
 from .addition import (Add, subtract, dist_subtract, dist_add)
 from .negation import Neg, negated
 from .ordering import (NumberOrderingRelation, number_ordering,

packages/proveit/numbers/number_sets/__init__.py

@@ -1,6 +1,6 @@
 from .integers import (
         Integer, IntegerEven, IntegerNeg, IntegerNonZero,
-        IntegerNonPos, IntegerOdd, Interval, infinity)
+        IntegerNonPos, IntegerOdd, Interval, infinity, Prime)
 from .natural_numbers import ZeroSet, Natural, NaturalPos
 from .rational_numbers import (Rational, RationalNonZero,
                                RationalPos, RationalNeg,

packages/proveit/numbers/number_sets/integers/_theory_nbs_/common.ipynb

@@ -18,8 +18,11 @@
     "# Prepare this notebook for defining the common expressions of a theory:\n",
     "%common_expressions_notebook # Keep this at the top following 'import proveit'.\n",
     "from proveit import Literal\n",
+    "from proveit.logic.sets import Set\n",
+    "from proveit.numbers import two, three, five, seven, num\n",
     "from proveit.numbers.number_sets.integers.integer import (\n",
-    "        IntegerSet, IntegerEvenSet, IntegerNegSet, IntegerNonZeroSet, IntegerNonPosSet, IntegerOddSet)\n",
+    "        IntegerSet, IntegerEvenSet, IntegerNegSet, IntegerNonZeroSet, IntegerNonPosSet,\n",
+    "        IntegerOddSet, PrimeSet)\n",
     "%begin common"
    ]
   },
@@ -77,6 +80,15 @@
     "IntegerOdd = IntegerOddSet()"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Prime = PrimeSet()"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
@@ -86,6 +98,32 @@
     "infinity = Literal('infinity',r'\\infty')"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "first_10_primes = (\n",
+    "        Set(two,     three,   five,    seven,   num(11),\n",
+    "            num(13), num(17), num(19), num(23), num(29))\n",
+    ")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "primes_less_than_100 = (\n",
+    "        Set(two, three, five, seven, num(11), num(13), num(17),\n",
+    "            num(19), num(23), num(29), num(31), num(37), num(41),\n",
+    "            num(43), num(47), num(53), num(59), num(61), num(67),\n",
+    "            num(71), num(73), num(79), num(83), num(89), num(97))\n",
+    ")"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,

packages/proveit/numbers/number_sets/integers/_theory_nbs_/demonstrations.ipynb

@@ -19,9 +19,10 @@
     "from proveit.logic import Boolean, Equals, Exists, NotEquals, InSet, NotInSet, Or\n",
     "from proveit.numbers import (Add, Neg, Less, LessEq, greater, greater_eq,\n",
     "        number_ordering, Mult, num, subtract)\n",
-    "from proveit.numbers import (zero, one, two, three, four, five, six, seven,\n",
-    "                             eight, nine, Integer, IntegerEven, IntegerNonZero, IntegerNeg, IntegerNonPos,\n",
-    "                             IntegerOdd, Interval, Natural, NaturalPos, Rational, Real)\n",
+    "from proveit.numbers import (\n",
+    "        zero, one, two, three, four, five, six, seven, eight, nine,\n",
+    "        Integer, IntegerEven, IntegerNonZero, IntegerNeg, IntegerNonPos,\n",
+    "        IntegerOdd, Interval, Natural, NaturalPos, Prime, Rational, Real)\n",
     "%begin demonstrations"
    ]
   },
@@ -1485,6 +1486,120 @@
     "InSet(num(13), IntegerOdd).prove()"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### Prime Numbers (`Prime`), Prime Membership (`PrimeMembership`)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(y, Prime)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(InSet(y, Prime), Boolean).prove()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(y, Integer).prove(assumptions=[InSet(y, Prime)])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "# A side-effect of y being prime: y is 2 or y is odd\n",
+    "Or(Equals(y, two), InSet(y, IntegerOdd)).prove(assumptions=[InSet(y, Prime)])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(y, Rational).prove(assumptions=[InSet(y, Prime)])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(y, Prime).derive_element_in_rational(assumptions=[InSet(y, Prime)])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(y, Real).prove(assumptions=[InSet(y, Prime)])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(y, Prime).derive_element_in_real(assumptions=[InSet(y, Prime)])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from proveit.numbers.number_sets.integers import first_10_primes\n",
+    "first_10_primes"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from proveit.logic.sets import Set\n",
+    "small_primes = [two, three, five, seven, num(11)]\n",
+    "for p in small_primes:\n",
+    "    display(InSet(p, Prime).conclude())"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "try:\n",
+    "    InSet(num(53), Prime).conclude()\n",
+    "except Exception as the_exception:\n",
+    "    print(f\"EXCEPTION: {the_exception}\")"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,

packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_is_two_or_odd/thm_proof.ipynb

@@ -0,0 +1,48 @@
+{
+ "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\">numbers</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">number_sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">integers</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#prime_is_two_or_odd\">prime_is_two_or_odd</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory\n",
+    "from proveit import defaults, display_provers # useful imports"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving prime_is_two_or_odd"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}

packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_membership_is_bool/thm_proof.ipynb

@@ -0,0 +1,48 @@
+{
+ "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\">numbers</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">number_sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">integers</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#prime_membership_is_bool\">prime_membership_is_bool</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory\n",
+    "from proveit import defaults, display_provers # useful imports"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving prime_membership_is_bool"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}

packages/proveit/numbers/number_sets/integers/_theory_nbs_/proofs/prime_within_int/thm_proof.ipynb

@@ -0,0 +1,48 @@
+{
+ "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\">numbers</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">number_sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">integers</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#prime_within_int\">prime_within_int</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory\n",
+    "from proveit import defaults, display_provers # useful imports"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving prime_within_int"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}