made name overlap more strict. maybe this makes external solvers easier?

Author: philzook58

examples/soft_found/lf/Basics.ipynb

@@ -91,7 +91,8 @@
   | saturday
   | sunday.
 """
-#from kdrag.all import *
+
+# from kdrag.all import *
 import kdrag as kd
 from kdrag import smt
 
@@ -118,15 +119,19 @@
   end.
 """
 d = smt.Const("d", day)
-next_weekday = kd.define("next_weekday", [d], kd.cond(
-    (d.is_monday, day.tuesday),
-    (d.is_tuesday, day.wednesday),
-    (d.is_wednesday, day.thursday),
-    (d.is_thursday, day.friday),
-    (d.is_friday, day.monday),
-    (d.is_saturday, day.monday),
-    (d.is_sunday, day.monday),
-))
+next_weekday = kd.define(
+    "next_weekday",
+    [d],
+    kd.cond(
+        (d.is_monday, day.tuesday),
+        (d.is_tuesday, day.wednesday),
+        (d.is_wednesday, day.thursday),
+        (d.is_thursday, day.friday),
+        (d.is_friday, day.monday),
+        (d.is_saturday, day.monday),
+        (d.is_sunday, day.monday),
+    ),
+)
 
 
 # %% [markdown]
@@ -155,7 +160,7 @@
 # interpreter under your favorite IDE (see the [Preface] for
 # installation instructions) and try it for yourself.  Load this
 # file, [Basics.v], from the book's Coq sources, find the above
-# example, submit it to Coq, and observe the result.) 
+# example, submit it to Coq, and observe the result.)
 #
 # Second, we can record what we _expect_ the result to be in the
 # form of a Coq example:
@@ -175,7 +180,7 @@
 this:
 """
 """Proof. simpl. reflexivity.  Qed."""
-#l.unfold(next_weekday, next_weekday)
+# l.unfold(next_weekday, next_weekday)
 l.auto(by=next_weekday.defn)
 l.qed()
 
@@ -201,7 +206,7 @@
 # We'll come back to this topic in later chapters.
 
 # %% [markdown]
-# ###  Homework Submission Guidelines 
+# ###  Homework Submission Guidelines
 #
 # (** If you are using _Software Foundations_ in a course, your
 #     instructor may use automatic scripts to help grade your homework
@@ -257,13 +262,13 @@
 #     that the grading scripts can use it for internal purposes. *)
 
 # %%
-#From Coq Require Export String.
+# From Coq Require Export String.
 
 # %% [markdown]
 # ### Booleans
 # Following the pattern of the days of the week above, we can
 # define the standard type [bool] of booleans, with members [true]
-# and [false]. 
+# and [false].
 
 # %%
 """Inductive bool : Type :=
@@ -274,7 +279,7 @@
 
 # %% [markdown]
 #  Functions over booleans can be defined in the same way as
-#     above: 
+#     above:
 
 # %%
 """
@@ -298,28 +303,42 @@
 """
 
 
-
 b, b1, b2 = smt.Consts("b b1 b2", bool)
 
 
-negb = kd.define("negb", [b], kd.cond(
-    (b.is_true, bool.false),
-    (b.is_false, bool.true),
-))
-andb = kd.define("andb", [b1, b2], kd.cond(
-    (b1.is_true, b2),
-    (b1.is_false, bool.false),
-))
-orb = kd.define("orb", [b1, b2], kd.cond(
-    (b1.is_true, bool.true),
-    (b1.is_false, b2),
-))
-
-negb1 = kd.define("negb1", [b], 
-b.match_(
-  (bool.true, bool.false),
-  (bool.false, bool.true),
-))
+negb = kd.define(
+    "negb",
+    [b],
+    kd.cond(
+        (b.is_true, bool.false),
+        (b.is_false, bool.true),
+    ),
+)
+andb = kd.define(
+    "andb",
+    [b1, b2],
+    kd.cond(
+        (b1.is_true, b2),
+        (b1.is_false, bool.false),
+    ),
+)
+orb = kd.define(
+    "orb",
+    [b1, b2],
+    kd.cond(
+        (b1.is_true, bool.true),
+        (b1.is_false, b2),
+    ),
+)
+
+negb1 = kd.define(
+    "negb1",
+    [b],
+    b.match_(
+        (bool.true, bool.false),
+        (bool.false, bool.true),
+    ),
+)
 
 kd.prove(smt.ForAll([b], negb(b) == negb1(b)), by=[negb1.defn, negb.defn])
 
