show tactic

Author: philzook58

examples/nng.ipynb

@@ -24,14 +24,21 @@
     "python3 -m pip install -e ."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "If the following cell fails after first installation, you may need to restart the notebook runtime"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": null,
    "metadata": {},
    "outputs": [],
    "source": [
     "import kdrag as kd\n",
-    "import kdrag.smt as smt\n",
+    "import kdrag.smt as smt # smt is essentially a reexport of z3\n",
     "\n",
     "#Or for short:\n",
     "#from kdrag.all import *"
@@ -820,6 +827,7 @@
    "outputs": [],
    "source": [
     "l = kd.Lemma(smt.ForAll([n,m], n + Nat.Succ(m) == Nat.Succ(n + m)))\n",
+    "l\n",
     "# TODO"
    ]
   },

kdrag/tactics.py

@@ -553,6 +553,15 @@ def generalize(self, *vs):
         self.goals.append(goalctx._replace(goal=smt.ForAll(vs, goalctx.goal)))
         return self.top_goal()
 
+    def show(self, thm: smt.BoolRef):
+        """
+        To document the current goal
+        """
+        goal = self.top_goal().goal
+        if not thm.eq(goal):
+            raise ValueError("Goal does not match", thm, goal)
+        return self.top_goal()
+
     def assumption(self):
         """
         Exact match of goal in the context