Presentations of the form x = f(x,y,...) are simple

Stream: Equational

[Bolton Bailey]

Looking at the view for all the presently known implications, the first unknown implication right now is Equation9[x = x ∘ (x ∘ y)] =?=> Equation152[x = (x ∘ x) ∘ (x ∘ y)]

I claim this is a non-implication. We can construct a magma over all elements of the free magma over Nat where x ∘ (x ∘ y) does not match any subterm. The magma operation on a and b would return the expression a ∘ b if that didn't match any x ∘ (x ∘ y), and would return x = a if a ∘ b matched some x ∘ (x ∘ y). This magma is well-defined because in both cases, the result doesn't have any subterm matching x ∘ (x ∘ y):

1. If a ∘ b doesn't match x ∘ (x ∘ y) at the top level, then since a and b don't match in any subterm, no subterm of a ∘ b matches, and the expression a ∘ b is therefore part of the carrier.
2. If a ∘ b does match x ∘ (x ∘ y) at the top level, then the result is a, which is known to be in the carrier

This magma now satisfies the Equation9 (update: no it doesn't), but not Equation152, since 0 and (0 ∘ 0) ∘ (0 ∘ 1) are distinct elements of the carrier. This gives us the non-implication.

More broadly, this construction seems to work for any equation of the form x = f(x,y,...) (with a bare variable on one side). Is this right? Is the project aware of this idea? How can it best be included?

[Bolton Bailey]

Also, correct me if I'm wrong, but I think this is what in group theory would be called a "presentation". If we reduce the equation on the right hand side of the implication, does this not just decide any implication from a magma equation of this form?

[Daniel Weber]

I don't think this model satisfies equation 9 - setting x = 0, y = 0 ∘ 1, x ∘ y = 0 and x ∘ (x ∘ y) = 0 ∘ 0 != x

[Terence Tao]

Note that you are overloading the ∘ operation for both the free magma operation and the modified magma operation. If you give them two distinct symbols, I think you might see the problem more clearly

[Bolton Bailey]

Yep, I'm wrong, at least I got a proof of implication out of the counterexample (though presumably egg will be able to find this pretty easily)

theorem Equation9_implies_Equation152 (G : Type*) [Magma G] [Finite G] (h : Equation9 G) :
    Equation152 G := by
  unfold Equation9 at h
  have : ∀ (x : G), x = x ◇ x := by
    intro x
    have := h x (x ◇ x)
    rw [<-h x x] at this
    exact this
  unfold Equation152
  intro x y
  rw [<-this x]
  apply h

[Terence Tao]

I guess you can upload it to Subgraph.lean (and move 9 and 152 over to Equations.lean) if you have the time... every little bit helps. (Perhaps in the future we would have a more automated submission tool.)

[Johan Commelin]

Note that the magmas of #Equational > 3102 does not imply 3176 are of this form.

[Johan Commelin]

I think that for equations of the form x = f(x, y) where f is not of the form g(x, y) \diw g(x, y), it is probably possible to build magmas in a very similar way to what I did by hand. But you somehow need to be able to "invert" f and extract x from f(x, y). At least with g(x, y) \diw g(x, y) that isn't possible, and there might be other exceptions as well.

[Johan Commelin]

Edit: I retract this claim.

I guess the condition is: we always have $f(x, y, \dots) = f_1(x, y, \dots) \diamond f_2(x, y, \dots)$ and when can we extract $x$ from $f_1(x, y, \dots)$ and $f_2(x, y, \dots)$?
Suppose that $m_i$ (resp. $n_i$) is the number of occurences of $x$ (resp. $y$) in $f_i$. If the matrix

$$\begin{pmatrix} m_1 & n_1 \\ m_2 & n_2 \end{pmatrix}$$

is invertible, then we can determine the length of x and y. In particular, we can find the substrings x and y, and match whether two strings a and b are of the form $f_1(x, y, \dots)$ and $f_2(x, y, \dots)$.

So in that scenario we can define a magma on strings by using string concatenation a ++ b unless a and b are exactly of the form $f_1(x, y, \dots)$ and $f_2(x, y, \dots)$ and in that case, extract x and return that as result instead.

There might be more general f for which we can do something, but I think this is already quite a general class.

Edit: I retract this claim.

[Bolton Bailey]

Ok, I was still curious about the structure of the magma presented by/of equation 9, so I decided to use the proof assistant to assist me. I believe what follows is a formalization of the statement that if you exclude both x ∘ (x ∘ y) and x ∘ x as subexpressions, then the magma you get by the construction I attempted earlier, with the additional simplification of x ∘ x to x does, in fact, satisfy equation 9.

import equational_theories.Equations
import equational_theories.AllEquations
import Mathlib.Data.Fintype.Card
import Mathlib.NumberTheory.Padics.PadicVal.Basic
import equational_theories.ForMathlib.Algebra.Group.Nat
import equational_theories.FreeMagma
import Mathlib.Data.Subtype

def matches9 (G : Type*) : FreeMagma G → Prop
  | FreeMagma.Fork x (FreeMagma.Fork y _) => x = y
  | _ => false

def subexpr_matches9 (G : Type*) : FreeMagma G → Prop
  | FreeMagma.Fork x y => matches9 G (FreeMagma.Fork x y) ∨ subexpr_matches9 G x ∨ subexpr_matches9 G y
  | _ => false

def matches3 (G : Type*) : FreeMagma G → Prop
  | FreeMagma.Fork x y => x = y
  | _ => false

def subexpr_matches3 (G : Type*) : FreeMagma G → Prop
  | FreeMagma.Fork x y => matches3 G (FreeMagma.Fork x y) ∨ subexpr_matches3 G x ∨ subexpr_matches3 G y
  | _ => false

def MagmaPresented9 (α : Type) : Type := { val : FreeMagma α // ¬ subexpr_matches9 (α) val ∧ ¬ subexpr_matches3 (α) val}

open Classical

noncomputable def opMagmaPresented9 {α} (a b : MagmaPresented9 α) : MagmaPresented9 α :=
  if h1 : subexpr_matches9 α (FreeMagma.Fork a.val b.val) then ⟨a.val, a.property⟩
  else if h2 : subexpr_matches3 α (FreeMagma.Fork a.val b.val) then ⟨a.val, a.property⟩
  else ⟨FreeMagma.Fork a.val b.val, by
    apply And.intro
    exact h1
    exact h2
  ⟩

noncomputable instance MagmaMagmaPresented9 {α} : Magma (MagmaPresented9 α) := ⟨opMagmaPresented9⟩

theorem opMagmaPresented9_obeys9 {α} : Equation9 (MagmaPresented9 α) := by
  intro x y
  unfold Magma.op MagmaMagmaPresented9 opMagmaPresented9
  simp

  have h1' : subexpr_matches3 α (x.val ⋆ x.val) := by
    simp [subexpr_matches3]
    left
    simp [matches3]
  have h2' : subexpr_matches9 α (x.val ⋆ (x.val ⋆ y.val)) := by
    simp [subexpr_matches9]
    left
    simp [matches9]

  by_cases h1 : subexpr_matches9 α (x.val ⋆ y.val) <;> by_cases h2 : subexpr_matches9 α (x.val ⋆ x.val)
  <;> by_cases h3 : subexpr_matches3 α (x.val ⋆ y.val)  <;> simp [h1, h2, h3, h1', h2']

[Bolton Bailey]

I do not pretend to understand if there is some deep meaning here about what characterizations we can make of which presented magmas, at this point Lean knows more than me.

[Hernan Ibarra]

Not sure if I'm understanding correctly, but the metatheorems you have seem very similar to the ones of Chapter 8. @Johan Commelin

[Hernan Ibarra]

In any case here is a proof of 9 \notimplies 152. The dual of 9 [x = (y x) x] has the same rightmost variable on the LHS and the RHS, while 152 does not have this property. The result now follows from (the dual of) Metatheorem 8.2.

[Johan Commelin]

@Hernan Ibarra Somewhat. But in my case we have x on the left, whereas on the right we have two variables. I didn't find a metatheorem about that.

[Hernan Ibarra]

Oh I just realized the implication 9 -> 152 was proven. There must be something wrong with my argument. (EDIT: Ah I forgot to dualize 152)

[Terence Tao]

Btw lists of dual pairs are available at https://github.com/teorth/equational_theories/blob/main/data/dual_equations.md

[Hernan Ibarra]

(So 9 does not imply 166)

[Terence Tao]

Does this suggest that one of your metatheorems could productively resolve a fair number of open implications? I could set this as a task (one can output the list conjecturally first, if the metatheorem has not been formalized in Lean, then work to formalize the list in Lean later).

[Terence Tao]

Wait, post-egg, we almost know completely what Equation9 implies and doesn't imply at this point (the graph visualization tool lists only 2852 as unresolved)

[Terence Tao]

... which is weird. 9 implies 23, which implies 2582 by another application of 9

[Hernan Ibarra]

Terence Tao said:

Does this suggest that one of your metatheorems could productively resolve a fair number of open implications? I could set this as a task (one can output the list conjecturally first, if the metatheorem has not been formalized in Lean, then work to formalize the list in Lean later).

Oh yes, me and @Anand Rao Tadipatri are working on this already. All of the metatheorems found so far are computationally tractable.

[Hernan Ibarra]

Anand is hoping we can formalize the metatheorems in Lean, but outputting a conjectural list is not a bad idea (and would be much easier).

[Bolton Bailey]

Somewhat surprised that egg didn't find 9 implies 2852: x = ((x ◇ (x ◇ y)) ◇ x) ◇ x should reduce to x = (x ◇ x) ◇ x and then to x = x ◇ x and then to x = x. What expressions is egg currently being given?

[Terence Tao]

Oh, right, egg isn't running on all 22 million pairs I believe, this is maybe why there is some weirdness

[Terence Tao]

It could be worth reviving one of the older simple substitution scripts to seek out and eliminate these sorts of leftover low hanging fruit

[Terence Tao]

(older == ~5 days old :joy: )

[Terence Tao]

I opened equational#284 to see if this phenomenon is prevalent

[Vlad Tsyrklevich]

I suspect this ticket won't be necessary after equational#281 lands. The reason it wasn't caught with EquationSearch is that the crude method of sub-expression matching I use does not allow replacing sub-expressions unless they have the exact same variables in starting and ending sub-expressions, this is due to complexity introduced by having to rebind variables in the rest of expression (in this case no rebinding is necessary so I could have actually implemented this without too much trouble, but I got bogged down by a more general implementation and it stalled there.)

[Terence Tao]

OK. It looks like equational#281 is basically ready to merge but I wanted to be sure that there werent any further obvious optimizations to be done there before adding it to the Lean codebase. The proofs are numerous and moderately large, but it looks like the compiler can handle it; so maybe it's already okay as it is, in which case I will approve it and close equational#284.

[Johan Commelin]

Fwiw, I retract my meta-claim.