contracts

Author: philzook58

examples/real_analysis_game/README.md

@@ -0,0 +1,3 @@
+A very nice lean course on real analysis. It is particularly suited to knuckledragger because it avoids mathlib and highly generic polymorphic definitions or crazy typeclasses.
+
+<https://github.com/AlexKontorovich/RealAnalysisGame>

src/kdrag/__init__.py

@@ -14,6 +14,7 @@
 from . import utils
 from . import datatype
 from . import rewrite
+from . import contracts
 from . import tactics
 import functools
 from .parsers import microlean
@@ -46,6 +47,8 @@ def define_const(name: str, body: smt.ExprRef) -> smt.ExprRef:
     return kernel.define(name, [], body)  # type: ignore
 
 
+contract = contracts.contract
+
 FreshVar = kernel.FreshVar
 
 FreshVars = tactics.FreshVars

src/kdrag/contract.py src/kdrag/contracts.pysrc/kdrag/contract.py renamed to src/kdrag/contracts.py

@@ -1,3 +1,15 @@
+"""
+
+Contracts are a database of lemmas associated with a function symbol.
+They are usually used to specify intended pre and postconditions for functions as an abstraction over their definition.
+This can also be though of as a subtyping refinement.
+
+There is a registry which can be queried.
+
+This registry is not trusted code.
+
+"""
+
 from dataclasses import dataclass
 import kdrag.smt as smt
 import kdrag as kd
@@ -9,21 +21,17 @@ class Contract:
     args: list[smt.ExprRef]
     pre: smt.BoolRef
     post: smt.BoolRef
-    proof: kd.Proof
+    proof: kd.kernel.Proof
 
 
 contracts: dict[smt.FuncDeclRef, Contract] = {}
 
-"""
-def add_contract(f: smt.FuncDeclRef, proof: kd.Proof):
-    assert f not in contracts
-    contracts[f] = proof
-"""
 
-
-def lemmas(e: smt.ExprRef) -> list[kd.Proof]:
+def lemmas(e: smt.ExprRef, into_binders=True) -> list[kd.kernel.Proof]:
     """
-    Instantiate all contract lemmas found in
+    Instantiate all contract lemmas found in a pexression.
+    This sweeps the expression and instantiates the contract lemma with the arguments to the function.
+    Once it goes under binders, this becomes more difficult, so it returns the quantified form of the lemmas
     """
     res = []
     seen: set[int] = set([e.get_id()])
@@ -44,7 +52,8 @@ def lemmas(e: smt.ExprRef) -> list[kd.Proof]:
                     todo.append(c)
         elif isinstance(e, smt.QuantifierRef):
             # There may be variables inside here. Fallback to just giving z3
-            decls.update(kd.utils.decls(e.body()))
+            if into_binders:
+                decls.update(kd.utils.decls(e.body()))
         else:
             raise ValueError(f"Unexpected term type: {e}")
     res.extend(contracts[decl].proof for decl in decls if decl in contracts)
@@ -53,7 +62,7 @@ def lemmas(e: smt.ExprRef) -> list[kd.Proof]:
 
 def contract(
     f: smt.FuncDeclRef, args: list[smt.ExprRef], pre, post, by=None, **kwargs
-) -> kd.Proof:
+) -> kd.kernel.Proof:
     """
     Register the contract for function f: for all args, pre => post.
 
@@ -64,28 +73,21 @@ def contract(
     |= ForAll(x, Implies(x > 0, foo4392(x) > 0))
     >>> c.thm.pattern(0)
     foo4392(Var(0))
-    >>> prove(foo(5) > 0)
+    >>> kd.prove(foo(5) > 0, contracts=True)
     |= foo4392(5) > 0
-    >>> prove(foo(5) > 5)
+    >>> kd.prove(foo(5) > 5, contracts=True)
     Traceback (most recent call last):
         ...
     LemmaError: ...
     """
     assert f not in contracts
     if by is None:
