Refutations using Z3

Stream: Equational

[Daniel Weber]

Using Z3 I was able to refute Equation4283[x ∘ (x ∘ y) = x ∘ (y ∘ x)] => Equation4358[x ∘ (y ∘ z) = x ∘ (z ∘ y)]:
x | 0 | 1 | 2 | 3 | 4 | 5 | 6
--- | --- | --- | --- | --- | --- | --- | ---
0 | 1 | 1 | 1 | 4 | 1 | 6 | 1
1 | 1 | 1 | 3 | 1 | 1 | 1 | 1
2 | 1 | 5 | 1 | 1 | 5 | 1 | 5
3 | 1 | 1 | 1 | 1 | 1 | 1 | 1
4 | 1 | 1 | 3 | 1 | 1 | 1 | 1
5 | 1 | 1 | 1 | 1 | 1 | 1 | 1
6 | 1 | 1 | 3 | 1 | 1 | 1 | 1
With x = 0, y = 1, z = 2

[Daniel Weber]

How do I get it to display as a table?

[Nicholas Carlini]

	0	1	2	3	4	5	6
0	1	1	1	4	1	6	1
1	1	1	3	1	1	1	1
2	1	5	1	1	5	1	5
3	1	1	1	1	1	1	1
4	1	1	3	1	1	1	1
5	1	1	1	1	1	1	1
6	1	1	3	1	1	1	1

[Daniel Weber]

One typo of mine led to whether Equation4585[(x ∘ x) ∘ x = (x ∘ y) ∘ y] implies Equation4341[x ∘ (y ∘ y) = x ∘ (z ∘ z)], and Z3 is unable to resolve this. Any suggestions? It feels like it should be false

[Henrik Böving]

I'd suggest to try at least CVC4 or 5 and potentially vampire, these systems are usually better at first (and higher) order reasoning than Z3

[Daniel Weber]

Vampire was able to refute it

[Shreyas Srinivas]

There is another thread on vampire

[Daniel Weber]

Yes, I'm aware, but it's about using it for proving implications, not producing counterexamples

[Daniel Weber]

Can there be implications which are only refuted on infinite magmas?

[Seraphina Nix]

I would have to assume there can be, or at least I don't see why there wouldn't be, but I haven't thought of a proof yet. It would be interesting to find an implication which is true for all finite magmas, but not true for an infinite magma (or prove that no such implication could exist).

[Terence Tao]

It is known by the way that there are systems of equations with no finite models, e.g., https://link.springer.com/chapter/10.1007/978-1-4899-2608-1_14 , though I don't know of a single-equation magma law with this property (there are single-equation groupoid laws).

[Cody Roux]

Is it worth trying to programmatically generate lean models from the Z3 models? I'm looking for a little project where I won't get creamed by people working faster than me...

[Terence Tao]

Sounds like a good project to me. You could create an issue on the github to declare your interest in this topic, so that anyone else who is interested can reach out to you, or know that you are on the case and work on something else instead.

[Daniel Weber]

As mentioned above, you might want to also use other solvers, but Z3 is a good start. Also, you might want to take a look at #Equational > Memoizing finite magmas for kernel-friendly reduction for discussion on how these models can be stored in Lean

[Joachim Breitner]

Although I wouldn't put the “encoded table” in the lean source. The table as an array of arrays would probably be a good interchange format here (and we can make sure that ita elaborated to the compact form for evaluation behind the scenes)

[Cody Roux]

I was thinking of declaring an inductive and generating an explicit function over it which encodes the multiplication table, but I can try to be more flexible.

The huge advantage of Z3 here is the Python API which gives some kind of datatype you can iterate over with counter-models; I don't know that Vampire is offering anything like that.

Indeed I'm not sure whether SMT-Lib even really standardizes the counter-models (it probably does tbh).

[Cody Roux]

https://github.com/teorth/equational_theories/issues/67

[Daniel Weber]

I think you should be able to comment "claim" on it to be automatically assigned to it

[Shreyas Srinivas]

I will get the issue added to the project dashboard.

[Shreyas Srinivas]

Pietro is working on the automation part. I can assign it to you if you wish

[Cody Roux]

yes please!

[Shreyas Srinivas]

when you start a PR please follow the contribution guidelines to get the PR linked to the issue

[Joachim Breitner]

Using Fin has the advantage over a custom inductive type that for example the universal quantifiers has a Decidable instance, so that all the equations can be checked with by decide. And that you can also use general machinery like my op-memoization elaborator.

[Joachim Breitner]

You can still write the operation as an explicit function, I guess.

[Cody Roux]

I'm just deriving Fintype, though we'll see if that scales, I guess. At any rate it seems hard to avoid quadratic work at the time being.

[Cody Roux]

Done with the draft version! Now I need to re-learn how to create a github PR...

[Shreyas Srinivas]

If you have already

1. Created a fork of the repository
2. Created a branch in your fork.
3. Pushed your changes to this branch

[Shreyas Srinivas]

Then when you go to the GitHub page of your fork, GitHub will offer a yellow banner with a green button on one side asking if you want to "Compare and pull request"

[Cody Roux]

I think I have it? https://github.com/teorth/equational_theories/pull/92

Honestly git scares me more than algebra.

[Cody Roux]

Very happy to hear feedback on usability though

[Cody Roux]

Ideally one would plug in the equations generator to be able to pick two equations to try, however I haven't stared at that script yet.

[Shreyas Srinivas]

An algebraic theory of git would certainly prove that point

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

The automation worked. Your PR is "In Progress"

[Shreyas Srinivas]

(deleted)

[Cody Roux]

I would love an algebraic theory of Linus' naming conventions as well

[Cody Roux]

I'm psyched my little script made it in! I have a couple improvements in mind:

1. Tell the user if the implication was proven rather than erroring out
2. have a function that takes in two numbers, grabs the relevant equations and tries to generate a counter-example

I was actually going to do 2 before merging the WIP PR.

What's the process here? Make a new issue, or directly make a PR?

[Cody Roux]

It's https://github.com/teorth/equational_theories/pull/95, if required I'll either submit an issue, close the PR and re-submit or whatever is preferred.