improved backwards tactic system

Author: philzook58

kdrag/__init__.py

@@ -17,6 +17,7 @@
 NewType = notation.NewType
 
 Calc = tactics.Calc
+Lemma = tactics.Lemma
 
 R = smt.RealSort()
 Z = smt.IntSort()

kdrag/kernel.py

@@ -225,20 +225,22 @@ def instan2(ts: list[smt.ExprRef], thm: smt.BoolRef) -> Proof:
 def forget(ts: list[smt.ExprRef], pf: Proof) -> Proof:
     """
     "Forget" a term using existentials. This is existential introduction.
+    This could be derived from forget2
     """
     assert is_proof(pf)
-    vs = fresh_const(pf.thm)
+    vs = [smt.FreshConst(t.sort()) for t in ts]
     return __Proof(smt.Exists(vs, smt.substitute(pf.thm, *zip(ts, vs))), reason=[pf])
 
 
 def forget2(ts: list[smt.ExprRef], thm: smt.BoolRef) -> Proof:
     """
     "Forget" a term using existentials. This is existential introduction.
+    `thm` is an existential formula, and `ts` are terms to substitute those variables with.
     forget easily follows.
     """
-    vs = fresh_const(thm)
+    assert smt.is_quantifier(thm) and thm.is_exists()
     return __Proof(
-        smt.Implies(thm, smt.Exists(vs, smt.substitute(thm, *zip(ts, vs)))),
+        smt.Implies(smt.substitute_vars(thm.body(), *reversed(ts)), thm),
         reason="exists_intro",
     )
 

kdrag/tactics.py

@@ -198,84 +198,98 @@ def simp(t: smt.ExprRef, by: list[kd.kernel.Proof] = [], **kwargs) -> kd.kernel.
 
 
 class Lemma:
-    # Isar style forward proof
-    def __init__(self, goal):
-        self.goal = goal
-        self.lemmas = []
-        self.vars = []
-        self.hyps = []
-
-    def intro(self, vars):  # fix
-        self.vars.extend(vars)
-        return self
-
-    def assume(self, hyps):
-        self.hyps.extend(hyps)
-        return self
-
-    def _wrap(self, form):
-        return smt.ForAll(self.vars, smt.Implies(smt.And(self.hyps), form))
-
-    def have(self, conc, **kwargs):
-        self.lemmas.append(lemma(self._wrap(conc), **kwargs))
-        return self
-
-    def qed(self):
-        return lemma(self.goal, by=self.lemmas)
-
-
-class Lemma2:
     # Isar style forward proof
     def __init__(self, goal: smt.BoolRef):
         # self.cur_goal = goal
         self.lemmas = []
         self.thm = goal
-        self.goals = [goal]
+        self.goals = [([], goal)]
 
     def intros(self):
-        goal = self.goals.pop()
-        vs, herb_lemma = kd.kernel.herb(goal)
-        self.lemmas.append(herb_lemma)
-        self.goals.append(goal.thm.arg(0))
-        return vs
+        ctx, goal = self.goals.pop()
+        if smt.is_quantifier(goal) and goal.is_forall():
+            vs, herb_lemma = kd.kernel.herb(goal)
+            self.lemmas.append(herb_lemma)
+            self.goals.append((ctx, herb_lemma.thm.arg(0)))
+            return vs
+        elif smt.is_implies(goal):
+            self.goals.append((ctx + [goal.arg(0)], goal.arg(1)))
+            return self
+
+    def cases(self, t):
+        ctx, goal = self.goals.pop()
+        if t.sort() == smt.BoolSort():
+            self.goals.append((ctx + [smt.Not(t)], goal))
+            self.goals.append((ctx + [t], goal))
+        elif isinstance(t, smt.DatatypeRef):
+            dsort = t.sort()
+            for i in reversed(range(dsort.num_constructors())):
+                self.goals.append((ctx + [dsort.recognizer(i)(t)], goal))
+        else:
+            raise ValueError("Cases failed. Not a bool or datatype")
+        return self
 
-    def cases(self):
-        pass
+    def auto(self):
+        ctx, goal = self.goals[-1]
+        self.lemmas.append(lemma(smt.Implies(smt.And(ctx), goal)))
+        self.goals.pop()
+        return self
 
     def split(self):
-        goal = self.goals.pop()
+        ctx, goal = self.goals[-1]
         if smt.is_and(goal):
-            goals.extend(goal.children())
+            self.goals.pop()
+            self.goals.extend([(ctx, c) for c in goal.children()])
         else:
             raise ValueError("Split failed. Not an and")
 
     def exists(self, *ts):
-        goal = self.goals.pop()
-        # kd.kernel.forget(self.goal, t)
-        self.goals.append(utils.instan(goal, *ts))
+        ctx, goal = self.goals[-1]
+        lemma = kd.kernel.forget2(ts, goal)
+        self.lemmas.append(lemma)
+        self.goals[-1] = (ctx, lemma.thm.arg(0))
+        return self
 
     def apply(self, pf: kd.kernel.Proof):
