Autogenerated proof worth showing

Stream: Equational

[Martin Dvořák]

[a thread of a very low relevance; you probably want to ignore it]

I will be giving a talk about this project at a small local event.
I think that, as a part of my presentation, it would be nice to show one or two of the auto-generated proofs.
Do you have a suggestion which auto-generated proof is nice but not trivial?
While browsing the repo, I found the following proof generated by egg (edited for human readability):

-- equation 877 : `x = y ◇ ((x ◇ x) ◇ (z ◇ z))`
-- equation 2 :   `x = y`

example (G : Type) [Magma G] (ass : Equation877 G) : Equation2 G :=
fun x₁ y₁ =>

  let x₂ := x₁ ◇ x₁
  let x₄ := x₂ ◇ x₂
  let x₈ := x₄ ◇ x₄
  let y₂ := y₁ ◇ y₁
  let y₄ := y₂ ◇ y₂
  let y₈ := y₄ ◇ y₄

  have hy₈ : y₁ = y₈ := ass y₁ y₄ y₁

  calc x₁
  _ = y₁ ◇ x₄                := by rw [ass x₁ y₁ x₁]
  _ = y₁ ◇ (y₁ ◇ (x₈ ◇ x₈))  := by rw [ass x₄ y₁ x₄]
  _ = y₁ ◇ (y₁ ◇ (x₁ ◇ x₁))  := by rw [ass x₁ x₄ x₁]
  _ = y₁ ◇ (y₈ ◇ (x₁ ◇ x₁))  := by rw [hy₈]
  _ = y₄                     := by rw [←ass y₄ y₁ x₁]
  _ = y₁ ◇ (y₈ ◇ (y₁ ◇ y₁))  := by rw [ass y₄ y₁ y₁]
  _ = y₁ ◇ (y₁ ◇ (y₁ ◇ y₁))  := by rw [hy₈]
  _ = y₁ ◇ (y₁ ◇ (y₈ ◇ y₈))  := by rw [hy₈]
  _ = y₁ ◇ y₄                := by rw [ass y₄ y₁ y₄]
  _ = y₁                     := by rw [←ass y₁ y₁ y₁]

I think it is pretty neat!
Do you have a different suggestion?

[Martin Dvořák]

Since Zulip messed up the formatting a bit, I am posting it as a screenshot as well:
image.png

[Andrés Goens]

I'm biased here (because I committed that one), so I of course also think it's pretty neat! Just should plug @Joachim Breitners calcify here, which is doing the heavy lifting here in terms of neatness!

[Martin Dvořák]

I mean, the proof itself is pretty neat(*) . As for the presentation, it was just a trivial refactoring done manually.

(*) Or do you see an easy way how to shorten the proof?

[Andrés Goens]

oh, wait, I think I spoke too soon. I thought this was from the subgraph file (where we used the egg tactic for generating proof scripts with calcify), but maybe you meant it was the specialized magmaegg one? I can't find the original proof in the repo tbh

[Andrés Goens]

by the way, the naming for the assumption in that manual refactor might be slightly less than ideal :sweat_smile:

[Martin Dvořák]

Andrés Goens said:

oh, wait, I think I spoke too soon. I thought this was from the subgraph file (where we used the egg tactic for generating proof scripts with calcify), but maybe you meant it was the specialized magmaegg one? I can't find the original proof in the repo tbh

https://github.com/teorth/equational_theories/blob/68a6284d55aa082d15070e9a2cafcffb0d958190/equational_theories/Generated/MagmaEgg/small/_005.lean#L108

[Martin Dvořák]

Andrés Goens said:

by the way, the naming for the assumption in that manual refactor might be slightly less than ideal :sweat_smile:

I hate standalone h as a name.

[Andrés Goens]

Martin Dvořák said:

Andrés Goens said:

oh, wait, I think I spoke too soon. I thought this was from the subgraph file (where we used the egg tactic for generating proof scripts with calcify), but maybe you meant it was the specialized magmaegg one? I can't find the original proof in the repo tbh

https://github.com/teorth/equational_theories/blob/68a6284d55aa082d15070e9a2cafcffb0d958190/equational_theories/Generated/MagmaEgg/small/_005.lean#L108

ahh, thanks, yeah I had a typo in my search. Right, that's indeed a magma egg proof, so no calcify refactor, my bad!

[Andrés Goens]

Martin Dvořák said:

Andrés Goens said:

by the way, the naming for the assumption in that manual refactor might be slightly less than ideal :sweat_smile:

I hate standalone h as a name.

right, but "ass" means something else too :sweat_smile:

[Martin Dvořák]

My point was to ask whether other contributors have their favorite auto-generated proof for human audience.

[Bruno Le Floch]

The second half of the proof is redundant in a sense: once you know any $x=y^4$ you have $x=y^4=z$.

[Martin Dvořák]

Oh yeah! How blind I was! Thanks a lot for noticing!

[Martin Dvořák]

It is weird that we don't have a direct proof of:
https://teorth.github.io/equational_theories/implications/show_proof.html?pair=180,2

Was there some kind of cleaning that removed proofs that were already in the transitive closure?

[Vlad Tsyrklevich]

Yes, we try to minimize proofs. (It is still not 100% minimal, but close enough)

[Martin Dvořák]

Minimize proofs or minimize the number of theorems that cover the implication graph?

[Vlad Tsyrklevich]

sorry, I should have said minimize the number of proofs, so the latter.

[Zoltan A. Kocsis (Z.A.K.)]

I guess it's reasonable to limit the number of proofs, not only to shorten compile times but also to ease the future maintenance burden. After finishing the article, it could be interesting to review the repo and create a "Cutting Room Floor" collection, separate from the main project, to showcase some of the unused proofs.

[Vlad Tsyrklevich]

I don't think they're interesting, they're just auto-generated proofs of the same form as others that remain in the repo. None that were removed were human-written.