Syntax

Stream: Equational

[Adam Topaz]

Here is a sketch of how one can express equations and implications between them in a purely syntactic way within lean. The type MagmaRel should correspond to the type of "equations" that appear in the repo, and the type MagmaImpl R S should correspond to an implication between two such equations:

inductive MagmaWord : Nat → Nat → Type where
  | id (A : Nat) : MagmaWord A A
  | comp {A B C : Nat} : MagmaWord A B → MagmaWord B C → MagmaWord A C
  | fst (X Y : Nat) : MagmaWord (X + Y) X
  | snd (X Y : Nat) : MagmaWord (X + Y) Y
  | lift {T X Y : Nat} :
      MagmaWord T X → MagmaWord T Y → MagmaWord T (X + Y)
  | toNil (L : Nat) : MagmaWord L 0
  | mul : MagmaWord 2 1

structure MagmaRel where
  source : Nat
  lhs : MagmaWord source 1
  rhs : MagmaWord source 1

inductive MagmaRel.rel (R : MagmaRel) : {A B : Nat} → MagmaWord A B → MagmaWord A B → Prop where
  | of : R.rel R.lhs R.rhs
  | rfl {A B : Nat} (e : MagmaWord A B) : R.rel e e
  | symm {A B : Nat} {e f : MagmaWord A B} : R.rel e f → R.rel f e
  | trans {A B : Nat} {e f g : MagmaWord A B} : R.rel e f → R.rel f g → R.rel e g
  | id_comp {A B : Nat} (e : MagmaWord A B) : R.rel (MagmaWord.comp (.id _) e) e
  | comp_id {A B : Nat} (e : MagmaWord A B) : R.rel (MagmaWord.comp e (.id _)) e
  | assoc {A B C D : Nat} (e : MagmaWord A B) (f : MagmaWord B C) (g : MagmaWord C D) :
      R.rel ((e.comp f).comp g) (e.comp (f.comp g))
  | comp_congr {A B C : Nat} (e e' : MagmaWord A B) (f f' : MagmaWord B C) :
      R.rel e e' → R.rel f f' → R.rel (e.comp f) (e'.comp f')
  | lift_fst {T X Y : Nat} (e : MagmaWord T X) (f : MagmaWord T Y) :
      R.rel ((e.lift f).comp (.fst _ _)) e
  | lift_snd {T X Y : Nat} (e : MagmaWord T X) (f : MagmaWord T Y) :
      R.rel ((e.lift f).comp (.snd _ _)) f
  | lift_unique {T X Y : Nat} (e f : MagmaWord T (X + Y)) :
      R.rel (e.comp (.fst _ _)) (f.comp (.fst _ _)) →
      R.rel (e.comp (.snd _ _)) (f.comp (.snd _ _)) →
      R.rel e f
  | toNil_unique {X : Nat} (e f : MagmaWord X 0) : R.rel e f

structure MagmaImpl (R S : MagmaRel) where
  impl (h : ∀ {A B : Nat} (e f : MagmaWord A B), R.rel e f) : S.rel e f

Here is some further explanation: The type MagmaWord A B (with A B : Nat) are expressions which correspond to functions M^A -> M^B where M is a magma, which can be built entirely in the language of magmas. A term of MagmaRel is then just the information of representatives of two such functions M^A -> M for some fixed A. The MagmaRel.rel is the inductive proposition of all relations built out of the given MagmaRel.

[Shreyas Srinivas]

why reinvent equality?

[Adam Topaz]

The benefit of this is that everything is completely syntactically explicit, so that one can, for example, generate random terms of MagmaRel.

[Shreyas Srinivas]

I wonder if we could follow the approach of the egg repo

[Adam Topaz]

You can do that directly with the Magma typeclass, but that would require more metaprogramming.

[Adam Topaz]

Can you explain what the egg approach is?

[Shreyas Srinivas]

They use existing typeclasses. They have a tactic called egg, this takes a list of intermediate milestones to produce a chain of rewrites to the goal from the axioms

[Shreyas Srinivas]

