1518

Stream: Equational

[Bernhard Reinke]

Bernhard Reinke said:

Hello, I think I have a counterexample that shows that 1648 does not imply 206. The magma is supported on the integers and defined as follows

$$x ◇ y = x - sign(y - x)$$

I think a variant of this satisfies 1518, namely
x ◇ y = y + 1 if $y \geq x$ and x ◇ y = y - 2 otherwise. I think it should not satisfy 3862 (or many of the unknowns)

[Bernhard Reinke]

Actually I looked at 2054, I think signs might be wrong from the dualization

[Bernhard Reinke]

Ok, also for 2054 this doesn't work directly, I think I have to adjust the formula again

[Notification Bot]

3 messages were moved here from #Equational > 1648 !=> 206 by Bernhard Reinke.

[Bernhard Reinke]

I think a greedy translation based approach should work here. I was trying to get a very simple example for the integers, but it turns out more complicated than I hoped, I would be happy to let someone else take over

[Bernhard Reinke]

Pace Nielsen said:

Here is 1518.

Equation1518.pdf
Equation1518.tex

I want to have a go at formalizing this. Is there any greedy (non-commutative) translation invariant approach that was already formalized? Also, I think the implications for finite magmas are still open, so in principle this might be superseded by a finite model.

[Bernhard Reinke]

I think Obelix has a translation invariant approach, I will try to follow this

[Notification Bot]

2 messages were moved here from #Equational > Outstanding equations, v1 by Bernhard Reinke.

[Bernhard Reinke]

@Pace Nielsen, I think there is an issue with (7) for the starting configuration. If $(x_2 *x_1^{-1}, x_1^{-1}) \in E_0$, then $x_2 * x_1^{-1}$ does not satisfy (7).

[Bernhard Reinke]

I will try to formalize another noncommutative greedy approach in the mean time

[Bernhard Reinke]

I think I will try to formalize 1516 !=> 1489

[Terence Tao]

You may find exists_greedy_chain to be useful.

[Pace Nielsen]

@Bernhard Reinke I just looked at that file, and I don't know what I was thinking. :surprise: Conditions 5--7 are just wrong. I checked with Vampire and the translation ansatz should work, and I have a good idea how to fix it quickly (and get simpler conditions). I'll post a correction soon.

[Pace Nielsen]

Equation1518-corrected.pdf
Equation1518-corrected.tex

@Bernhard Reinke I've double-checked this. Hopefully all the bugs were fixed.

[Bernhard Reinke]

Looks good! I am now mostly focusing on formalizing 1516, but I want to do it in a way that is easily adjustable to the other noncommutative greedy methods. I will have a closer look again once I am finished with 1516

[Terence Tao]

May or may not be relevant, but I believe the 1516 argument does not require noncommutativity. In the version I wrote in https://teorth.github.io/equational_theories/blueprint/1516-chapter.html I was able to use the integers as the carrier for the translation invariant model. This may not actually make it any easier to formalize, especially since you seem interested in handling the noncommutative case anyways, but just wanted to mention the option.

[Bernhard Reinke]

I guess when I started at looking at the formalization of 1516 !=> 1489, there wasn't a proof for 1516 !=> 255. I guess I could pivot to another noncommutative case, in particular I am following this proof at the moment, I guess the model for 1516 !=> 255 can also show 1489 along the way

[Terence Tao]

The proof of 1516 !=>255 has, as its first step, the construction of a translation invariant model with one extra property. It could also conceivably be done using the original noncommutative construction, so if you end up formalizing the original proof of 1516 !=> 1489, I think it can be repurposed to also help obtain 1516 !=> 255.

[Bernhard Reinke]

Ok, then I will proceed with the noncommutative construction for 1516

[Terence Tao]

From the point of view of Lean formalization it may in fact be of almost identical difficulty. For a human we generally think better when working in a familiar carrier such as the integers, as opposed to the free nonabelian group on infinitely many generators, but Lean doesn't really care either way.

[Bernhard Reinke]

Ok, I have a first draft for1516 !=> 1489 at equational#831. I am not yet showing the things needed for the second level of the greedy construction.

On a technical level, I am not super happy with the data structures I chose for the partial solutions, but I noticed this only gradually and comparing to the file dealing with 854.

[Terence Tao]

Would some of the results about the free group be suitable to place in the Mathlib or ForMathlib folder?

[Bernhard Reinke]

there are some lemmas that also work for general free groups. In particular, one lemma I show is that no element of a free group has order 2, but I do this a bit ad hoc. I think a nice addition would be a discussion about cyclically reduced words, and a resulting proof that every nontrivial element in a free group has infinite order.

I have some lemmas about "fresh" generators, but here I am not sure how much general interest there is in mathlib for the free group on countable generators. But this is useful for other translation invariant approaches.

I saw that @Amir Livne Bar-on is now also working on a translation invariant model, maybe he can have look and say what woud be useful for him, and we can try to find a suitable place for it

[Amir Livne Bar-on]

I'm only starting, but there's already some interesting differences. The reason I shared the code at an initial state is exactly to be able to share language with other people who work on t-i-greedy.

After a first look, it seems like you prove simple equalities about free group elements with decide and tauto, while I've been having trouble using them. I'll check what you did differently and learn from it. Also the countability proof is different.

There's a lot of theory of the free group that relates to concrete usage that should go in Mathlib. Probably nobody used it foe calculations before so there are only high-level properties of the reduction relation.

[Bernhard Reinke]

The greedy method for 1518 is now formalized, see equational#849 . This time I tried to follow the data type structure as in the proof of 854, and extract an aesop strategy, the general statements for it are now in FreshGenerator.lean. So far the technique for proving inequalities involving fresh generators is a bit primitive (and should also work in the free abelian group). I am curious to have a look at a translation invariant method where we really use noncommutativity.

[Bernhard Reinke]

The technique is pretty robust, at least 1526 was doable with only small edits, see equational#852

[Bernhard Reinke]

I guess 917 should be also a small variant

[Terence Tao]

Glad to see that one can recycle some code! I guess the number of outstanding implications that can be solved by this method is not so large that it is worth trying to automate it further, but perform ad hoc code reuse instead...

[Bernhard Reinke]

OK, 917 is now also done, see equational#853.

[Terence Tao]

This is an impressive formalization speed! How mechanical are you finding the process of adapting the arguments from one construction to another?

[Bernhard Reinke]

Somewhat mechanical: the things that need the most adjusting are the interplays between the different rules, but the parts of the argument that are dealing with the fresh generators are pretty uniform.

I should note that I am also restricting myself to the constructions that are very similar to the ones I have looked at so far.
They all share the feature that you can understand them via one extension step, where there are only two types of new relations added. So 1722 should be also quickly doable, but for example 3306 seems tedious to do.

[Terence Tao]

There is an alternate arrangement of 3308 (as well as most of the other outstanding implications) that uses a more "classic" greedy algorithm rather than a translation invariant one at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/713.2C.201289.2C.201447/near/482066500 . I guess it will be clearer how to handle it as one gets more experience formalizing the greedy arguments.