Adding the egg repository as a dependency

Stream: Equational

[Shreyas Srinivas]

I am working on a PR to add the egg repository to the main repo if this is welcome

[Terence Tao]

OK but I may switch to a new repository soon, I am trying to set up a blueprint CI using @Pietro Monticone 's instructions and the instructions require creating a new repo rather than developing an existing one

[Shreyas Srinivas]

I think it is one step

[Shreyas Srinivas]

using this repo : https://github.com/pitmonticone/LeanProject as a template

[Shreyas Srinivas]

It might make more sense for me to make the PR to the new repo

[Shreyas Srinivas]

Using the "use this template" button Screenshot from 2024-09-26 17-53-49.png

[Terence Tao]

Yes I have done that and am currently running the leanblueprint new script. It is downloading Mathlib I think right now.

image.png

[Shreyas Srinivas]

ah right. Once your new repository is up, I can also add the gitpod config to make contributing simpler

[Terence Tao]

OK I completed the setup at https://github.com/teorth/equational_theories . Will move the files over now.

[Shreyas Srinivas]

The first PR is in

[Shreyas Srinivas]

I'll add a few commits and confirm that it can be merged in a moment

[Shreyas Srinivas]

@Terence Tao : sorry there was a one character typo. Another PR coming in to fix it

[Shreyas Srinivas]

Ready

[Shreyas Srinivas]

I can confirm that gitpod works with PR 2

[Shreyas Srinivas]

PR no. 3 adds egg as a dependency: https://github.com/teorth/equational_theories/pull/3

[Shreyas Srinivas]

It builds sucessfully after a lake update

[Shreyas Srinivas]

Both PRs 2 and 3 are ready for merge

[Marcus Rossel]

Hey, I maintain the egg tactic together with @Andrés Goens. I'm looking into trying out the tactic on some of the theorems. My hope is that we can solve theorems by just egg [*]. For example, the following works:

/-- This proof is from https://mathoverflow.net/a/450905/766 -/
theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) : Equation43 G := by
  egg [*]

A major caveat to this approach is that equality saturation cannot handle equations where the quantified variables do not satisfy the subset relation in either direction of the equality. So an equation like Equation2 (∀ x y : G, x = y) cannot be used for rewriting. We might be able to partially brute force our way out of that problem though by instantiating such quantified variables with terms from the local context.

[Andrés Goens]

or alternatively, using egg calc which implements the guided equality saturation idea: essentially tring to replicate an "informal computation" from a blackboard

[Daniel Weber]

Using lake exe extract_implications causes egg/egg_for_lean.static to run

[Andrés Goens]

that's weird, I wonder if it's picking it up from that compile_time_search_path%? Doesn't sound like it should