they use a variation of equality saturation procedures which takes the intermediate steps into account

[Adam Topaz]

Ok, but does this not mean that there is an internal (meta) representation of the equality which is a term of a type that's roughly similar to the one above?

[Shreyas Srinivas]

@Andrés Goens would be able to explain the internals better than me, but they probably do have some representation of equality that helps them outsource to the egg tool

[Shreyas Srinivas]

https://egraphs-good.github.io/

[Shreyas Srinivas]

But it works across different typeclasses rather for one algebraic theory, whereas I get the impression that we would have to build a new type for each algebraic theory in the approach you have suggested.

[Adam Topaz]

Shreyas Srinivas said:

But it works across different typeclasses rather for one algebraic theory, whereas I get the impression that we would have to build a new type for each algebraic theory in the approach you have suggested.

If you want to generalize, you can do so with this approach (this is what I mentioned elsewhere about Lawvere theories). Of ourse Lawvere theories don't cover all algebraic classes (e.g. Fields), but they do cover everything from universal algebra.

[Shreyas Srinivas]

I am out of my depth with Lawvere theories.

[Shreyas Srinivas]

But I suppose that's the limitation with that approach as Terence Tao mentioned

[Shreyas Srinivas]

That one needs to know Lawvere theories to work on such an inductive type.

[Adam Topaz]

They don't matter too much for the purposes of this project. But it seems to me that even if you go with egg's approach, you still have to convert a usual lean equation about magmas to some intermediate expression (in principle it could even just be something involving Lean.Expr) before passing it off in some controlled way to whatever external tool. The examples of the equations appearing in the project look like $\forall x y, x * y = y * x$ and $\forall x y z, x * (y * z) = (x * y) * z$. If you want to capture all of those in some uniform way, you need to keep track of how many variables there are (2 in the first equation, 3 in the second, etc.) and that's literally all that's happening in the code above.

[Shreyas Srinivas]

Yeah, but egg has done that for us already

[Shreyas Srinivas]

I just added it as a dependency

[Adam Topaz]

Oh ok, that's a different story.

[Shreyas Srinivas]

Shreyas Srinivas said:

https://egraphs-good.github.io/

@Terence Tao : This tool might belong in your list of tools in the README. The underlying data structure e-graph is an efficient representation of equivalences and dependencies of a network of equations.

[Terence Tao]

I like the idea of refactoring the Lean code using some class for formal Magma words, as it may allow some of the graph management to be done easily within Lean rather than by an external tool, though as I said before the important thing is that there is enough API that it would be painless for someone with a casual knowledge of both math and Lean to be able to prove implications under such a refactoring, presumably by using existing proofs as a template.

[Shreyas Srinivas]

I think egg's internal representation is more likely to be universal than a specific inductive type for algebraic structures like magmas

[Adam Topaz]

