Formalising Counterexamples from the Greedy Method

Stream: Equational

[Shreyas Srinivas]

Is Fresh finite? Can it be replaced byFin?

[Bernhard Reinke]

it is a finite enumerative type (of order 10 in the current construction). It makes pattern matching easier, not sure if it also works that nicely with Fin.

[Shreyas Srinivas]

We can use fin_cases. It might be easier to write a tactic with Fin

[Shreyas Srinivas]

Writing a new inductive type feels a bit harder

[Bernhard Reinke]

I am almost done with my 3308 construction. In retrospect it might be also possible to work directly with ℕ ⊕ ℕ. It is definitely convenient to use inductive types for the partial solutions

[Shreyas Srinivas]

Are you setting them up manually?

[Bernhard Reinke]

I am not sure what you mean, but I guess the answer is yes.

[Bernhard Reinke]

You can have a look at the PR if you want

[Bernhard Reinke]

equational#906

[Shreyas Srinivas]

Just took a look at it and I think this can substantially benefit from Fin and fin_cases

[Shreyas Srinivas]

I am away on an academic retreat for the next two days, but if I find time, I will try to rework this proof and see if a general method can be extracted

[Eric Taucher]

(deleted)

[Shreyas Srinivas]

@Bernhard Reinke : See equational#928 where I have replaced Fresh with Fin 10. This is a draft PR and I will see if I can factor out more.

[Bernhard Reinke]

If you want, you can compare it the the new construction in 1722. The starting lemmas there are a bit more general (and hopefully useful for the other greedy methods), but I don't know where to put them

[Amir Livne Bar-on]

Would it be useful to change the carrier from the free group with generators from Nat to one with generators from an arbitrary countable set? I have the code for that in a side branch

[Bernhard Reinke]

I think it might be useful for the construction for 1729

[Shreyas Srinivas]

So I took a look at the 1722 file. A few comments:

1. I see that the adjoinFresh construction and theorems are repeated.
2. I believe FinEnum is on its way out for some reason, so using it might not be the best way to go ahead. We can use Fintype.elems and convert it to a list.
3. I think you should just use Fin n in some of the cases.

[Shreyas Srinivas]

The obvious first target for generalisation is to extract the theory of embeddings and equivalences that you are using into general theorems and instantiate them in each equation's case

[Shreyas Srinivas]

@Bernhard Reinke : If you don't mind it, I would prefer to merge equational#928 because I think it would be easier to work on the refactoring business separately

[Shreyas Srinivas]

.

[Notification Bot]

20 messages were moved here from #Equational > Thoughts and impressions thread by Shreyas Srinivas.

[Bernhard Reinke]

Please go ahead! There is also now equational#932, same doubling of adjoinFresh for now. Maybe it makes sense to merge this as well before doing the refactoring regarding adjoinFresh.

[Bernhard Reinke]

As for FinEnum: I thought this is the right class to use if you have specific bijection to a Fin n, I slightly prefer this over choosing one using Fintype or Finite. Probably one can generalize the adjoinFresh construction for countable types as well.

I think the type abbrev F := Unit ⊕ Fin dom_bound ⊕ Fin dom_bound in equational#932 makes sense and I definitively prefer it over just one Fin (1 + 2* dom_bound) , dependent elimination works better with the first type. I even thought about using an inductive type for F again, but inferring FinEnum F was easier using directly the proxy type.

[Shreyas Srinivas]

I too like FinEnum. I use it for algorithms code in lean. But it is not liked by mathlib in its current form and there is an effort to create a different API in batteries.

[Shreyas Srinivas]

I don't know when these changes will be merged upstream and cause problems during toolchain updates

[Shreyas Srinivas]

My preferred solution would be to pin the toolchain at some point to avoid having to constantly maintain the repo against upstream breakages and keep the project building. But this is my personal preference because I usually don't see upstreaming to mathlib as a priority in any of my projects.

[Shreyas Srinivas]

But for as long as we do keep up to date, the potential of a breakage caused by FinEnum remains in the near term.

[Bernhard Reinke]

Thanks for merging! :octopus: Are you planing on refactoring or should I give it a go? If so, any suggestion where to put the new adjoinFresh statements?

[Shreyas Srinivas]

Feel free to give it a try. I am usually working on this outside my work hours. We can split the work between us by refactoring in byte-sized chunks. I see three distinct pieces that are common to all the greedy method proofs. There is a type obtained as a sum type of Nat and a Fintype. This type is Equiv to Nat and there are some common associated lemmas for moving properties around. There is the part where we incorporate specific equational properties per equation, and finally there is the starting seed allocation of values to the operation table.

[Shreyas Srinivas]

I can see each of these being factored out in separate PRs

[Shreyas Srinivas]

I'll take a look at it sometime between today evening and friday evening, and take up the remaining tasks at that point

[Shreyas Srinivas]

It might be convenient to initially leave some stubs of definitions and theorems in the files for the individual equations.

[Shreyas Srinivas]

Lastly let's announce our PRs and their scope in this thread

[Amir Livne Bar-on]

Bernhard Reinke said:

I think it might be useful for the construction for 1729

Dusted off the code, and created a PR if there's still interest:
https://github.com/teorth/equational_theories/pull/933

[Shreyas Srinivas]

As a rule we only care about producing the final op function. we might want to factor out the rest of it into a tactic

