Proposal: Add Finite typeclasses to non-implications

Stream: Equational

[Vlad Tsyrklevich]

Just for fun I started working on some local scripts to try to generalize the 2 simple proofs we have of Austin pairs to other non-implications. I've hit the roadblock that it is not possible to derive the list of non-implications without finite proofs without resorting to some ugly hacks. I built a small proof-of-concept locally, changing one (finite) non-implication from ∃ (G : Type) (_ : Magma G), Facts G [...] [...] to ∃ (G : Type) (_ : Magma G) (_: Finite G), Facts G [...] [...] and then plumbing support for this through the @[equational_result] attribute into lake exe extract_implications to pull this data out.

My proposal is to add support for this upstream, first adding support for parsing this form of theorem correctly, and then going through and re-factoring all non-implications we have in the repository to explicitly add the Finite typeclass where appropriate. I think it would also be interesting to then consider adding Infinite to the rest, and if no issues come up then enforcing that new non-implications have one of the two going forward to keep this from rotting.

I am not experienced with Lean, so objections or design suggestions are very welcome!

[Vlad Tsyrklevich]

Outside of the Austin pair motivation, I think it may also be interesting to see if there are non-implications that we did not discover at the beginning because they are only captured by large finite magmas and we were able to rule them out with infinite constructions before realizing they had this property. In the other direction, if there is some 'abstract nonsense' way to construct infinite counterexamples from finite ones then it would be possible to prove that they are as complete as the set of all known non-implications, though whether this is difficult/trivial/interesting to others is not something I can answer.

[Terence Tao]

That's a nice extension to the original project (namely, to calculate the "finite magma implication graph" as well as the "arbitrary magma implication graph", the former being the latter minus the Austin pairs). If there is some relatively painless way to add Finite tags to the (99% of the) anti-implications that were disproven by finite means, that would certainly help with this extended version of the project.

