# Problem with the Python verifier

24 views

### Paul Merrell

Dec 5, 2013, 2:07:18 AM12/5/13
I think we have a serious problem with verify.py. I wrote a theorem that proves that 1=2 after violating a freeness constraint. I wrote this in peano/peano_thms.gh:

thm (unfree19.9 () () (= (1) (2))
x (2) tyex
x (= x (2)) 19.9
mpbi
x (1) tyex
x (= x (1)) 19.9
mpbi
EqReplaceEq0
)

The javascript verify.js correctly identifies the mistake. (It doesn't immediately tell you it's wrong in the editor you have to actually check it in, but that's something I'm thinking of working on.)

verify.py seems to be OK with this theorem. I can try to investigate, but I'm terrible with Python.

Paul

Dec 5, 2013, 2:17:41 AM12/5/13

+1 for "this is a serious problem"!

I have reproduced this result with an older version of verify.py. I'm not sure what's going on, since I've had it catch similar freeness violations in the past.

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.

### Paul Merrell

Dec 6, 2013, 1:16:30 AM12/6/13
I haven't looked at the python verifier, but quick update on the javascript verifier. Now freeness violations show up immediately when you type them or when you close the theorem. If you have a missing or an extra freeness constraint, it alerts you in the editor and you can fix it with one click. If the conclusion in the theorem header doesn't match the proof stack you can correct that with one click too.

### Jim Kingdon

Dec 12, 2013, 2:05:10 AM12/12/13
On 12/04/2013 11:07 PM, Paul Merrell wrote:
> I think we have a serious problem with verify.py. I wrote a theorem
> that proves that 1=2 after violating a freeness constraint.

Good catch. Here's a test case that reproduces it (the python verifier
flunks the test; the javascript one appears to pass it):

diff --git a/testsuite b/testsuite
index 0c033c5..7671f0f 100644
--- a/testsuite
+++ b/testsuite
@@ -706,4 +706,27 @@ stmt (KindMismatchInInterface () () (= (separate x
φ φ) (separate x φ φ)))
!append in.ghi
stmt (ExpectedBindingGotTerm () () (= (separate A A φ) (separate A A φ)))
!reject test.gh Expected a binding variable, found term variable A
+!unshare
+
+# Attempt to apply a theorem which violates a freeness constraint
+!append axioms.ghi
+kind (formula)
+tvar (formula p q φ)
+term (formula (↔ p q))
+
+kind (object)
+tvar (object s t A B C)
+var (object x y)
+term (formula (= s t))
+term (object (1))
+
+term (formula (∃ x φ))
+stmt (ThereExistsAddRemove ((φ x)) () (↔ (∃ x φ) φ))
+!append test.gh
+import (AXIOMS axioms.ghi () "")
+var (object x)
+thm (bad () () (↔ (∃ x (= x (1))) (= x (1)))
+ x (= x (1)) ThereExistsAddRemove
+)

Dec 20, 2013, 1:20:28 AM12/20/13

Thanks for the report (Paul) and the test case (Jim). I finally got around to investigating this today, and the bug was super simple: a function was called for its boolean return value but had no "return" keyword, so I guess Python decided its return value should always be "False". How helpful! :)

I pushed the fix and the new test case to the repo.

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+unsubscribe@googlegroups.com.