Fix distinct variable checking for proof dummy variables.

1 files changed, 13 insertions, 7 deletions

diff --git a/ghilbert.py b/ghilbert.py
index c9c17b0..1a89e94 100755
--- a/ghilbert.py
+++ b/ghilbert.py
@@ -127,14 +127,13 @@ def has_var(ix, expr, argmap):
             return True
     return False
 
-def relvarsof(expr, vset, relvars):
+def relvarsof(expr, vset):
     if expr[0] is Ghilbert.VARIX:
-        if expr[2] < relvars:
-            vset.add(expr[2])
+        vset.add(expr[2])
     else:
         # (Ghilbert.TERM, termid[1], termid, subexp, ...)
         for e in expr[3:]:
-            relvarsof(e, vset, relvars)
+            relvarsof(e, vset)
 
 # This one probably doesn't need to be a method...
 def hyp_match(e_stack, e_proto, vmap):
@@ -1303,6 +1302,11 @@ class Ghilbert():
         # Disjoint variable handling
         # Only worry about variables that occur in the hypotheses or
         # conclusions of the theorem.
+        # But suppose the statement we are applying requires the variables
+        # in the substitutions for two of its variables to be disjoint,
+        # but they are not, but the intersection involves only variables
+        # that are not in the hypotheses or conclusions of the theorem
+        # being proven. We still want to prevent such a use.
         relvars = pip.nvars
         dvs = e[6]
         if dvs != None:
@@ -1311,23 +1315,25 @@ class Ghilbert():
                 vset1 = dvarsmap[v]
                 if vset1 is None:
                     vset1 = set()
-                    relvarsof(vmap[v], vset1, relvars)
+                    relvarsof(vmap[v], vset1)
                     dvarsmap[v] = vset1
                 vset2 = dvarsmap[w]
                 if vset2 is None:
                     vset2 = set()
-                    relvarsof(vmap[w], vset2, relvars)
+                    relvarsof(vmap[w], vset2)
                     dvarsmap[w] = vset2
                 for u1 in vset1:
                     for u2 in vset2:
                         if u1 == u2:
-                            u = invert(pip.vdict, u1)
+                            u = pip.vlist[u1][2]
                             raise VerifyError(
                                 _("Disjoint variable violation for "
                                   "(%(var1)s, %(var2)s) applying %(stmt)s :"
                                   "substitutions for both contain %(var3)s")
                                 % {"var1" : vlist[v][2], "var2" : vlist[w][2],
                                    "stmt" : e[1], "var3" : u})
+                        if u1 >= relvars or u2 >= relvars:
+                            continue
                         if u1 < u2:
                             pip.dvreqs.add((u1, u2))
                         else: