Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix bug in counter example pruning script #271

Merged
merged 2 commits into from
Oct 4, 2024
Merged

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Oct 4, 2024

Strangely, even after updating implications.json to the latest version, the unknown count increases from from 2726304 to 2734065. Not sure what’s going on, but as this is definitely fixing one (among more than one?) bug, probably still worth merging.

This does not update the All4x4Magmas files, because I’m confused how they should be generated these days, see
https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/4.C3.974.20magmas/near/474767268

got one implication wrong.

It seems that for the 4x4 table there was some change to the underlying
`refutations4x4.txt` file, because it is changing more files than I
expected.
@zaklogician
Copy link
Contributor

zaklogician commented Oct 4, 2024

The Refutation*.lean files checked into the current main branch are generated using the generate_5x5_refutations.sh bash script from the file plan-5x5.txt (itself generated from other files by a heap of tools starting with Mace4, although a copy is checked in so we don't have to rerun it every time).

The bash script itself calls out to a Haskell tool, gen-refutations in src/finite_magma_tools which parses data/plan-5x5.txt and emits the Lean code directly.

However, gen-refutations does not read implications.json and does not do pruning - it's a throwaway tool, meant to eventually be replaced by an updated generate_lean.py which can handle something like plan-5x5.txt. I made an attempt at doing precisely this (see the repo linked in #265) but bounced back when the implication counts didn't match up.

I think this bug might have been the cause, so I'll revisit #265 by rebasing my port over this once this is merged.

@nomeata nomeata merged commit 1082fda into main Oct 4, 2024
2 checks passed
@nomeata nomeata deleted the joachim/fix-pruning branch October 4, 2024 09:05
teorth pushed a commit that referenced this pull request Oct 4, 2024
I implemented `make-plan` output format support in `generate_lean.py`.
This means that it can now be used to prune the refutation set of the
cancellative 5x5 magmas using the already proven implications read from
`implications.json`.

This greatly reduces the number of explicit proofs we have to do: of the
previous 196990 facts that we had to check explicitly, pruning leaves
only 24266 (a 87% improvement).

Since #271 fixed the bug that led to lost implications, this now put us
back on 2726304 unknowns.

Merging this will resolve issue #265 .

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants