Theorem decorator

Author: philzook58

src/kdrag/tactics.py

@@ -1460,3 +1460,36 @@ def qed(self, **kwargs) -> kd.kernel.Proof:
         if self._parent is not None:
             self._parent.exact(pf)
         return pf
+
+
+def Theorem(
+    goal: smt.BoolRef,
+) -> Callable[[Callable[[ProofState], None]], kd.kernel.Proof]:
+    """
+    A decorator to create a theorem from a function that takes a `ProofState` as argument.
+
+    >>> x = smt.Int("x")
+    >>> @Theorem(x + 1 > x)
+    ... def mytheorem(l: ProofState):
+    ...     "An example theorem"
+    ...     l.auto()
+    >>> mytheorem
+    |= x + 1 > x
+    >>> mytheorem.__doc__
+    'An example theorem'
+    """
+
+    def res(f: Callable[[ProofState], None]) -> kd.kernel.Proof:
+        l = kd.Lemma(goal)
+        f(l)
+        pf = l.qed()
+        # To override metadata of the returned proof
+        # Proof is frozen, so this is a bit fishy
+        # @functools.update_wrapper had assumptions about return type being a function
+        object.__setattr__(pf, "__doc__", getattr(f, "__doc__", None))
+        object.__setattr__(pf, "__module__", getattr(f, "__module__", None))
+        object.__setattr__(pf, "__name__", getattr(f, "__name__", None))
+        object.__setattr__(pf, "__qualname__", getattr(f, "__qualname__", None))
+        return pf
+
+    return res

src/kdrag/theories/logic/__init__.py

@@ -59,25 +59,30 @@ def slemma(thm, by=[], **kwargs):
     )
 )
 
-l = kd.Lemma(smt.ForAll([A], (A == emp) == smt.Not(smt.Exists([x], elem(x, A)))))
-_A = l.fix()
-l.split()
-with l.sub() as l1:
-    l1.intros()
-    l1.intros()
-    _x = l1.obtain(-1)
-    l1.show(smt.BoolVal(False), by=[ext_ax, elem_emp])
-with l.sub() as l2:
-    l2.intros()
-    l2.rw(ext_ax)
-    _x = l2.fix()
-    l2.apply(0)
-    l2.exists(_x)
-    l2.have(elem(_x, emp) == smt.BoolVal(False), by=[elem_emp(_x)])
-    l2.have(elem(_x, _A), by=[])
-
-    l2.auto()
-emp_exists_elem = l.qed()
+
+# l = kd.Lemma(smt.ForAll([A], (A == emp) == smt.Not(smt.Exists([x], elem(x, A)))))
+@kd.tactics.Theorem(smt.ForAll([A], (A == emp) == smt.Not(smt.Exists([x], elem(x, A)))))
+def emp_exists_elem(l):
+    _A = l.fix()
+    l.split()
+    with l.sub() as l1:
+        l1.intros()
+        l1.intros()
+        _x = l1.obtain(-1)
+        l1.show(smt.BoolVal(False), by=[ext_ax, elem_emp])
+    with l.sub() as l2:
+        l2.intros()
+        l2.rw(ext_ax)
+        _x = l2.fix()
+        l2.apply(0)
+        l2.exists(_x)
+        l2.have(elem(_x, emp) == smt.BoolVal(False), by=[elem_emp(_x)])
+        l2.have(elem(_x, _A), by=[])
+
+        l2.auto()
+
+
+# emp_exists_elem = l.qed()
 
 
 l = kd.Lemma(smt.ForAll([A], smt.Implies((A != emp), smt.Exists([x], elem(x, A)))))

src/kdrag/theories/logic/zf.py

@@ -376,4 +376,6 @@ def test_smart_prove():
     #with pytest.raises(Exception) as _:
     #    kd.prove(smt.ForAll([x], f(x) == g(x)), unfold=[g])
     with pytest.raises(kd.kernel.LemmaError):
-        kd.prove(smt.ForAll([x], d(x) == x+1), unfold=1)
+        kd.prove(smt.ForAll([x], d(x) == x+1), unfold=1)
+
+