@@ -357,7 +376,7 @@
 # %% [markdown]
 # We can also introduce some familiar infix syntax for the
 # boolean operations we have just defined. The [Notation] command
-# defines a new symbolic notation for an existing definition. 
+# defines a new symbolic notation for an existing definition.
 #
 
 # %%
@@ -402,9 +421,9 @@
   if b1 then true
   else b2.
 """
-negb1 = kd.define("negb1", [b], smt.If(b1.is_true, bool.false, bool.true))
-andb1 = kd.define("andb1", [b1, b2], smt.If(b1.is_true, b2, bool.false))
-orb1 = kd.define("orb1", [b1, b2], smt.If(b1.is_true, bool.true, b2))
+negb2 = kd.define("negb2", [b], smt.If(b1.is_true, bool.false, bool.true))
+andb2 = kd.define("andb2", [b1, b2], smt.If(b1.is_true, b2, bool.false))
+orb2 = kd.define("orb2", [b1, b2], smt.If(b1.is_true, bool.true, b2))
 
 
 # %% [markdown]
@@ -630,19 +649,19 @@
 # %%
 c = smt.Const("c", color)
 p = smt.Const("p", rgb)
-monochome = kd.define("monochrome", [c],
-                      c.match_(
-                          (color.black, bool.true),
-                          (color.white, bool.true),
-                          (color.primary(p), bool.false)
-                        )
-                      )
-
-isred = kd.define("isred", [c],
-                      c.match_(
-                          (color.primary(rgb.red), bool.true),
-                        default=bool.false)
-                      )
+monochome = kd.define(
+    "monochrome",
+    [c],
+    c.match_(
+        (color.black, bool.true),
+        (color.white, bool.true),
+        (color.primary(p), bool.false),
+    ),
+)
+
+isred = kd.define(
+    "isred", [c], c.match_((color.primary(rgb.red), bool.true), default=bool.false)
+)
 isred.defn
 
 # %% [markdown]
@@ -719,18 +738,13 @@
 bit = kd.Enum("bit", "B1 B0")
 nybble = kd.Struct("nybble", ("b0", bit), ("b1", bit), ("b2", bit), ("b3", bit))
 
-nybble(
-    b0=bit.B0,
-    b1=bit.B1,
-    b2=bit.B0,
-    b3=bit.B1
-)
+nybble(b0=bit.B0, b1=bit.B1, b2=bit.B0, b3=bit.B1)
 
 # %% [markdown]
 #
 #
 # (* ================================================================= *)
-# ## Numbers 
+# ## Numbers
 #
 # (** We put this section in a module so that our own definition of
 #     natural numbers does not interfere with the one from the
@@ -852,10 +866,7 @@
 
 # %%
 n = smt.Const("n", Nat)
-pred = kd.define("pred", [n], n.match_(  
-    (Nat.O, Nat.O),
-    (Nat.S(n), n)
-))
+pred = kd.define("pred", [n], n.match_((Nat.O, Nat.O), (Nat.S(n), n)))
 pred.defn
 
 # %% [markdown]

examples/soft_found/lf/Basics.py

@@ -6,7 +6,7 @@
 admit_enabled = True
 # timeout = 1000
 admit_level = 50
-
+strict_define = True
 
 # TODO: Someday, when it is annoyingly slow to check built in theories, we can add a flag to disable them
 # check_lib = True

src/kdrag/config.py

@@ -263,6 +263,15 @@ def define(name: str, args: list[smt.ExprRef], body: smt.ExprRef) -> smt.FuncDec
     if f not in defns or defns[f].ax.thm.eq(def_ax.thm):
         defns[f] = defn
     else:
+        if config.strict_define:
+            raise ValueError(
+                "Redefining function",
+                f,
+                "from",
+                defns[f].ax,
+                "to",
+                def_ax.thm,
+            )
         print("WARNING: Redefining function", f, "from", defns[f].ax, "to", def_ax.thm)
         defns[f] = defn
     if len(args) == 0:

src/kdrag/kernel.py

@@ -149,8 +149,9 @@ def define(self, args, body):
         Shorthand to define a new function for this dispatch. Calls kdrag.define.
         """
         assert isinstance(self.name, str)
