Automatically generating magma laws & proofs from equations

Stream: Equational

[Anand Rao Tadipatri]

Proving some of the non-implications using metatheorems requires operating on the law associated with an equation (as defined in Chapter 1 of the blueprint) and showing that a proof for the law holds for the corresponding equation.

In this (in-progress) PR, I've modified the equation command to

• automatically create a corresponding MagmaLaw and add it to the environment
• automatically generate a proof that a magma G satisfies the law iff the equation is true in the magma

For example, typing in

equation 27 := x = (x ◇ y) ◇ z

now automatically generates the declarations

#print Law27
/- @[reducible] def Law27 : Law.MagmaLaw (Fin 3) :=
Lf 0 ≃ Lf 0 ⋆ Lf 1 ⋆ Lf 2 -/

#print Law27.models_iff
/- @[reducible] def Law27.models_iff : ∀ (G : Type) [inst : Magma G], satisfies G Law27 ↔ Equation27 G :=
models_iff_3 Law27 -/

@Hernan Ibarra and I plan to build on top of this framework and prove some non-implications in the graph using the invariant based metatheorems described in Chapter 8 of the blueprint.

This code may be independently useful to others proving implications or non-implications from the laws.

[Anand Rao Tadipatri]

I just noticed an open PR (#322) that seems to do something similar. I'm sorry for the overlap, I didn't notice this when I started working on my code.

Update: I also noticed that PR #357 by @Andrés Goens also does something similar -- I apologize for the overlap here too and I'd be happy to collaborate on merging the features into a single PR.

[Andrés Goens]

@Anand Rao Tadipatri it's nice that we're at least converging towards the same goal! (it looks like equational#357 and your code for that are very similar, for example). Maybe as a heads-up for the future: can you try and use the claim mechanism (see contributing.md), so that this overlap doesn't happen? I did equational#357 because the issue (equational#143) was not claimed in https://github.com/users/teorth/projects/1 , if you claim it others will know you're working on it and not duplicate the effort

[Andrés Goens]

Happy to collaborate on making things consistent! I'm not sure we want to have all of it in a single PR since it's much harder to review/read, but maybe we can split it up in different PRs?

[Andrés Goens]

I think for the automatic generation of Laws we should for example agree on over which alphabet. In equational#357 I use Nat whereas in equational#356 you seem to be using Fin n (I think that's the main difference). I see that Fin n has the advantage of being minimal, but I worry it'll just make things harder to compose the proofs then, since we'll have to cast from Fin n to Fin m if the number of variables disagree, so I thought it was easier just to state everything over FreeMagma Nat

[Andrés Goens]

(We should ping @Daniel Weber as well, who claimed equational#147 and is working on it on equational#322)

[Anand Rao Tadipatri]

@Andrés Goens Thanks for the message. When I started working on this, it was as a part of the broader goal of implementing the metatheorem and I didn't think to check the issue tracker. I'll make sure to do that the next time I start working on a broader subtask to avoid similar overlaps.

[Anand Rao Tadipatri]

@Andrés Goens Thanks for the message. When I started working on this, it was as a part of the broader goal of implementing the metatheorem and I didn't think to check the issue tracker. I'll make sure to do that the next time I start working on a broader subtask to avoid similar overlaps.

[Anand Rao Tadipatri]

The way I currently generate equivalence proofs like

@[reducible] def Law27.models_iff : ∀ (G : Type) [inst : Magma G], satisfies G Law27 ↔ Equation27 G :=
models_iff_3 Law27

relies on the number of variables to call the appropriate lemma, so I would prefer to keep Fin n.

However, I agree that it would be a nuisance to cast around equations with different numbers of variables. I was thinking this could be dealt with some API that transports a MagmaLaw A to a MagmaLaw B along a function f : A -> B together with a function that takes in a MagmaLaw (Fin n) and a MagmaLaw (Fin m) and gives MagmaLaw (Fin (max m n)) x MagmaLaw (Fin (max m n)).

[Anand Rao Tadipatri]

The way I currently generate equivalence proofs like

@[reducible] def Law27.models_iff : ∀ (G : Type) [inst : Magma G], satisfies G Law27 ↔ Equation27 G :=
models_iff_3 Law27

relies on the number of variables to call the appropriate lemma, so I would prefer to keep Fin n.

However, I agree that it would be a nuisance to cast around equations with different numbers of variables. I was thinking this could be dealt with some API that transports a MagmaLaw A to a MagmaLaw B along a function f : A -> B together with a function that takes in a MagmaLaw (Fin n) and a MagmaLaw (Fin m) and gives MagmaLaw (Fin (max m n)) x MagmaLaw (Fin (max m n)).

[Andrés Goens]

FWIW, this "just works" with my version in equational#357 (over Nat) and @Daniel Weber 's tactics:

theorem Law2_leq_Law3 : Law2 ≤ Law3 := by
  intro G _ h
  equation_to_law
  apply Equation2_implies_Equation3 G
  law_to_equation
  apply h

and that proof doesn't rely on the number of specific variables (although it just goes in the one direction, the other should also be simple too)

[Andrés Goens]

I'll have a look at how your PR needs the Fin n, I wonder if we could generate these proofs by keeping track of the number in the meta code but still produce them over Nat?

[Andrés Goens]

ohh, I see, you explicitly proved stuff for Fin 1 up to Fin 6 :grinning:

[Andrés Goens]

I wonder if we can have it both ways, proving that an implication ov FreeMagma Nat implies it over FreeMagma (Fin n)

[Andrés Goens]

I'll give that a try a bit later

[Anand Rao Tadipatri]

I see, that's quite neat.

[Anand Rao Tadipatri]

Andrés Goens said:

ohh, I see, you explicitly proved stuff for Fin 1 up to Fin 6 :grinning:

Yes, it's not the most principled approach :smiley:, but since we're interested in only a specific subset of equations anyway, I thought this wouldn't be too bad a way to generate those lemmas.

[Andrés Goens]

yeah, absolutely, I think it's a clever solution

[Shreyas Srinivas]

Btw, since the claims process came up, it is important to know that if you make a PR without following the claims process, it won't appear on the task board and this means it likely doesn't get seen. From the maintainers side, the claims process not only makes the contribution process fair, but also makes our job simpler.

[Shreyas Srinivas]

Also, I question the need for any of the changes in MagmaLaw.lean

[Shreyas Srinivas]

These are cosmetic name changes and replace defs with abbrevs

[Shreyas Srinivas]

These are fairly upstream files and might cause a lot of merge conflicts for downstream contributors, so such name changes should have a very good justification. Also changing all defs to reducible is not a good idea.

[Andrés Goens]

I proved the equivalence of implications over Fin n and Nat, except for n = 0, I think that maybe holds vacuously but I wasn't sure how to construct the empty function over an uninhabited type (Fin 0 is uninhabited, right?) not sure that this even works in type theory. While I'm curious about that, I think the case n = 0 is not very interesting for us and that should be able to get us to use both approaches

[Andrés Goens]

it's in equational#368

[Anand Rao Tadipatri]

Shreyas Srinivas said:

Btw, since the claims process came up, it is important to know that if you make a PR without following the claims process, it won't appear on the task board and this means it likely doesn't get seen. From the maintainers side, the claims process not only makes the contribution process fair, but also makes our job simpler.

Thanks, that sounds reasonable to me.

[Andrés Goens]

@Anand Rao Tadipatri maybe we can merge this and then merge/rebase you PR on that. That way we can use your proof generation mera code and generate proofs over fin which we can also in meta code lift to nat using equational#368?

[Anand Rao Tadipatri]

Shreyas Srinivas said:

These are cosmetic name changes and replace defs with abbrevs

I agree, the abbrevs can be turned back to defs. The change from evalInMagma to evalHom was to use homomorphisms instead of the underlying functions.

[Anand Rao Tadipatri]

Andrés Goens said:

I proved the equivalence of implications over Fin n and Nat, except for n = 0, I think that maybe holds vacuously but I wasn't sure how to construct the empty function over an uninhabited type (Fin 0 is uninhabited, right?) not sure that this even works in type theory. While I'm curious about that, I think the case n = 0 is not very interesting for us and that should be able to get us to use both approaches

Thank you! The map from Fin 0 is called docs#Fin.elim0.

[Shreyas Srinivas]

I don't think homomorphisms are even defined that far up in the file tree

[Shreyas Srinivas]

Also, this is just a name change

[Shreyas Srinivas]

Basically it triggers too many downstream changes. At least, refactors should not be mixed with feature PRs. The way to do that is to propose a separate task and claim it, and then before merging, check how other PRs are affected.

[Anand Rao Tadipatri]

Andrés Goens said:

Anand Rao Tadipatri maybe we can merge this and then merge/rebase you PR on that. That way we can use your proof generation mera code and generate proofs over fin which we can also in meta code lift to nat using equational#368?

That sounds good to me!

[Shreyas Srinivas]

One extra consideration in this project compared to normal lean projects is how should the automatic proof scripts be updated and lemmas regenerated

[Shreyas Srinivas]

I would advise against such refactors

[Anand Rao Tadipatri]

Shreyas Srinivas said:

Basically it triggers too many downstream changes. At least, refactors should not be mixed with feature PRs. The way to do that is to propose a separate task and claim it, and then before merging, check how other PRs are affected.

That sounds reasonable. The evalHom function was already defined in an earlier file, and I was using it in place of evalInMagma, which is its underlying function.

[Shreyas Srinivas]

Yeah but I'd suggest switching back the theory files to evalInMagma and keeping defs as they are, not abbrevs

[Shreyas Srinivas]

At least in this PR. Further if there are parts of your PR not overlapping with @Andrés Goens, I suggest requesting a task (for example posting an issue and linking it in zulip) that only covers those parts. After discussion, one of the maintainers can make it a project task that you can then claim. Our current model is that the claimer's proposed PR closes issues.

[Shreyas Srinivas]

I know this might all sound bureaucratic, but it just makes the outstanding tasks process of PFR simpler all around as long as we all stick to it, and ensures that every contribution is considered properly.

[Anand Rao Tadipatri]

Thanks, I'll do that. I appreciate the effort of the maintainers in making the contribution process smooth and streamlined!

[Andrés Goens]

@Anand Rao Tadipatri what's the current plan on equational#356? It would be nice to have the proofs of equivalence of laws and equations, which would allow us to use duality to prove some of the missing implications. Would it make sense to split that and do a PR just introducing these proofs of equivalence first?

[Anand Rao Tadipatri]

Okay, that sounds good to me. I'm currently working on creating an environment extension that stores all the laws created, I'll update the PR or open a new one once I've done that.

[Daniel Weber]

@Anand Rao Tadipatri said:

Okay, that sounds good to me. I'm currently working on creating an environment extension that stores all the laws created, I'll update the PR or open a new one once I've done that.

Do you want to claim equational#142? I haven't started to work on it yet, I can disclaim it

[Anand Rao Tadipatri]

I'm not operating on the syntax of the equations in this PR, so I'd be fine if you went ahead and worked on it. I don't mind picking it up later though, once I've properly generated some of the invariants-related conjectures.

[Anand Rao Tadipatri]

@Andrés Goens Is it fine if my PR generates the laws over Fin n and we use the machinery of equational#368 to then cast to equations over Nat?

[Andrés Goens]

I guess the idea is that this would literally just be outputing the enviroment extension you're generating into a string, right?

[Andrés Goens]

Anand Rao Tadipatri said:

Andrés Goens Is it fine if my PR generates the laws over Fin n and we use the machinery of equational#368 to then cast to equations over Nat?

absolutely, I thought that was the idea! (wouldn't be sure how else you'd do it)

[Anand Rao Tadipatri]

Okay, that's what I understood too, but I just wanted to make sure before going ahead :)

[Anand Rao Tadipatri]

Andrés Goens said:

I guess the idea is that this would literally just be outputing the enviroment extension you're generating into a string, right?

Oh, I see. Yes, I think I understand now. I was planning to store the laws and not the equations, so do you reckon that an output like [0 1] = [1 0] would be reasonable? (instead of x * y = y * x) If not, I can try to configure the extension to also keep track of the original equations with the variable names while printing.

[Anand Rao Tadipatri]

I could first create a PR without the printing feature and follow up with another one that addresses equational#142, just to keep things separate and self-contained.

[Andrés Goens]

Anand Rao Tadipatri said:

I could first create a PR without the printing feature and follow up with another one that addresses equational#142, just to keep things separate and self-contained.

sounds reasonable to me!

[Anand Rao Tadipatri]

@Andrés Goens I've generalized your result for casting laws from Fin n to Nat to omit the n != 0 hypothesis. My PR for automatically adding the satisfiability equivalence proofs is at equational#427.

[Anand Rao Tadipatri]

@Daniel Weber I'd be happy to now claim equational#142 to add the export feature.

[Daniel Weber]

Alright, I disclaimed it

[Andrés Goens]

Anand Rao Tadipatri said:

Andrés Goens I've generalized your result for casting laws from Fin n to Nat to omit the n != 0 hypothesis. My PR for automatically adding the satisfiability equivalence proofs is at equational#427.

nice, thanks!

[Anand Rao Tadipatri]

I'm not sure where to post this, but I seem to be facing some strange build error with one of the generated files:

✖ [3337/3343] Building equational_theories.Generated.EquationSearch.theorems.Run5
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/checkdecls/.lake/build/lib:././.lake/packages/MD4Lean/.lake/build/lib:././.lake/packages/UnicodeBasic/.lake/build/lib:././.lake/packages/BibtexQuery/.lake/build/lib:././.lake/packages/doc-gen4/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/art/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././equational_theories/Generated/EquationSearch/theorems/Run5.lean -R ./././. -o ././.lake/build/lib/equational_theories/Generated/EquationSearch/theorems/Run5.olean -i ././.lake/build/lib/equational_theories/Generated/EquationSearch/theorems/Run5.ilean -c ././.lake/build/ir/equational_theories/Generated/EquationSearch/theorems/Run5.c --json
error: Lean exited with code 137
Some required builds logged failures:
- equational_theories.Generated.EquationSearch.theorems.Run5

Has anyone else encountered this issue before?

[Kevin Buzzard]

That file (and indeed the entire project) builds for me on a326d6dfda7f6da2e5f350d4eb4cda214b52d899 (current main)

[Pietro Monticone]

Related question here: #Equational > Do we need to build EquationalSearch files?

[Kevin Buzzard]

Oh -- exit code 137 could be an out-of-memory issue. The machine I built it on had 32G of ram!

[Pietro Monticone]

The "Compile Blueprint" action takes a very long time in those specific PRs

Screenshot 2024-10-08 at 21.31.33.png

[Andrés Goens]

Still working towards getting all the dual proofs, we're making more progress! In equational#459 I'm "lifting" an implication on equations (deep embedding) EquationN => EquationM into a proof for the laws: LawN.implies LawM. I'm building these proofs in the meta code, when adding the tag @[equational_result]. So, now the following "just works":

@[equational_result]
theorem Equation2_implies_Equation3 (G: Type*) [Magma G] (h: Equation2 G) : Equation3 G :=
  fun _ ↦ h _ _

#print Law2_implies_Law3 -- theorem Law2_implies_Law3 : Law.MagmaLaw.implies Law2 Law3 := fun G inst h ↦ (Law3.models_iff G).mpr (Equation2_implies_Equation3 G ((Law2.models_iff G).mp h)

[Andrés Goens]

From these it should be simple to build the proofs of duality now!

[Daniel Weber]

Don't you also need equational#186 for the other direction? That's what's currently blocking my equation_to_law and law_to_equation tactics

[Andrés Goens]

ah, yeah I'm just ignoring that for now :sweat_smile:

[Andrés Goens]

but you're right, I do need it for the other direction

[Andrés Goens]

at least at the laws level it works!

@[equational_result]
theorem Equation2_implies_Equation8 (G: Type*) [Magma G] (h: Equation2 G) : Equation8 G :=
  fun _ ↦ h _ _

theorem Law2_implies_Law8_dual : Law2 ≤ Law23 := by
  apply Law.MagmaLaw.implies_iff_op.mpr
  have Law2op_eq_Law2 : Law2.op = Law2 := by decide
  have Law23op_eq_Law8 : Law23.op = Law8 := by decide
  rw [Law2op_eq_Law2, Law23op_eq_Law8]
  apply Law2_implies_Law8

These should also be able to be generated automatically

[Andrés Goens]

I guess a question here is what we should name them, should we have a separate theorem for the duals (called LawN_implies_LawM_dual), or should we compute the dual and generate that theorem? In the latter case, the @[equational_result] tag would complain when you're trying to prove a theorem where you've already proved the dual

[Andrés Goens]

Maybe this is worth a poll?

[Andrés Goens]

/poll How should we generate dual theorems
New names (not colliding with existing names)
Name collisions (so that the tag would complain if you're proving something where you've proved the dual)

[Joachim Breitner]

I'm still confused why we prove the any implications here explicitly. I can understand that we may want explicit proofs that say the dual of 2 is 2, and the dual of 8 is 23, to have trust in that “database” . So roughly 2000 simple autogenerated proofs, and an entry for that information in the equational_result attribute.

But the (trivial) inference that then, if we have 2 implies 8, we also have 2 implies 23, why not do that when calculating the closure? Why is that more interesting than applying transitivity?

[Andrés Goens]

that's a good point, I don't think they're fundamentally any different. I like that suggestion

[Andrés Goens]

there's something to be said about both cases, in that we're trusting the code that computed these closures if we're not building explicit proofs and having the kernel check them, but we could do that only "just in time" when checking a specific implication

[Andrés Goens]

(I haven't looked at the script generating the closure carefully, but IIRC it's not building those, admittedly trivial, proofs)

[Daniel Weber]

It's not, unless someone has added that since I wrote it. It might be good to formally verify that it correctly computes the closure, though