-        by = lemmas(pre) + lemmas(post)
-    else:
-        by = by + lemmas(pre) + lemmas(post)
-    pf = kd.prove(smt.ForAll(args, pre, post, patterns=[f(*args)]), by=by, **kwargs)
+        by = []
+    thm = smt.ForAll(args, smt.Implies(pre, post), patterns=[f(*args)])
+    by = by + lemmas(thm)
+    pf = kd.kernel.prove(thm, by=by, **kwargs)  # Do we want kd.tactics.prove here?
     contracts[f] = Contract(f, args, pre, post, pf)
     return pf
 
 
-# def define(name, args, body, pre=None, post=None): ...
-
-
-def prove(thm: smt.BoolRef, by=[], **kwargs) -> kd.Proof:
-    by = by + [
-        contracts[decl].proof for decl in kd.utils.decls(thm) if decl in contracts
-    ]
-    return kd.prove(thm, by=by, **kwargs)
+# Special define?

src/kdrag/tactics.py

@@ -229,6 +229,7 @@ def prove(
     timeout=1000,
     dump=False,
     solver=None,
+    contracts=None,
     # defns=True,
     # induct=False,
     # simps=simps,
@@ -265,6 +266,10 @@ def prove(
     |= succ2(x) == x + 2
     >>> prove(succ(x) == x + 1, unfold=[succ])
     |= succ(x) == x + 1
+    >>> kd.contract(succ, [x], x >= 0 , succ(x) >= 0, by=[succ.defn])
+    |= ForAll(x, Implies(x >= 0, succ(x) >= 0))
+    >>> kd.prove(smt.Implies(x >=0, succ(x) >= 0), contracts=True)
+    |= Implies(x >= 0, succ(x) >= 0)
     """
     start_time = time.perf_counter()
 
@@ -278,6 +283,18 @@ def prove(
     elif not isinstance(by, list):
         by = list(by)
 
+    if contracts is None:
+        pass
+    elif contracts is True:
+        by = by + kd.contracts.lemmas(thm)
+    elif isinstance(contracts, list):
+        by = list(by)
+        for decl in contracts:
+            if decl in kd.contracts.contracts:
+                by.append(kd.contracts.contracts[decl].proof)
+            else:
+                raise KeyError(f"No contract found for {decl}")
+
     if unfold is None:
         pass
     elif isinstance(unfold, int):
@@ -1076,6 +1093,34 @@ def obtain(self, n: int | smt.QuantifierRef) -> smt.ExprRef | list[smt.ExprRef]:
                 "obtain failed. Not an exists", formula, "Available exists:", exists_f
             )
 
+    def contract(self) -> "ProofState":
+        """
+        Add contract lemmas to the context
+
+        >>> x = smt.Int("x")
+        >>> succ = kd.define("mysucc72", [x], x + 1)
+        >>> kd.contract(succ, [x], x >= 0, succ(x) >= 0, by=[succ.defn])
+        |= ForAll(x, Implies(x >= 0, mysucc72(x) >= 0))
+        >>> l = Lemma(smt.Implies(smt.And(x >= 0, succ(x) >= 0), succ(succ(x)) >= 0))
+        >>> _ = l.intros()
+        >>> l.contract()
+        [And(x >= 0, mysucc72(x) >= 0),
+        Implies(mysucc72(x) >= 0, mysucc72(mysucc72(x)) >= 0),
+        Implies(x >= 0, mysucc72(x) >= 0)]
+        ?|= mysucc72(mysucc72(x)) >= 0
+
+        """
+        self.goalctx = self.top_goal()
+        ctx, goal = self.goalctx.ctx, self.goalctx.goal
+        clemmas = kd.contracts.lemmas(goal)
+        if not clemmas:
+            raise ValueError("No contract lemmas available for goal", goal)
+        for l in clemmas:
+            self.add_lemma(l)
+        newctx = ctx + [l.thm for l in clemmas]
+        self.goals[-1] = self.goalctx._replace(ctx=newctx)
+        return self
+
     def specialize(self, n: int | smt.QuantifierRef, *ts):
         """
         Instantiate a universal quantifier in the context.