-        defn = kd.define(self.name, args, body)
-        self.register(args[0].sort(), defn)
+        sort = args[0].sort()
+        defn = kd.define(sort.name() + "." + self.name, args, body)
+        self.register(sort, defn)
         return defn
 
 

src/kdrag/notation.py

@@ -32,7 +32,7 @@ class FilterMod:
     A module encapsulating filter theory over sets of type T.
 
     >>> FilterMod(smt.RealSort()).filter_full
-    |= ForAll(F, Implies(wf(F), sets(F)[K(Real, True)]))
+    |= ForAll(F, Implies(Filter_Real.wf(F), sets(F)[K(Real, True)]))
     """
 
     def __init__(self, T: smt.SortRef):

src/kdrag/theories/algebra/filter.py

@@ -127,7 +127,7 @@ def BitVecSort(N):
 BVN = BitVecN
 BVN.empty = BVN(smt.Empty(seq.Seq(BV1)))  # type: ignore
 x, y, z = smt.Consts("x y z", BitVecN)
-to_int = smt.Function("to_int", BitVecN, smt.IntSort())
+to_int = smt.Function("BitVecN.to_int", BitVecN, smt.IntSort())
 to_int = kd.notation.to_int.define(
     [x],
     smt.If(

src/kdrag/theories/bitvec.py

@@ -56,7 +56,7 @@ def Vec0(N: int) -> smt.DatatypeSortRef:
     >>> u[1]
     val(u)[X1]
     >>> dot(u, v)
-    dot(u, v)
+    Vec0_2.dot(u, v)
     """
     Fin = FinSort(N)
     S = kd.NewType("Vec0_" + str(N), smt.ArraySort(Fin, kd.R))
@@ -116,7 +116,7 @@ def Vec(N):
 u, v = kd.smt.Consts("u v", Vec3)
 # kd.notation.add.define([u, v], Vec3(u.x0 + v.x0, u.x1 + v.x1, u.x2 + v.x2))
 # kd.notation.sub.define([u, v], Vec3(u.x0 - v.x0, u.x1 - v.x1, u.x2 - v.x2))
-norm2.define([u], u.x0 * u.x0 + u.x1 * u.x1 + u.x2 * u.x2)
+# norm2.define([u], u.x0 * u.x0 + u.x1 * u.x1 + u.x2 * u.x2)
 
 cross = kd.define(
     "cross",

src/kdrag/theories/real/vec.py

@@ -357,9 +357,9 @@ def test_no_mix_keyword():
 
 def test_smart_prove():
     x = smt.Int("x")
-    f = kd.define("f", [x], x + 1)
-    g = kd.define("g", [x], x + 1)
-    d = kd.define("d", [x], f(x))
+    f = kd.define("mysilly_f20", [x], x + 1)
+    g = kd.define("mysilly_g20", [x], x + 1)
+    d = kd.define("mysilly_d20", [x], f(x))
     kd.prove(smt.ForAll([x], f(x) == x + 1), unfold=1)
     kd.prove(
         smt.ForAll([x], f(x) == x + 1),

tests/test_kernel.py

@@ -7,7 +7,6 @@
 import examples.soft_found.lf.Tactics
 notebooks = [
     "examples/nng.ipynb",
-    "examples/soft_found/lf/Basics.ipynb",
     "examples/soft_found/lf/IndProp.ipynb",
     "examples/soft_found/lf/Imp.ipynb",
     "examples/soft_found/lf/Lists.ipynb",