Equations command modification #427

0art0 · 2024-10-08T10:27:22Z

This PR modifies the equation command to automatically generate the corresponding law with variables over Fin n (in addition to the law with variables over Nat that is already being generated).

This is used to show that the automatically generated laws are equivalent to the original equation in terms of satisfiability.

Additionally, this PR introduces an environment extension to store all the equational laws, which can be used to export laws as described in #142.

This PR also modifies a result transporting laws from Fin n to Nat to omit the n != 0 hypothesis.

This reverts commit a3cf909, reversing changes made to fd25f3f.

This reverts commit f0eabb9.

goens · 2024-10-08T11:19:51Z

this looks good to me!

pitmonticone · 2024-10-08T14:30:43Z

Thank you very much @0art0!
Please make sure the project builds correctly by locally running scripts/run_before_push.sh.

0art0 · 2024-10-08T16:36:32Z

Thanks. I seem to be getting a strange build error in 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

I can't immediately think of a reason why the changes introduced in my code would be causing this, but I'll continue to track down the issue.

pitmonticone · 2024-10-08T18:03:35Z

Ok @0art0. I will take a look at it later.

Can you please resolve the merge conflicts?

…into equations-command-modification

0art0 · 2024-10-08T18:57:43Z

@pitmonticone Thank you so much. I've merged conflicts on both PRs.

Shreyas4991 · 2024-10-08T22:54:31Z

@0art0 : Is this PR ready for reviewing? I believe there is another PR that is dependent on this one as well.

0art0 · 2024-10-08T22:57:14Z

Yes, it's ready for reviewing. Thank you for helping out with fixing the build issues. The PR that depends on this one is #429.

0art0 · 2024-10-08T22:59:47Z

awaiting-review

Shreyas4991

I wonder if the MagmaNat theorems and the theorems in EquationalLawConversion should have corresponding blueprint entries. @0art0 and @teorth your thoughts? On the one hand these are fairly trivial theorems, on the other hand the blueprints in the past have contained all the tiny lemmata as well.

0art0 · 2024-10-08T23:14:32Z

I think the theorems converting between MagmaLaws over Fin n and Nat can be added to the blueprint. The EquationalLawConversion file is more of an implementation detail, in my opinion; it was a quick hack on my part to bypass the complicated meta-programming that would otherwise be required to convert maps from Fin n to a curried sequence of quantifiers.

Shreyas4991 · 2024-10-08T23:17:21Z

~~@0art0 : which task does this PR close btw?~~ EDIT : Found it.

About the blueprint: Seems sensible. I'll change this PR to a draft, once the blueprint is ready we can get this merged.

0art0 · 2024-10-08T23:21:43Z

This closes #428. Alright, I can add a note about the conversion between MagmaLaws over Fin n and Nat. I think it would be good for @goens to have a look at it when it's done, since it's the machinery he formalized in #368.

pitmonticone · 2024-10-08T23:47:49Z

The action didn't timeout, but it still took 53 minutes to run the project. Is this expected?

I'm inclined to merge both PRs (#427 and #429) because they look fine to me (even if the branch of #429 seem to have been created from the branch of #427 which isn't considered best practice), but I may be missing something.

See discussion here https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Do.20we.20need.20to.20build.20EquationalSearch.20files.3F/near/475682423

Shreyas4991 · 2024-10-08T23:53:26Z

Let's wait for the blueprint to be updated

0art0 · 2024-10-09T00:21:16Z

I've added a section to the blueprint.

pitmonticone · 2024-10-09T00:39:24Z

Great, the cache mechanism worked properly and now it took just a few minutes.

pitmonticone · 2024-10-09T00:47:15Z

Thanks again @0art0!

Exports the equations defined in `Equations.lean` and `AllEquations.lean` to a JSON file `data/magma_equations.json`. Depends on PR #427. --------- Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>

goens · 2024-10-09T06:40:58Z

