Eq 1729 vs Eq 917

Stream: Equational

[Shreyas Srinivas]

I finally got to work on 1729 vs 917. See below the code from the equation explorer:

import Mathlib.Tactic

class Magma (α : Type _) where
  op : α → α → α

infix:65 " ◇ " => Magma.op

abbrev Equation1729 (G: Type _) [Magma G] := ∀ x y : G, x = (y ◇ y) ◇ ((y ◇ x) ◇ y)

abbrev Equation917 (G: Type _) [Magma G] := ∀ x y : G, x = y ◇ ((y ◇ y) ◇ (x ◇ y))

theorem Equation1729_implies_Equation917 (G: Type _) [Magma G] (h: Equation1729 G) : Equation917 G := by
  sorry
theorem Equation1729_not_implies_Equation917 : ∃ (G: Type) (_: Magma G), Equation1729 G ∧ ¬ Equation917 G := by
  sorry

I finally found some time to work on this, and because I had just started learning z3, I ran the following naive python z3 script:

from z3 import *

def main():
    x = Int('x')
    y = Int('y')
    s = Solver()
    op = Function('op', IntSort(), IntSort(), IntSort())
    s.add(x == op((op(y,y),op(op(y,x),y))))
    s.add(x != op(y, op(op(y,y), op(x,y))))
    print (s)
    res = s.check()
    if res == sat:
        print(s.model())

if __name__ == '__main__':
    main()

[Shreyas Srinivas]

I got back the following claimed counter example:

x == op(op(y, y), op(op(y, x), y)),
 x != op(y, op(op(y, y), op(x, y)))]
[x = 4,
 y = 0,
 op = [(0, 4) -> 2,
       (2, 0) -> 3,
       (1, 3) -> 4,
       (4, 0) -> 5,
       (1, 5) -> 6,
       (0, 6) -> 7,
       else -> 1]]

[Shreyas Srinivas]

Since I am new to this whole ATP business, I want to check if this is really doing what I think it is

[Shreyas Srinivas]

More specifically, I can't believe it would be this easy, so where am I going wrong?

[Amir Livne Bar-on]

This can't be, since all squares are 1, and left-multiplication by 1 is not surjective. I'm not familiar with z3, but probably it's missing a "for all" somewhere?

[Shreyas Srinivas]

I am following this guide here: https://ericpony.github.io/z3py-tutorial/guide-examples.htm

[Shreyas Srinivas]

In particular the section on functions

[Matthew Bolan]

I think z3 is telling you that for x=4 and y=0, 1729 is satisfied but not 917, but it is not claiming that 1729 is satisfied for all x and y. You can see in the model how it has specified x and y.

[Shreyas Srinivas]

Right that makes more sense

[Shreyas Srinivas]

But I don't get that from the tutorial docs

[Michael Bucko]

Matthew Bolan schrieb:

I think z3 is telling you that for x=4 and y=0, 1729 is satisfied but not 917, but it is not claiming that 1729 is satisfied for all x and y. You can see in the model how it has specified x and y.

You could try something like this?

implication = ForAll([x, y],
    Implies(
        x == d(d(y, y), d(d(y, x), y)),
        x == d(y, d(d(y, y), d(x, y)))
    )
)

(I'll have a look at that one too a little bit later)

EDIT: and then

s.add(Not(implication))

[Shreyas Srinivas]

that looks stronger. In fact it's saying that the Eq 917 will not satisfy that equality for any x and y. We just need it to dissatisfy the equation at some x and y

[Shreyas Srinivas]

I think this is correct:

def main():
    x = Int('x')
    y = Int('y')
    s = Solver()
    set_param(proof= True)
    op = Function('op', IntSort(), IntSort(), IntSort())
    eq1729 = ForAll([x, y], x == op(op(y, y), op(op(y, x), y)))
    not_eq917 = Exists([x,y], x != op(y, op(op(y,y), op(x,y))))
    s.add(eq1729)
    s.add(not_eq917)
    print (s)
    res = s.check()
    if res == sat:
        m = s.model()
        print(m)
        print("eq 1729 : ", m.evaluate(op((op(y,y),op(op(y,x),y)))))
        print("eq 719: ", m.evaluate(op(op(y,y), op(x,y))))

[Shreyas Srinivas]

I think in the previous example z3 interpreted all my constraints as existentials. Makes sense in hindsight

[Shreyas Srinivas]

And I am guessing now I can add more constraints and refine this search.

[Shreyas Srinivas]

Is this correct?

[Shreyas Srinivas]

More specifically how do I ensure that z3 uses my constraints to prune the search?

[Michael Bucko]

It looks good to me, but perhaps I am missing something. I only recently started experimenting with Python z3 API.

I ran your latest script, but it didn't give me a counterexample.

[Shreyas Srinivas]

I wouldn't expect it to terminate fast

[Shreyas Srinivas]

I ran it for an hour before deciding I need to take my machine home

[Shreyas Srinivas]

In fact the first reason I thought my initial answer was wrong was because how fast it finished

[Michael Bucko]

Btw. tried with Duper. 100,000 heartbeats - fail. Running 1,000,000 heartbeats now.

[Michael Bucko]

1,000,000 heartbeats was also a fail. Scared to run 10,000,000 :joy:

[Shreyas Srinivas]

I don't expect unconstrained search to succeed in reasonable time

[Shreyas Srinivas]

The above script is a starting point

[Michael Bucko]

Duper with 10,000,000 heartbeats finished after ca. 10 minutes. Didn't work.