It's possible to convert back and forth between such formal representations and concrete ones involving just the Magma class using metaprogramming. I'm under the impression that having the formal representation within lean itself would be a positive (note that egg itself is written in rust, and it looks like lean-egg's formal representations seem very close to just docs#Lean.Expr )

[Shreyas Srinivas]

In principle one can make an inductive type an instances of the typeclass and get it's benefits for free. The inductive type would essentially be the "free" word version of the typeclass

[Shreyas Srinivas]

This requires no metaprogramming.

[Shreyas Srinivas]

But I am not sure it is trivial to build the convenience of an existing API

[Andrés Goens]

The egg tactic internally uses Lean.Expr yes, and equality is Eq

[Shreyas Srinivas]

Reimplementing egg in lean is a different project altogether imho

[Andrés Goens]

And so the equations are just Lean Eq terms (with universal quantifiers before for all the variables)

[Adam Topaz]

@Shreyas Srinivas the free magma on how many variables?

[Andrés Goens]

so what @Adam Topaz is suggesting here just sounds like a deep embedding of equality in Magmas instead of a shallow one using Lean's equality directly

[Shreyas Srinivas]

Adam Topaz said:

Shreyas Srinivas the free magma on how many variables?

This is a bit of hindsight, but there can be a var constructor parametrised by variable numbers, so as many as you choose to add in the context.

[Andrés Goens]

Terence Tao said:

I like the idea of refactoring the Lean code using some class for formal Magma words, as it may allow some of the graph management to be done easily within Lean rather than by an external tool, though as I said before the important thing is that there is enough API that it would be painless for someone with a casual knowledge of both math and Lean to be able to prove implications under such a refactoring, presumably by using existing proofs as a template.

I think the point about accessibility (making it painless for someone with casual knowledge of math/Lean to prove implications) does speak more in favor of the shallow embedding, unless we do some sort of unembedding in the meta code to translate things back to the deep variant

[Andrés Goens]

Adam Topaz said:

Shreyas Srinivas the free magma on how many variables?

I guess it's essentially free on the (countably infinite) set type of variables Lean.Name, but you could always translate it to the free magma on the variables that appear in the (Lean) terms

[Shreyas Srinivas]

The only possible disadvantage of a shallow embedding is if you want to be certain that none of the already proven theorems in Mathlib are being used and you are able to trace all proofs back to axioms through a rewrite chain

[Andrés Goens]

that's a good point, although I guess it should be realtively simple to write a linter for that

[Adam Topaz]

This is not an issue. You can use free magmas to construct a term of MagmaImpl provided you prove eq1 implies eq2 in whatever way you want.

[Shreyas Srinivas]

You are right. This is not an issue with your deep embedding. Only with using mathlib's existing typeclasses

[Andrés Goens]

Adam Topaz said:

This is not an issue. You can use free magmas to construct a term of MagmaImpl provided you prove eq1 implies eq2 in whatever way you want.

but the question is how do you go backwards? i.e. if you have a proof over [Magma α] it would be hard to get that translated over to MagmaRel

[Adam Topaz]

Yes, that's true. This is where you need some meta code.

[Adam Topaz]

The main benefit of MagmaImpl is that this captures precisely the arrows in the graph considered in this project.

[Shreyas Srinivas]

In order to do a good deep embedding you want to create your own equality type and implement egg in lean. This could in principle be pursued in parallel with experiments using lean-egg which could use Mathlib typeclasses

[Shreyas Srinivas]

Basically deep embedding => recreating lots and lots of API before it becomes comfortable and easy to use

[Adam Topaz]

Another benefit is that you can generate terms of MagmaRel directly in Lean. If you want to do this with a shallow embedding, then you still need to essentially implement (more-or-less) the same meta code.

[Andrés Goens]

it does sound like you could have your cake and eat it too with the metaprogramming of lifting things back to MagmaRel

[Andrés Goens]

Adam Topaz said:

Another benefit is that you can generate terms of MagmaRel directly in Lean. If you want to do this with a shallow embedding, then you still need to essentially implement (more-or-less) the same meta code.

not sure I follow this, why would you need to reimplement the same meta code?

[Adam Topaz]

I should mention that I have some meta code that does this translation (in the more general context of Lawvere theories).

[Shreyas Srinivas]

@Andrés Goens : I think what Adam is talking about is generating terms as counterexamples

[Andrés Goens]

Adam Topaz said:

The main benefit of MagmaImpl is that this captures precisely the arrows in the graph considered in this project.

wouldn't these arrows just be implication in Lean? (in the shallow embedding)

[Adam Topaz]

Yes, but you need some way to represent the type of equations.

[Andrés Goens]

Adam Topaz said:

Yes, but you need some way to represent the type of equations.

Why isn't that just Eq?

[Adam Topaz]

That's a term of Expr.

[Shreyas Srinivas]

How much work would be involved before someone who doesn't know lawvere theories can conveniently use this deep embedding. My intuition suggests very non trivial amounts

[Adam Topaz]

you don't need to know anything about Lawvere theories.

[Shreyas Srinivas]

Btw, it feels like you are expressing op semantics for rewrite rules in MagmaRel. I was discussing with someone about going in the other direction only recently. Nice coincidence

[Adam Topaz]

with some metaprogramming you wouldn't need to interface at all with this deep embedding.

[Andrés Goens]

Adam Topaz said:

That's a term of Expr.

I don't follow. Only in the same way that everything in Lean is a term of Expr, including MagmaRel

[Shreyas Srinivas]

Couldn't we instead just deep embed egg's representation of equations and egraphs in lean?

[Shreyas Srinivas]

And then outsource only the saturation part?

[Adam Topaz]

I thought that was essentially just Expr (at least if you use lean-egg)

[Shreyas Srinivas]

No what I mean is lifting the data structures of egg into lean

[Shreyas Srinivas]

Maintain the initial and final data structure in-house in lean.

[Shreyas Srinivas]

And do a shallower translation to egg

[Shreyas Srinivas]

And back

[Shreyas Srinivas]

That way we get the e-graphs representation in lean.

[Shreyas Srinivas]

Could be useful for tracing relationships between equalities and showing them in infoview

[Andrés Goens]

I don't think you need an e-graph for that necessarily, those relationships are just whether a term appears in the proof of another if I understand correctly

[Shreyas Srinivas]

Yeah but egraphs are efficient

[Shreyas Srinivas]

For queries

[Andrés Goens]

To be honest, I don't really see the issue. We could just use a regular Magma as in [Mul α], and prove things in regular Lean and use lean-egg as a tactic like you would any other, and then also use @Adam Topaz's metaprogramming to lift this to (deeply embedded) words in a formal language of magmas. Why just not do both?

[Shreyas Srinivas]

I think I still don't see how Adam's idea can encode an all encompassing structure where I can play with groups, rings, heck even derivatives (early example in Nipkow's book) and hide all the high falutin abstractions without a lot of extra work

[Shreyas Srinivas]

A slightly deeper embedding of egg seems to cover all the above

[Terence Tao]

By the way, I initially used [Mul α] (or more precisely [Add α]) to encode Magmas but then ran into weird instance diamond issues when trying to create counterexample Magmas in which I wanted to redefine the addition or multiplication law on, say, the natural numbers. This was why I eventually created a new Magma class with a new infix symbol ∘ that did not conflict with the existing + and * symbols. By doing so I forego any API that Mathlib already has for [Mul α] or [Add α], but for this project I'm not expecting much synergy with Mathlib anyway (although the API for basic number systems is useful to verify axioms for counterexamples, e.g., using ring, and simp has been working wonders also).

[Shreyas Srinivas]

So those tactics are why I think deep embeddings will be somewhat more challenging to work with. We'd have to adapt them somehow

[Kim Morrison]

(I probably won't have much time for this project, but I think it would be a very sad mistake to not pursue Adam's suggestions here!)

[Kim Morrison]

(Slightly relatedly, I would encourage you to insist that all tools, e.g. to generate the implications graph, to identify interesting unknown statements, etc, are all written in Lean, not by scraping the Lean source file as text. This will come at a slightly initial cost --- less ability to leverage contributors' existing Perl skills, etc --- but will pay off in the end.)

[Daniel Weber]

Should the equational laws be abbrevs?

[Amir Livne Bar-on]

A lot of the counter-examples use the same magmas, and in fact the same half-proofs: an example with a proof that some equation holds or not holds in it.

I think it will save work if we switch most of the "not implies" statements to listing specific magmas and laws that are satisfied or not in them. (Some would still make sense to keep this way, e.g. algebraic considerations on the number of elements)

[Terence Tao]

Yes, we may end up having a table of magma examples with a list of what equations each one satisfies and which ones they don't. In principle, if an example satisfies say 1000 laws and doesn't satisfy 4000 others that already gives four million counterexamples!

[Terence Tao]

Daniel Weber said:

Should the equational laws be abbrevs?

I think eventually the equational laws should be some specialized structure along the lines of what @Adam Topaz suggested, partly in order to help organize these laws within Lean rather than by external tools, but also so that we can prove useful metatheorems about these laws within Lean (we are slowly collecting some metatheorems over in the outstanding tasks thread).

[Adam Topaz]

I got a start implementing some meta code to convert the deep representation suggested at the top of the thread to something that's at least human readable:

import Mathlib.Tactic.ProdAssoc
import Qq.MetaM

inductive NatExpr where
  | zero
  | one
  | add : NatExpr → NatExpr → NatExpr

instance : Add NatExpr := ⟨.add⟩
instance : One NatExpr := ⟨.one⟩
instance : Zero NatExpr := ⟨.zero⟩

def NatExpr.toNat : NatExpr → Nat
  | 0 => 0
  | 1 => 1
  | a + b => a.toNat + b.toNat

inductive MagmaWord : NatExpr → NatExpr → Type where
  | id (A : NatExpr) : MagmaWord A A
  | comp {A B C : NatExpr} : MagmaWord A B → MagmaWord B C → MagmaWord A C
  | fst (X Y : NatExpr) : MagmaWord (X + Y) X
  | snd (X Y : NatExpr) : MagmaWord (X + Y) Y
  | lift {T X Y : NatExpr} :
      MagmaWord T X → MagmaWord T Y → MagmaWord T (X + Y)
  | toNil (L : NatExpr) : MagmaWord L 0
  | mul : MagmaWord (1 + 1) 1

structure MagmaRel where
  source : NatExpr
  lhs : MagmaWord source 1
  rhs : MagmaWord source 1

inductive MagmaRel.rel (R : MagmaRel) : {A B : NatExpr} → MagmaWord A B → MagmaWord A B → Prop where
  | of : R.rel R.lhs R.rhs
  | rfl {A B : NatExpr} (e : MagmaWord A B) : R.rel e e
  | symm {A B : NatExpr} {e f : MagmaWord A B} : R.rel e f → R.rel f e
  | trans {A B : NatExpr} {e f g : MagmaWord A B} : R.rel e f → R.rel f g → R.rel e g
  | id_comp {A B : NatExpr} (e : MagmaWord A B) : R.rel (MagmaWord.comp (.id _) e) e
  | comp_id {A B : NatExpr} (e : MagmaWord A B) : R.rel (MagmaWord.comp e (.id _)) e
  | assoc {A B C D : NatExpr} (e : MagmaWord A B) (f : MagmaWord B C) (g : MagmaWord C D) :
      R.rel ((e.comp f).comp g) (e.comp (f.comp g))
  | comp_congr {A B C : NatExpr} (e e' : MagmaWord A B) (f f' : MagmaWord B C) :
      R.rel e e' → R.rel f f' → R.rel (e.comp f) (e'.comp f')
  | lift_fst {T X Y : NatExpr} (e : MagmaWord T X) (f : MagmaWord T Y) :
      R.rel ((e.lift f).comp (.fst _ _)) e
  | lift_snd {T X Y : NatExpr} (e : MagmaWord T X) (f : MagmaWord T Y) :
      R.rel ((e.lift f).comp (.snd _ _)) f
  | lift_unique {T X Y : NatExpr} (e f : MagmaWord T (X + Y)) :
      R.rel (e.comp (.fst _ _)) (f.comp (.fst _ _)) →
      R.rel (e.comp (.snd _ _)) (f.comp (.snd _ _)) →
      R.rel e f
  | toNil_unique {X : NatExpr} (e f : MagmaWord X 0) : R.rel e f

structure MagmaImpl (R S : MagmaRel) where
  impl (h : ∀ {A B : NatExpr} (e f : MagmaWord A B), R.rel e f) : S.rel e f

open Lean Elab Qq

def NatExpr.elab (X : Q(Type)) : NatExpr → TermElabM Q(Type)
  | .zero => return q(Unit)
  | .one => return X
  | .add a b => do
    let a ← a.elab X
    let b ← b.elab X
    return q($a × $b)

def Nat.elab (X : Q(Type)) : Nat → TermElabM Q(Type)
  | 0 => return q(Unit)
  | 1 => return X
  | n+2 => do
    let a ← (n+1).elab X
    return q($a × $X)

def MagmaWord.elab (X : Q(Type)) (mul : Q(Mul $X)) :
    {n m : NatExpr} → MagmaWord n m → TermElabM ((S T : Q(Type)) × Q($S → $T))
  | _, _, .id _ => return ⟨q($X), q($X), q(fun x : $X => x)⟩
  | _, _, .comp f g => do
    let ⟨Sf,Tf,f⟩ ← f.elab X mul
    let ⟨Sg,Tg,g⟩ ← g.elab X mul
    let ⟨_⟩ ← assertDefEqQ (u := 1) Tf Sg
    return ⟨Sf, Tg, q(fun x => $g ($f x))⟩
  | _, _, .fst A B => do
    let A ← A.elab X
    let B ← B.elab X
    return ⟨q($A × $B), q($A), q(fun (x,_) => x)⟩
  | _, _, .snd A B => do
    let A ← A.elab X
    let B ← B.elab X
    return ⟨q($A × $B), q($B), q(fun (_,x) => x)⟩
  | _, _, .mul => return ⟨q($X × $X), X, q(fun (x, y) => x * y)⟩
  | _, _, .lift f g => do
    let ⟨Sf,Tf,f⟩ ← f.elab X mul
    let ⟨Sg,Tg,g⟩ ← g.elab X mul
    let ⟨_⟩ ← assertDefEqQ (u := 1) Sf Sg
    return ⟨Sf, q($Tf × $Tg), q(fun x => ($f x, $g x))⟩
  | _, _, .toNil A => do
    let A ← A.elab X
    return ⟨A, q(Unit), q(fun _ => ())⟩

def MagmaRel.elab (X : Q(Type)) (mul : Q(Mul $X)) (r : MagmaRel) : TermElabM Q(Prop) := do
  let s := r.source
  let arr : Array (Name × Expr) := Array.range s.toNat |>.map fun n => (s!"x_{n}".toName, X)
  Meta.withLocalDeclsD (arr.map fun (n,x) => (n, fun _ => return x)) fun fvars => do
    let ⟨lS, lT, lhs⟩ ← r.lhs.elab X mul
    let ⟨rS, rT, rhs⟩ ← r.rhs.elab X mul
    let A ← s.elab X
    let B ← s.toNat.elab X
    let f : Q($B → $A) ← Lean.Expr.mkProdFun B A
    let tail := fvars[1:]
    let x : Q($B) ← show TermElabM Expr from do
      let mut out := fvars[0]!
      for t in tail do
        out ← Meta.mkAppM `Prod.mk #[out, t]
      return out
    let ⟨_⟩ ← assertDefEqQ (u := 1) lS A
    let ⟨_⟩ ← assertDefEqQ (u := 1) rS A
    let ⟨_⟩ ← assertDefEqQ (u := 1) lT X
    let ⟨_⟩ ← assertDefEqQ (u := 1) rT X
    let lhs : Q($X) := q($lhs ($f $x))
    let rhs : Q($X) := q($rhs ($f $x))
    let out : Q(Prop) ← Meta.mkForallFVars fvars q($lhs = $rhs)
    return out

elab "[impl|" r:term "," s:term "]" : term => do
  let r : MagmaRel ← unsafe Term.evalTerm MagmaRel q(MagmaRel) r
  let s : MagmaRel ← unsafe Term.evalTerm MagmaRel q(MagmaRel) s
  Meta.withLocalDecls #[(`X,.default,fun _ => return q(Type)), (.anonymous, .instImplicit, fun fvars => do
    let X : Q(Type) := fvars[0]!
    return q(Mul $X)
  )] fun fvars => do
    let some (X : Q(Type)) := fvars[0]? | throwError "Unknown error"
    let some (inst : Q(Mul $X)) := fvars[1]? | throwError "Unknown error"
    let rprop ← r.elab X inst
    let sprop ← s.elab X inst
    let out : Q(Prop) ← Meta.mkForallFVars fvars q($rprop → $sprop)
    return out

def allEq : MagmaRel := MagmaRel.mk (1+1) (.fst _ _) (.snd _ _)
def abel : MagmaRel := MagmaRel.mk (1+1) .mul (MagmaWord.lift (.snd _ _) (.fst _ _) |>.comp .mul)
def assoc : MagmaRel := MagmaRel.mk ((1 + 1) + 1)
  (MagmaWord.lift (MagmaWord.fst _ _ |>.comp .mul) (.snd _ _) |>.comp .mul)
  (MagmaWord.lift (MagmaWord.fst _ _ |>.comp (MagmaWord.fst _ _)) (MagmaWord.comp (.lift (MagmaWord.fst _ _ |>.comp <| .snd _ _) (.snd _ _)) MagmaWord.mul) |>.comp .mul)

example : [impl| allEq , assoc] := by
  dsimp only

See the example at the bottom, after the dsimp only. (BTW, I couldn't figure out how to apply dsimp only directly to the term in the elaborator. Does anyone know how to do that in the TermElabM monad?)
(edit: bug fixed in the code)

[David Renshaw]

Kim Morrison said:

(Slightly relatedly, I would encourage you to insist that all tools, e.g. to generate the implications graph, to identify interesting unknown statements, etc, are all written in Lean, not by scraping the Lean source file as text. This will come at a slightly initial cost --- less ability to leverage contributors' existing Perl skills, etc --- but will pay off in the end.)

A step in this direction:
https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Lean.20script.20for.20extracting.20current.20set.20of.20implications/near/473150651

[Amir Livne Bar-on]

Since this is a finite project, it might be easier to just generate the proofs of all x=f(y, z, ...) => x = y and of x ∘ y = f(z, w, ...) => x ∘ y = z ∘ w etc.

Is there an interest in doing this? It's a relatively small number of proofs (I have 900 in mind, we might find some more forms) and might help preventing people from wasting time on these laws.

Fwiw it was an easy script, if there are no objections in the next few hours I'll open a PR.

[Terence Tao]

I've opened an issue #36 [EDIT: I meant https://github.com/teorth/equational_theories/issues/36] to create these syntactic objects, as this will allow us to prove metatheorems about equational laws in Lean. Though for now the more low-tech approach of proving the finite number of instances of the metatheorems that we need will suffice.

[Daniel Weber]

This points to Mathlib. Perhaps one of the moderators could make equational#36 work?

[Bryan Gin-ge Chen]

This should work from now on: equational#36

[Cody Roux]

Obivously, this would work: https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Syntax.html#FirstOrder.Language.BoundedFormula but maybe it creates more pain than it alleviates. @Floris van Doorn ?

[Terence Tao]

There is now a PR (not by myself) getting started in this direction: equational#96

[Floris van Doorn]

Yes, you can use first-order logic to encode all the terms, of course. The language we are considering is so simple that you might not gain too much from it over doing it from scratch, though.

[Terence Tao]

I have merged @Franklin Pezzuti Dyer 's FreeMagma code to the repository, see https://github.com/teorth/equational_theories/blob/main/equational_theories/FreeMagma.lean. I am thinking that for our purposes we could encode a syntactic equation (let's call it SynEquation for now, but I'm open to better names [EDIT: actually I propose Law]) as simply an element E of FreeMagma ℕ × FreeMagma ℕ (i.e. two finite words over the natural numbers), and then say that a magma G models E, i.e., G ⊧ E, if for every assignment of elements of the magma to the natural numbers, the two words agree: ∀ f : ℕ → G, evalInMagma f E.1 = evalInMagma f E.2. There is some obvious API here to show that this operation is invariant under relabeling, symmetry, and duality (reversing the order of the magma and in the syntactic equation). Then we should be able to equip the class SynEquation with a preorder: E ≤ E' being something like ∀ (G: Type*) (hG: Magma G) : G ⊧ E → G ⊧ E' (though there may be some universe issues quantifying over G). One should then be able to start proving the metatheorems that I have started collecting at https://teorth.github.io/equational_theories/blueprint/sect0002.html , after one figures out how to pass back and forth between these syntactic equations, and the semantic equations that we are currently using in the repo.

How does this general approach sound? If it makes sense, I can start adding a chapter to the repository on syntactic equations that lists out the basic API that needs to be formalized. There may be some completeness and compactness theorems to establish as well, but this should be a lot easier than the general first-order logic version.

It's also possible that we could borrow from some existing Mathlib work in this area. I had avoided using Add or Mul for Magmas due to a desire to avoid the impression that magmas were likely to be associative or commutative, but perhaps the API there is sufficiently good that some way to equate magmas with say a Mul structure would be helpful? I also have no idea if the existing model theory support in Mathlib is good enough that it would also be worth tapping.

[Daniel Weber]

Regarding the universe problem - we can simply use ∀ (G: Type) (hG: Magma G) : G ⊧ E → G ⊧ E' and prove this implies ∀ (G: Type u) (hG: Magma G) : G ⊧ E → G ⊧ E' for any u, although that might require some effort, I'm not sure how hard the Löwenheim–Skolem theorem is to prove for this case

[Cody Roux]

I'll try to pencil something out; it shouldn't need all that choice machinery I think, since we're in happy Harrop formulae land over a countable language.

[Cody Roux]

Though I now remember that every equational theory has at least 1 finite model :)

[Cody Roux]

Created https://github.com/teorth/equational_theories/issues/104 hope that's not out of line, it's contingent on https://github.com/teorth/equational_theories/issues/36 but that should be closed soon.

I'm blanking on how to get compactness; I think one can take the limits of all the congruences induced on the free model by finite sub-models.

[Shreyas Srinivas]

It might help to add a full description in the issue

[Shreyas Srinivas]

Basically once an issue is added to the task list, it is easy to forget what the issue was created for and then we have to search zuli

[Shreyas Srinivas]

*zulip

[Cody Roux]

Done, please tell me if it needs more detail: https://github.com/teorth/equational_theories/issues/104

[Shreyas Srinivas]

Thanks. I got it added to the task list

[Shreyas Srinivas]

The claim + PR process will now work automatically

[Shreyas Srinivas]

Technically it can work without this step except being on the project dashboard

[Shreyas Srinivas]

But then if we coordinate on the dashboard, people might not find it unless the issue is on the dashboard

[Cody Roux]

I'll keep going here to avoid creating a new "completeness" thread; does anyone know if using Quotient over Quot is preferable? I seem to recall some discussion on the FRO that suggested otherwise.

[Edward van de Meent]

i think that you're likely to find more API available when using Quotient?

[Cody Roux]

I'll start with quotient and advise if I run into trouble

[Adam Topaz]

If you have a setoid, then you should absolutely use Quotient.

[Cody Roux]

Ok does anyone know how to make a Quotient.lift_2 "commute" with it's arguments? I'm almost there!

[Adam Topaz]

I’m not sure what do you mean?

[Cody Roux]

I need to rewrite Quotient.lift_2 f x y to something like f ? ?, but can't find the rule in the lib...

[Adam Topaz]

That’s true by rfl assuming x and y are of the form Quotient.mk …

[Cody Roux]

oooo

[Adam Topaz]

And simp would probably solve such a goal as well

[Adam Topaz]

If x and y are just terms of the quotient, you can use rcases x to replace it with a Quotient.mk …

[Cody Roux]

This is great, I have to apply the IH which is why things were stuck, thanks a bunch!

[Cody Roux]

Woo finally done! That was tough, had to use a smidge of choice, sadly

[Amir Livne Bar-on]

When formatting the output in analysis scripts and in visualizations, it would be nice to name some of the laws, and also sometimes to manually select a representative from some equivalence classes (e.g. showing 46 rather than 41 as the canonical member). Is it something that's possible to add using a decorator? Does it make sense to put these in AllEquations.lean?

[Daniel Weber]

That could be added to the equational_result attribute

[Amir Livne Bar-on]

That's for edges though? I'm looking to tag nodes

[Cody Roux]

We've proven 3.8! @Floris van Doorn is responsible for stating and proving the crucial lemmas. We change the proof slightly to work with multisets instead of "linear ℝ-forms" which, if they exist in Mathlib, are likely harder to work with.

[Cody Roux]

https://github.com/teorth/equational_theories/pull/177