-        goal = self.goals.pop()
-        self.lemmas.append(pf)
-        self.goals.append(utils.apply(goal, pf.thm))
-        # TODO.
-        # self.lemmas.append(pf)
-        # self.cur_goal = pf.thm.arg(0)
-        # return self
-
-    def assume(self, hyps):
-        self.goal.arg(0)
+        ctx, goal = self.goals.pop()
+        thm = pf.thm
+        if smt.is_quantifier(thm) and thm.is_forall():
+            vs, thm = kd.utils.open_binder(thm)
+        else:
+            vs = []
+        if not smt.is_implies(thm):
+            head = thm
+            body = smt.BoolVal(True)
+        else:
+            body, head = thm.children()
+        subst = kd.utils.pmatch(vs, head, goal)
+        if subst is None:
+            raise ValueError(f"Apply tactic failed to goal {goal} lemma {pf}")
+        else:
+            pf1 = kd.kernel.instan([subst[v] for v in vs], pf)
+            self.lemmas.append(pf1)
+            if smt.is_implies(pf1.thm):
+                self.goals.append((ctx, pf1.thm.arg(0)))
         return self
 
-    def _wrap(self, form):
-        return smt.ForAll(self.vars, smt.Implies(smt.And(self.hyps), form))
+    def assumption(self):
+        ctx, goal = self.goals.pop()
+        if any([goal.eq(h) for h in ctx]):
+            return self
+        else:
+            raise ValueError("Assumption tactic failed", goal, ctx)
 
     def have(self, conc, **kwargs):
-        self.lemmas.append(lemma(self._wrap(conc), **kwargs))
+        ctx, goal = self.goals.pop()
+        self.lemmas.append(lemma(smt.Implies(smt.And(ctx), conc)), **kwargs)
+        self.goals.append((ctx + [conc], conc))
         return self
 
     def __repr__(self):
-        return "?|- " + repr(self.goals[-1])
+        if len(self.goals) == 0:
+            return "Nothing to do. Hooray!"
+        ctx, goal = self.goals[-1]
+        return repr(ctx) + " ?|- " + repr(goal)
 
     def qed(self):
         return lemma(self.thm, by=self.lemmas)

kdrag/utils.py

@@ -65,7 +65,6 @@ def check_escape(x):
 
     while todo:
         pat, t = todo.pop()
-        print(todo, pat, t, subst)
         if is_var(pat):  # regular pattern
             if pat in subst:
                 if not alpha_eq(subst[pat], t):
@@ -497,6 +496,7 @@ def kbo(vs: list[smt.ExprRef], t1: smt.ExprRef, t2: smt.ExprRef) -> Order:
     """
     Knuth Bendix Ordering, naive implementation.
     All weights are 1.
+    Source: Term Rewriting and All That section 5.4.4
     """
     if t1.eq(t2):
         return Order.EQ

tests/test_kernel.py

@@ -143,8 +143,34 @@ def test_cond():
 def test_Lemma():
     x = smt.Int("x")
     l = kd.tactics.Lemma(x != x + 1)
-    l.intro([smt.Int("x")])
     l.have(x != x + 1)
+    l.assumption()
+    l.qed()
+
+    p, q, r = smt.Bools("p q r")
+    l = kd.tactics.Lemma(smt.Implies(p, p))
+    l.qed()
+
+    l = kd.tactics.Lemma(kd.QForAll([p, q], p, q, p))
+    p1, q1 = l.intros()
+    l.intros()
+    l.cases(p1)
+    l.auto()
+    l.auto()
+    l.qed()
+
+    y = smt.Int("y")
+    l = kd.tactics.Lemma(smt.Exists([x, y], smt.And(x == 2, y == 3)))
+    l.exists(smt.IntVal(2), smt.IntVal(3))
+    l.auto()
+    l.qed()
+
+    x, y, z = smt.Ints("x y z")
+    P = smt.Function("P", smt.IntSort(), smt.BoolSort())
+    myax = kd.axiom(smt.ForAll([z], P(z)))
+    l = kd.tactics.Lemma(kd.QForAll([x], P(x)))
+    x1 = l.intros()
+    l.apply(myax)
     l.qed()
 
 
@@ -200,3 +226,15 @@ def test_lambda_def():
 
 def test_bv():
     bv8 = bitvec.BVTheory(8)
+
+
+def test_forget():
+    x, y = smt.Ints("x y")
+    assert kd.kernel.forget2(
+        [smt.IntVal(2), smt.IntVal(3)], smt.Exists([x, y], smt.And(x == 2, y == 3))
+    ).thm.eq(
+        smt.Implies(
+            smt.And(smt.IntVal(2) == 2, smt.IntVal(3) == 3),
+            smt.Exists([x, y], smt.And(x == 2, y == 3)),
+        )
+    )