Problem with the Python verifier

[Paul Merrell]

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

[Adam Bliss]

+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.
For more options, visit https://groups.google.com/groups/opt_out.

[Paul Merrell]

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]

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
+)
+!reject test.gh something about freemaps

[Adam Bliss]

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.

--Adam

--
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.

[Jim Kingdon]

Excellent! Thanks for fixing that.

To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

--

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.