Pull Request from sudhindu/Prove-It master branch

build.py

@@ -10,8 +10,8 @@
 import itertools
 import re
 import time
-import lxml  # Comment in for Python 3
-from lxml import etree  # Comment in for Python 3
+#import lxml  # Comment in for Python 3
+#from lxml import etree  # Comment in for Python 3
 import shutil
 import argparse
 import nbformat
@@ -23,8 +23,8 @@
 import base64
 import datetime
 import tarfile
-# import urllib#Comment out for Python 3
-import urllib.request  # Comment in for Python 3
+import urllib#Comment out for Python 3
+#import urllib.request  # Comment in for Python 3
 import zmq  # to catch ZMQError which randomly occurs when starting a Jupyter kernel
 import proveit
 from proveit import Theory

build_alt.py

@@ -16,15 +16,15 @@
 import argparse
 import nbformat
 from nbconvert.preprocessors import Preprocessor, ExecutePreprocessor
-#from nbconvert.preprocessors.execute import executenb
+from nbconvert.preprocessors.execute import executenb
 from nbconvert import HTMLExporter
 import IPython
 from IPython.lib.latextools import LaTeXTool
 import base64
 import datetime
 import tarfile
-# import urllib#Comment out for Python 3
-import urllib.request  # Comment in for Python 3
+import urllib#Comment out for Python 3
+#import urllib.request  # Comment in for Python 3
 import zmq  # to catch ZMQError which randomly occurs when starting a Jupyter kernel
 import proveit
 from proveit import Theory

packages/proveit/linear_algebra/_theory_nbs_/theorems.ipynb

@@ -18,10 +18,10 @@
     "# Prepare this notebook for defining the theorems of a theory:\n",
     "%theorems_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
-    "from proveit import n\n",
+    "from proveit import n, K,H\n",
     "from proveit.logic import Forall, InSet, CartExp, InClass\n",
     "from proveit.numbers import NaturalPos, Rational, Real, Complex\n",
-    "from proveit.linear_algebra import VecSpaces"
+    "from proveit.linear_algebra import VecSpaces,InnerProdSpaces"
    ]
   },
   {
@@ -51,6 +51,13 @@
     "    domain = NaturalPos)"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
   {
    "cell_type": "code",
    "execution_count": null,
@@ -119,7 +126,7 @@
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   }

packages/proveit/linear_algebra/inner_products/_theory_nbs_/axioms.ipynb

@@ -53,7 +53,7 @@
     "    (K, H), Equals(\n",
     "        InClass(H, InnerProdSpaces(K)),\n",
     "        And(InClass(H, VecSpaces(K)),\n",
-    "            Forall((x, y), InSet(InnerProd(x, y), K)))))"
+    "            Forall((x, y), InSet(InnerProd(x, y), K), domain=H))))"
    ]
   },
   {
@@ -157,7 +157,7 @@
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   }

packages/proveit/linear_algebra/inner_products/_theory_nbs_/demonstrations.ipynb

@@ -15,6 +15,12 @@
    "outputs": [],
    "source": [
     "import proveit\n",
+    "from proveit import defaults\n",
+    "from proveit.numbers import Complex, NaturalPos, Real\n",
+    "from proveit.linear_algebra import InnerProdSpaces, HilbertSpaces, InnerProd\n",
+    "from proveit import n, v, w, x, y, K, H, U, V\n",
+    "from proveit.linear_algebra.inner_products import inner_prod_field_membership, inner_prod_complex_membership\n",
+    "from proveit.logic import CartExp, InClass, InSet\n",
     "%begin demonstrations"
    ]
   },
@@ -23,7 +29,200 @@
    "execution_count": null,
    "metadata": {},
    "outputs": [],