[Matthew Bolan]

I'm glad to see 1076 resolved, but I notice that the dashboard now reads that we have 4 implications with no conjecture. Was something deleted?

[Matthew Bolan]

It says we are missing $1076 \to 614$ and $1076 \to 4380$

[Matthew Bolan]

Looks like they were missing from my seed list for whatever reason. I will find seeds for them right now.

[Shreyas Srinivas]

equational#932 is the last PR to touch 1076

[Shreyas Srinivas]

Did we miss some equational_result attributes?

[Matthew Bolan]

refute_seed6 should also refute 614

[Shreyas Srinivas]

@Bernhard Reinke : Would you like to make another PR to add these ?

[Bernhard Reinke]

sure, do we have already the seed for 4380?

[Shreyas Srinivas]

I think Matthew posted it in the other thread

[Shreyas Srinivas]

At least for 614

[Shreyas Srinivas]

The thread is titled "713, 1289, 1447"

[Matthew Bolan]

Ok looks like 4380 should be falsified by the first seed on my list

[Matthew Bolan]

1 2 _ 0
1 _ _ 1
3 _ _ _
_ 0 _ _

[Matthew Bolan]

I think I just copy pasted them over incorrectly somehow

[Bernhard Reinke]

Works, thanks!

[Bernhard Reinke]

Here is the PR: equational#936

[Bernhard Reinke]

Shreyas Srinivas said:

Feel free to give it a try. I am usually working on this outside my work hours. We can split the work between us by refactoring in byte-sized chunks. I see three distinct pieces that are common to all the greedy method proofs. There is a type obtained as a sum type of Nat and a Fintype. This type is Equiv to Nat and there are some common associated lemmas for moving properties around. There is the part where we incorporate specific equational properties per equation, and finally there is the starting seed allocation of values to the operation table.

I started a PR at equational#939. Factoring out adjoinFresh is done, the second layer of factoring I have only done for 1722 yet, but I can probably do the rest soon. Is this file format what you have imagined? For adjoinFresh, I am now very much noncomputable, but on the other hand this now works as well for a countable number of fresh variables.

[Shreyas Srinivas]

Yes this looks right. Do please add a module docstring on top so what we and future readers know what this file is for and what the main definitions are and what they basically mean.

[Shreyas Srinivas]

Are we using countably many fresh variables?

[Bernhard Reinke]

I am not using them yet, but maybe this is helpful for 1692, or for delaying the proof that you only use finitely many of the new variables.

[Bernhard Reinke]

I think one might be able to do https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/713.2C.201289.2C.201447/near/484164880 without the finiteness assumptions in this way

[Bernhard Reinke]

I finished the refactoring on the first two parts. I started with a 713 proof using this refactorization, should I wait for this PR to resolve before doing one for 713?

[Shreyas Srinivas]

Can't we just refactor the 713 proof to use these defs?

[Bernhard Reinke]

It already does

[Shreyas Srinivas]

Then it can be added into this PR

[Bernhard Reinke]

OK, I added it

[Shreyas Srinivas]

How much can we generalize the computation of next?

[Shreyas Srinivas]

That seems to be what's remaining

[Bernhard Reinke]

I think this the heart of each argument, not sure how much you can generalize this. Something which is definitely more boilerplate is the verification of initial seeds, given by fromList_ok. Maybe one can do something there. Not sure if it is worth the effort though, since (I think) only 1289 is remaining. The other greedy methods do not follow the same adjunction scheme

[Matthew Bolan]

63 could be done similarly as well, but I think @Amir Livne Bar-on has claimed it and might be formalizing the translation invariant argument for it instead.

[Amir Livne Bar-on]

Sorry, I've been a bit out of touch. Aren't we talking about greedy constructions of translation-invariant operations? We already have some regular greedy constructions that were converted automatically from Vampire outputs IIUC

[Matthew Bolan]

63 has a proof which greedily constructs a translation-invariant operation, but also a proof that's just a regular greedy algorithm, more in the style of what Bernhard Reinke has been formalizing lately. The last batch of regular greedy algorithms are somewhat incompatible with the ones produced automatically by vampire - they often adjoin more than one element at a time, and they ask laws of the partial magmas that are not consequences of the equation being targeted.

[Terence Tao]

I should add that these newer "regular greedy algorithms" were mostly obtained by deconstructing @Pace Nielsen 's earlier translation-invariant greedy constructions. Roughly speaking, every time a relation of the form $f(a^{-1} b) = c$ appears in such a construction, one can attempt to replace it with its non-translation-invariant counterpart $a \diamond b = c$. This isn't a 100% deterministic operation because there is occasionally some freedom in how to "naturally" factor the argument $a^{-1} b$ of $f$ into its component pieces $a^{-1}, b$, but in practice the deconstruction was able to work for most of the extant translation-invariant arguments (though some new edge cases sometimes showed up that required some fiddling).

[Amir Livne Bar-on]

In the case of 63, the translation-invariant construction looks conceptually simpler, since the regular greedy algorithm proceeds in two "waves". That's why I chose to formalize that. But it may be easier to use the regular greedy construction if there's a clear recipe for formalizing this kind of proofs.

[Terence Tao]

At this point I think we have many viable options, so you should just go ahead and formalize the option you are most comfortable with.