We know that all commutative linear counterexamples have a finite model (this observation in fact basically goes back to the original paper of Austin, and was recently formalized (equational#442). On the other hand, the greedy constructions are inherently infinitary in nature, and they have been used to resolve anti-implications (Asterix <-> Obelix, Dupont <-> Dupond, Hardy -> Ramanujan, etc.) that are known to be immune to finite models. They also have been used to resolve implications for which we don't know how to use finiteness (and, as @Will Sawin observed some time ago, all of our uses of finiteness boil down to one trick, namely to pass from injectivity to surjectivity or vice versa). To give one recent example, we can now construct greedy (translation-invariant) countermodels of 3308, but it's not clear at all what happens if we require finiteness here.

[Mario Carneiro]

Are there any examples of nonimplications where counterexamples are necessarily finite? The only case that comes to mind is that a model of the singleton law is necessarily a singleton, but this will not feature in any counterexamples.

[Will Sawin]

Mario Carneiro said:

Are there any examples of nonimplications where counterexamples are necessarily finite? The only case that comes to mind is that a model of the singleton law is necessarily a singleton, but this will not feature in any counterexamples.

No, since for every non-singleton finite model you can take an infinite product of copies of it which is infinite but satisfies all the same laws.

[Mario Carneiro]

Oh, that's a nice result to have

[Mario Carneiro]

That does mean that it's unnecessary to have a `∃ (G : Type) (_ : Magma G) (_: Infinite G), ... theorem since you can upgrade any counterexample to an infinite one

[Mario Carneiro]

I don't think you necessarily want to have a rule saying every counterexample must be one or the other, several proofs produce countable but not obviously infinite models, and abstract nonsense constructions like FreeMagmaWithLaws could go either way in general

[Will Sawin]

Mario Carneiro said:

I don't think you necessarily want to have a rule saying every counterexample must be one or the other, several proofs produce countable but not obviously infinite models, and abstract nonsense constructions like FreeMagmaWithLaws could go either way in general

Yeah, the main things of interest for this are (1) collecting all disproofs using models known to be finite and (2) automating proofs that implications hold in the finite case using the injective implies surjective step. There's no need to figure out if models that are not obviously infinite are in fact finite, until steps (1) and (2) both fail.

[Shreyas Srinivas]

I don't know of any painless way to add those tags in the main branch directly. . If your suggestion is to "detect finite counterexample > add attribute" this will be hard and add merge conflicts to PRs which are also working on counterexamples.

One dirty trick might be to generate new versions of each counterexample theorem with the extra [Finite G] instance and copy the proofs verbatim, with an extra let declaration that creates a Finite instance and tries to run "interInstance" on it. Then delete those theorems which have an error. I don't have enough metaprogramming skills to do this

[Shreyas Srinivas]

Put these theorems in a separate folder and generate the Vitalstatistix of finite counterexamples from that folder

[Shreyas Srinivas]

I don't wish to rule out the first option either, but we will need a metaprogramming expert to check whether that is feasible and implement it

[Daniel Weber]

Will Sawin said:

Yeah, the main things of interest for this are (1) collecting all disproofs using models known to be finite and (2) automating proofs that implications hold in the finite case using the injective implies surjective step. There's no need to figure out if models that are not obviously infinite are in fact finite, until steps (1) and (2) both fail.

I could try doing (2), but (1) should be done before that to avoid running on all implications which are known to have a finite counterexample

[Terence Tao]

Yeah, that should cut things down by 99% or so hopefully from the raw 13 million. We could also look at extremal anti-implications (not implied by any other anti-implication) just to get started. It's still going to be a far larger set though than the 88 (!) conjecturally open implications we have right now - we've relied a fair bit on infinitary methods (particularly confluence, saturation, and greedy methods) to get us to this point.

[Vlad Tsyrklevich]

Shreyas Srinivas said:

I don't know of any painless way to add those tags in the main branch directly

There are only ~1k non-implication theorems on main and most of them are in a few auto-generated folders. I think this refactor should be fairly trivial.

I also don't think it will lead to merge conflicts as 1) all of the active work is necessarily not on simple operator-table non-implications, and 2) anyways if it does lead to a merge conflict it should be a trivially resolvable one

[Vlad Tsyrklevich]

Will Sawin said:

(2) automating proofs that implications hold in the finite case using the injective implies surjective step

This is exactly what I had begun doing before realizing I didn't have the data I needed.

[Vlad Tsyrklevich]

I'll take a look at converting most of the auto-generated finite non-implications before submitting anything upstream, to ensure that I have a good working model first.

[Vlad Tsyrklevich]

I was able to convert all but 11.5k non-implications in the closure with relatively little effort. I have to get some work done now, but I'll return to it this evening to clean it up and cover the remaining finite counterexamples.

[Amir Livne Bar-on]

We probably want to change the transitive reduction to only rely on finite-cardinality implications

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

all of the active work is necessarily not on simple operator-table non-implications

Well, speak of the devil. (I still don't think it should be an issue though.)

[Vlad Tsyrklevich]

equational#702 is just the plumbing necessary to correctly parse Finite non-implications and report them in extract_implications, no theorems are updated yet (though that change has already been staged and tested locally.)

[Vlad Tsyrklevich]

This has been merged, but a review would still be appreciated from anyone with more Lean experience

[Vlad Tsyrklevich]

equational#711 and equational#712 should finish this off by marking non-implications with the Finite typeclass. I've started generating some Austin pair proofs locally and next I'll work on trying to get finite implications wired into extract_implications locally and then propose something

[Vlad Tsyrklevich]

equational#729 completes this series and allows adding Finite to implications as well. Note that I've updated the extract_implications script to ignore finite implications by default and tested this. Comments welcome.

[Michael Bucko]

Vlad Tsyrklevich schrieb:

equational#729 completes this series and allows adding Finite to implications as well. Note that I've updated the extract_implications script to ignore finite implications by default and tested this. Comments welcome.

Can you please elaborate on GraphEdge? It's not yet in the latest main.

[Vlad Tsyrklevich]

GraphEdge is added in one of the commits in that PR: https://github.com/teorth/equational_theories/pull/729/commits/ec74640b0dba9045b835de72fd1db60f7cd21b2c

It's a refactor to not use the ParseImplications.Implication structure, as the Closure code was just using it as a general data structure to store edges, but that no longer works after this change (since a finite Bool is added), so I changed it to use it's own structure.