-   "source": []
+   "source": [
+    "defaults.assumptions=[InClass(U,HilbertSpaces),\n",
+    "                      InClass(V, InnerProdSpaces(K)), InClass(H, HilbertSpaces),\n",
+    "                      InSet(v, V), InSet(w, V), InSet(x, H), InSet(y, H)]"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### Testing the instantiation of some theorems underlying important `InnerProd` methods."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "inner_prod_field_membership.instantiate({H:V,x:v,y:w})"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "inner_prod_complex_membership.instantiate({H:H,x:x,y:y})"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### Testing some `InnerProd` and `InnerProdSpaces` methods and related `VecSpaces` methods."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### Some new default assumptions:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "defaults.assumptions = [\n",
+    "    InSet(n, NaturalPos), InSet(v, CartExp(Complex, n)), InSet(w, CartExp(Complex, n)),\n",
+    "    InSet(x, CartExp(Real, n)), InSet(y, CartExp(Real, n))]"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### Notice that we can deduce that the Cartesian products $C^{n}$ and $R^{n}$ are contained in the appropriate classes of vector spaces:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Cn_vec_space_claim = CartExp(Complex, n).deduce_as_vec_space()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Rn_vec_space_claim = CartExp(Real, n).deduce_as_vec_space()"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### We can find a specific “including” vector space for our Cartesian products as well, though in the case of Cartesian products we get a Cartesian product back again and not technically a vector space with an associated field attribute:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from proveit.linear_algebra.vector_spaces import including_vec_space\n",
+    "Cn_including_vec_space = including_vec_space(CartExp(Complex, n), field=Complex)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Rn_including_vec_space = including_vec_space(CartExp(Real, n), field=Real)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### Notice that the “including” vector space returned in the case of a Cartesian product is just the Cartesian product itself and not an explicit vector space with associated field attribute:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "try:\n",
+    "    some_field = Cn_including_vec_space.field\n",
+    "except Exception as the_exception:\n",
+    "    print(f'{the_exception}')"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### We can form the inner product of two vectors:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InnerProd(v, w)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### And we can deduce the inner product's membership in a specified field:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InnerProd(v, w).deduce_membership(Complex)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InnerProd(x, y).deduce_membership(Real)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InnerProd(v, x).deduce_membership(Complex)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "##### We see an (expected) error if we try to deduce that an inner product is Real when one vector is in $\\mathbb{R}^{n}$ while the other vector is in $\\mathbb{C}^{n}$:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "try:\n",
+    "    InnerProd(v, x).deduce_membership(Real)\n",
+    "except Exception as the_exception:\n",
+    "    print(f'Exception: {the_exception}')"
+   ]
   },
   {
    "cell_type": "code",
@@ -37,7 +236,7 @@
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   }

packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/allowed_presumptions.txt

@@ -0,0 +1 @@
+proveit.logic.equality.sub_right_side_into

packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_inner_prod_space/thm_proof.ipynb

@@ -15,6 +15,8 @@
    "outputs": [],
    "source": [
     "import proveit\n",
+    "from proveit import defaults\n",
+    "from proveit.linear_algebra.inner_products import hilbert_space_def\n",
     "theory = proveit.Theory() # the theorem's theory"
    ]
   },
@@ -27,6 +29,42 @@
     "%proving hilbert_space_is_inner_prod_space"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "defaults.assumptions = hilbert_space_is_inner_prod_space.all_conditions()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "hilbert_space_def"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "hilbert_space_def.sub_right_side_into(hilbert_space_is_inner_prod_space.condition)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%qed"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
@@ -37,7 +75,7 @@
  ],
  "metadata": {
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": "Python 3 (ipykernel)",
    "language": "python",
    "name": "python3"
   }

packages/proveit/linear_algebra/inner_products/_theory_nbs_/proofs/hilbert_space_is_vec_space/allowed_presumptions.txt

@@ -0,0 +1,2 @@
+proveit.linear_algebra.inner_products.hilbert_space_is_inner_prod_space
+proveit.linear_algebra.inner_products.inner_prod_space_is_vec_space