The blueprint looks good to me too! (I presume @teorth would have written down the proof as 'trivial', but I think this level of detail doesn't hurt either)

eric-wieser · 2024-10-09T14:00:40Z

equational_theories/EquationsCommand.lean

+  -- define law over `Fin n`
+  elabCommand (← `(command| abbrev%$tk $finLawIdent : Law.MagmaLaw (Fin $freeMagmaSize) := $tl))
+  -- compatibility between the `finLaw` and the original equation
+  let modelsIffLemma : Ident := mkIdent (.mkSimple s!"models_iff_{is.size}")
+  elabCommand (← `(command| abbrev%$tk $finThmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $finLawIdent ↔ $eqIdent G := $modelsIffLemma $finLawIdent))
+  -- define the actual law over `Nat`
+  elabCommand (← `(command| abbrev%$tk $lawIdent : Law.NatMagmaLaw := $tl))
+  -- compatibility between the law and the original equation
+  elabCommand (← `(command| abbrev%$tk $thmName : ∀ (G : Type _) [$inst : Magma G], G ⊧ $lawIdent ↔ $eqIdent G :=
+                    fun G _ ↦ Iff.trans (Law.satisfies_fin_satisfies_nat G $finLawIdent).symm ($finThmName G)))


It might be better to do this in a more low-level way, rather than re-elaborating the law repeatedly. A hybrid approach would be to elaborate the law once and use Expr.toSyntax to repeat it.

Thanks for the suggestion. The law happens to be elaborated slightly differently in the two situations -- in one case, the leaves are coerced to Fin n, while in the second case, they are left as natural numbers, so storing the rest of elaboration as an expression may not directly work. (It's possible that I may be misunderstanding the comment.)

…ld (#465) #427 has caused builds to become much slower. If I comment out two lines that it added, as in this PR, build times become reasonable again. This is a stopgap until we understand the source of the slowness.

0art0 added 10 commits October 7, 2024 02:12

Counter-example files

7ff497d

Merge branch 'main' of https://github.com/teorth/equational_theories

fd25f3f

Generalize satisfies_fin_satisfies_nat to omit n != 0 assumption

f2e0349

Remove ¬(n = 0) assumption from lemmas in Preorder

272c8e4

Automatically generate compatibility proof between Law and Equation

ae8a0cc

Environment extension for magma laws

96e3bc3

Merge branch 'main' into equations-command-modification

a3cf909

Revert "Merge branch 'main' into equations-command-modification"

f0eabb9

This reverts commit a3cf909, reversing changes made to fd25f3f.

Reapply "Merge branch 'main' into equations-command-modification"

f509781

This reverts commit f0eabb9.

Delete auto-generated conjecture files

33a66f3

0art0 mentioned this pull request Oct 8, 2024

META: Automatically generate laws from equations together with proofs of equi-satisiability #428

Closed

This was referenced Oct 8, 2024

Export equations #429

Merged

DATA: Create an automated tool to regularly gather the equations from Equations.lean and AllEquations.lean and output them to a text file that is easy for machines to read #142

Closed

Merge branch 'main' of https://github.com/teorth/equational_theories …

d68a19a

…into equations-command-modification

Merge branch 'main' into equations-command-modification

e2ebf4b

pitmonticone self-assigned this Oct 8, 2024

pitmonticone marked this pull request as draft October 8, 2024 22:07

Shreyas4991 marked this pull request as ready for review October 8, 2024 22:54

github-actions bot added the awaiting-review the PR passes CI and is ready for review label Oct 8, 2024

Shreyas4991 reviewed Oct 8, 2024

View reviewed changes

Shreyas4991 mentioned this pull request Oct 9, 2024

improved equation command #448

Merged

Blueprint on magma law conversion lemma

723b6e8

Merge branch 'main' into equations-command-modification

20567c6

pitmonticone merged commit adc92cb into teorth:main Oct 9, 2024
1 check passed

eric-wieser reviewed Oct 9, 2024

View reviewed changes

dwrensha mentioned this pull request Oct 9, 2024

comment out MagmaLawExt.addEntry call that majorly slows down the build #465

Merged

teorth mentioned this pull request Oct 9, 2024

split AllEquations into pieces for more parallelism #472

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Equations command modification #427

Equations command modification #427

0art0 commented Oct 8, 2024

goens commented Oct 8, 2024

pitmonticone commented Oct 8, 2024

0art0 commented Oct 8, 2024

pitmonticone commented Oct 8, 2024

0art0 commented Oct 8, 2024

Shreyas4991 commented Oct 8, 2024

0art0 commented Oct 8, 2024 •

edited

Loading

0art0 commented Oct 8, 2024

Shreyas4991 left a comment •

edited

Loading

0art0 commented Oct 8, 2024 •

edited

Loading

Shreyas4991 commented Oct 8, 2024 •

edited

Loading

0art0 commented Oct 8, 2024

pitmonticone commented Oct 8, 2024

Shreyas4991 commented Oct 8, 2024

0art0 commented Oct 9, 2024

pitmonticone commented Oct 9, 2024

pitmonticone commented Oct 9, 2024

goens commented Oct 9, 2024

eric-wieser Oct 9, 2024

0art0 Oct 10, 2024

Equations command modification #427

Equations command modification #427

Conversation

0art0 commented Oct 8, 2024

goens commented Oct 8, 2024

pitmonticone commented Oct 8, 2024

0art0 commented Oct 8, 2024

pitmonticone commented Oct 8, 2024

0art0 commented Oct 8, 2024

Shreyas4991 commented Oct 8, 2024

0art0 commented Oct 8, 2024 • edited Loading

0art0 commented Oct 8, 2024

Shreyas4991 left a comment • edited Loading

Choose a reason for hiding this comment

0art0 commented Oct 8, 2024 • edited Loading

Shreyas4991 commented Oct 8, 2024 • edited Loading

0art0 commented Oct 8, 2024

pitmonticone commented Oct 8, 2024

Shreyas4991 commented Oct 8, 2024

0art0 commented Oct 9, 2024

pitmonticone commented Oct 9, 2024

pitmonticone commented Oct 9, 2024

goens commented Oct 9, 2024

eric-wieser Oct 9, 2024

Choose a reason for hiding this comment

0art0 Oct 10, 2024

Choose a reason for hiding this comment

0art0 commented Oct 8, 2024 •

edited

Loading

Shreyas4991 left a comment •

edited

Loading

0art0 commented Oct 8, 2024 •

edited

Loading

Shreyas4991 commented Oct 8, 2024 •

edited

Loading