unsafe def main (_args : List String) : IO Unit := do
  let module := `equational_theories.Subgraph
  searchPathRef.set compile_time_search_path%

  let output : Output ← withImportModules #[{module}] {} (trustLevel := 1024) fun env =>

[Daniel Weber]

It also happened when I attempted to create a new lean_exe

[Andrés Goens]

Hm, maybe lake links all dependencies statically? I'm out of my depth here

[Andrés Goens]

@Daniel Weber what happens exactly (how do you see it)? when I run lake exe extract_implications it seems to just work

[Andrés Goens]

oh, nvm I see what you say, the first line is

ℹ [39/44] Ran egg/egg_for_lean.static

[Daniel Weber]

Yes, and earlier I didn't have rust installed so it just gave an error and didn't work (now I installed it)

[Andrés Goens]

I tried an empty script that does nothing and it happens there too, I guess it's lake because it's declared as a dependency that treats it like a global dependency for executables

[Andrés Goens]

not sure if there's a way to make it only a dependency of the lib

[Joachim Breitner]

Should we remove the egg dependency from the lakefile until it is actually used?

[Andrés Goens]

Marcus Rossel said:

Hey, I maintain the egg tactic together with Andrés Goens. I'm looking into trying out the tactic on some of the theorems. My hope is that we can solve theorems by just egg [*]. For example, the following works:

/-- This proof is from https://mathoverflow.net/a/450905/766 -/
theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) : Equation43 G := by
  egg [*]

A major caveat to this approach is that equality saturation cannot handle equations where the quantified variables do not satisfy the subset relation in either direction of the equality. So an equation like Equation2 (∀ x y : G, x = y) cannot be used for rewriting. We might be able to partially brute force our way out of that problem though by instantiating such quantified variables with terms from the local context.

we started trying this out (and by we, I mean @Marcus Rossel fixed things and I've just played around with it a bit now)

It looks relatively promising: It seems we can prove a bunch of implications that are not in Subgraph.lean (and we can't prove a few that are), with a timeout of 1s. Here's a diff for the implications that extract_implications gives (computing the transitive closure):

implications diff

equational_theories git:(eggxplosion) diff implications_egg_sorted.txt implications_subgraph_sorted.txt
1,2d0
< Equation14 → Equation1
< Equation14 → Equation23
4,9c2,25
< Equation14 → Equation8
< Equation1689 → Equation1
< Equation168 → Equation1
< Equation23 → Equation1
< Equation28393 → Equation1
< Equation29 → Equation1
---
> Equation1689 → Equation168
> Equation1689 → Equation2
> Equation1689 → Equation23
> Equation1689 → Equation3
> Equation1689 → Equation38
> Equation1689 → Equation387
> Equation1689 → Equation39
> Equation1689 → Equation4
> Equation1689 → Equation40
> Equation1689 → Equation41
> Equation1689 → Equation42
> Equation1689 → Equation43
> Equation1689 → Equation45
> Equation1689 → Equation4512
> Equation1689 → Equation4513
> Equation1689 → Equation4522
> Equation1689 → Equation4564
> Equation1689 → Equation4579
> Equation1689 → Equation4582
> Equation1689 → Equation46
> Equation1689 → Equation5
> Equation1689 → Equation6
> Equation1689 → Equation7
> Equation1689 → Equation8
11,14d26
< Equation29 → Equation23
< Equation29 → Equation8
< Equation2 → Equation1
< Equation2 → Equation14
16d27
< Equation2 → Equation1689
18,19d28
< Equation2 → Equation28393
< Equation2 → Equation29
21,23d29
< Equation2 → Equation3722
< Equation2 → Equation3744
< Equation2 → Equation374794
25d30
< Equation2 → Equation381
42d46
< Equation2 → Equation5105
46,47d49
< Equation3722 → Equation1
< Equation3744 → Equation1
50,53d51
< Equation3744 → Equation4512
< Equation374794 → Equation1
< Equation381 → Equation1
< Equation387 → Equation1
55d52
< Equation38 → Equation1
57,58d53
< Equation39 → Equation1
< Equation39 → Equation381
60d54
< Equation3 → Equation1
62d55
< Equation3 → Equation3722
64,67d56
< Equation40 → Equation1
< Equation41 → Equation1
< Equation41 → Equation3722
< Equation41 → Equation3744
69d57
< Equation41 → Equation381
83d70
< Equation42 → Equation1
85,87d71
< Equation43 → Equation1
< Equation4512 → Equation1
< Equation4513 → Equation1
89d72
< Equation4522 → Equation1
92,97d74
< Equation4564 → Equation1
< Equation4564 → Equation4512
< Equation4579 → Equation1
< Equation4579 → Equation4512
< Equation4579 → Equation4564
< Equation4582 → Equation1
103,104d79
< Equation45 → Equation1
< Equation45 → Equation381
106,108d80
< Equation46 → Equation1
< Equation46 → Equation3722
< Equation46 → Equation3744
110d81
< Equation46 → Equation381
124d94
< Equation4 → Equation1
126d95
< Equation4 → Equation28393
128,129d96
< Equation4 → Equation3722
< Equation4 → Equation3744
131d97
< Equation4 → Equation381
137,138d102
< Equation5105 → Equation1
< Equation5 → Equation1
141,143d104
< Equation5 → Equation3722
< Equation5 → Equation3744
< Equation5 → Equation381
147,148d107
< Equation5 → Equation4564
< Equation5 → Equation4579
150,151d108
< Equation6 → Equation1
< Equation6 → Equation14
153d109
< Equation6 → Equation1689
156,157d111
< Equation6 → Equation28393
< Equation6 → Equation29
159,161d112
< Equation6 → Equation3722
< Equation6 → Equation3744
< Equation6 → Equation374794
163d113
< Equation6 → Equation381
180d129
< Equation6 → Equation5105
183,184d131
< Equation7 → Equation1
< Equation7 → Equation14
186d132
< Equation7 → Equation1689
189,190d134
< Equation7 → Equation28393
< Equation7 → Equation29
192,194d135
< Equation7 → Equation3722
< Equation7 → Equation3744
< Equation7 → Equation374794
196d136
< Equation7 → Equation381
213d152
< Equation7 → Equation5105
216d154

It seems like we can't handle equation 1689 well, the one from the paper of Kisielewicz. I'll play around with it a a bit, but ofc the point is also that some ingenuity is required for these implications, so it's maybe not as suprising. The cool thing is we have a bunch of equations that are new! I have added them in a PR draft here for now: equational#200

The issue remains with the rust requirement creeping into the script, so not sure if we want to merge it like it is (although it's a shame since the proofs are a one-liner with the egg tactic). I can just take out the proofs (e.g. just use by? and copy the term or something, or maybe using @Joachim Breitner 's calcify tactic, I quite like that one for these kind of things). Would that be welcome (a PR with just the new subgraph proofs)?

I think @Marcus Rossel is also playing around with the tactic a bit more so maybe we'll get nicer results on AllEquations :)

[Andrés Goens]

(it seems it's 86 new implications in the transitive closure over what is currently in Supgraph.lean)

[Joachim Breitner]

Does calcify produce good results from egg proofs? That might a nice and pretty option!

[Joachim Breitner]

Would that be welcome (a PR with just the new subgraph proofs)?

Certainly, I think; why not (if the proofs are somewhat reasonable, i.e. not a 1MB dump of the raw proof term :-)

[Joachim Breitner]

I am wary of making a working local rust toolchain a requirement for people to work on this project. Not sure what to do about this.

[Daniel Weber]

How hard would it be to modify egg such that it only builds itself if the tactic is executed?

[Andrés Goens]

yeah, when the proof terms are reasonably small, calcify results are nice (sometimes egg finds unnecessarily long proof terms though), but I'd shorten that manually for a PR :sweat_smile:

[Andrés Goens]

Daniel Weber said:

How hard would it be to modify egg such that it only builds itself if the tactic is executed?

that's more of a lake than an egg issue if I'm not mistaken

[Andrés Goens]

it's already like that for libraries, but for am executable (in particular the extract _implications script) it doesn't

[Marcus Rossel]

Andrés Goens said:

It seems like we can't handle equation 1689 well, the one from the paper of Kisielewicz.

The corresponding theorem can be solved by:

theorem Equation1689_implies_Equation2 (G: Type*) [Magma G] (h: Equation1689 G) : Equation2 G:= by
  have : ∀ a b c : G, a ∘ (b ∘ ((b ∘ c) ∘ c)) = (a ∘ b) ∘ b := by egg [*, h _ (_ ∘ _) _; h]
  egg [*]

(Which then also means that we don't need all of the preceding lemmas)

[Andrés Goens]

Marcus Rossel said:

Andrés Goens said:

It seems like we can't handle equation 1689 well, the one from the paper of Kisielewicz.

That can be solved by

theorem Equation1689_implies_Equation2 (G: Type*) [Magma G] (h: Equation1689 G) : Equation2 G:= by
  have : ∀ a b c : G, a ∘ (b ∘ ((b ∘ c) ∘ c)) = (a ∘ b) ∘ b := by egg [*, h _ (_ ∘ _) _; h]
  egg [*]

probably the timeout of 1s was not enough then on my potato

[Terence Tao]

By the way, is there already a file listing all the known and open implications for the subgraph? It would be nice to list that on the front page of the project (under "statistics and data files from a given point in time").

[Terence Tao]

If dependency and compile time is an issue, one could generate two output files, one a list of lean proofs using the egg dependency, and one just a list of conjectures for the same implications with no egg dependency.

[Andrés Goens]

I started going through the new implications that we found this way, here's some results so far:

• a few of the equations were redundant even though I computed the (alphabetically sorted) diff of the transitive closure generated from extract_implications, for example a bunch of them were just that some equations imply Equation1 which is a tautology. I imagine the extract_implications script is not picking up some of these
• some implications are new and interesting! The proofs that we find with our tactic are also mostly quite small and calcify seems to work well in a lot of them (although one I was getting a pretty nasty term and by manually looking at it, it was easy to express it as a simple rw). It's not straightforward to go through them, so I'll start doing that slowly, sounds like a good way to get some more intuition myself, I don't want to just let automated tools have all the fun!
• I've made a PR (equational#207) with the first three non-trivial equations that I got this way, it's quite late over here so I might not do much more of that today

[Marcus Rossel]

@Andrés Goens you can get calcify's suggestion using egg? now.

[Andrés Goens]

nice!

[Andrés Goens]

Marcus Rossel said:

Andrés Goens you can get calcify's suggestion using egg? now.

hm, I get error loading library, libCalcify-Basic-1.so: cannot open shared object file: No such file or directory (even if I just try it out on the lean-egg repo standalone)

[Andrés Goens]

(ok nvm, just a clean build works)

[Joachim Breitner]

I'd be interested in examples where you expect calcify to do better! Maybe file issues if you don't mind

[Marcus Rossel]

Joachim Breitner said:

I'd be interested in examples where you expect calcify to do better! Maybe file issues if you don't mind

I think right now it'll be difficult to find examples of that, because the problem is firmly on the side of egg's proof generation. But there are plans to improve that in the future and then we might find some work for you :wink:

[Andrés Goens]

yeah I did think it might be the proof terms that are a bit janky, but I wonder how much more could calcify do. In particular, I'm not sure if using rw to justify steps would be in scope of it (would def. work great with egg proofs which are all about rws), but kind of an inverse of rw sounds pretty non-trivial

[Joachim Breitner]

calcify does clean up the mess that simp does, so maybe it could clean after egg as well (but I haven't looked at the proof terms, so I shouldn't be too bold).

A rwify tactic might also be useful if you are looking for smaller proofs.

[Andrés Goens]

the mess that egg does is inspired by simps :)

[Joachim Breitner]

Ah, and yes, calcify could certainly try to use more concise proofs at each step. That wasn't a focus so far.

[Andrés Goens]

so in principle it should be similar

[Andrés Goens]

doesn't hurt to add the issues and if it turns out they're out of scope/too messy, you can just close them

[Marcus Rossel]

To be more precise, our proof gen is pretty much just mathlib's congruence quotations glued together with transitivity. We need that (I think) because we support rewriting under binders. Is calcify supposed to support that?

[Andrés Goens]

Andrés Goens said:

• I've made a PR (equational#207) with the first three non-trivial equations that I got this way, it's quite late over here so I might not do much more of that today

the rest of these (non-trivial, new) equations for Subgraph.lean are now in a PR: equational#232

I used calcify and manually cleaned up a bit more, but calcify already produces pretty nice proofs for a lot of the cases! (and eliminates the need for a rust toolchain installed for others) there are some interesting examples it found, I was expecting the proofs to be a lot larger, but I guess for these simple examples Flatt et al's algorithm works quite well!