Skip to content

Commit

Permalink
All4x4Tables: BUG lost implications after pruning
Browse files Browse the repository at this point in the history
The script at `equational_theories/Generated/All4x4Tables/src/generate_lean.py`
is supposed to read the implications.json file, and prune the finite magma
checks based on that, so that we don't have to generate redundant explicit
refutations that already follow from the known implications.

I recently ported this script to work with the cancellative magmas added
in teorth#224.

Unfortunately, there seems to be a bug in this naive port: once we move to
implicit refutations, the total proof_false decreases, and the number of
unknowns increases. For example, running on a now-recent main we have

```
BEFORE (explicit proofs in All4x4Tables):
{"explicit_proof_true": 28263,
"implicit_proof_true": 5457962,
"unknown": 2726304,
"implicit_proof_false": 3486,
"explicit_proof_false": 13845794
}

AFTER (implicit proofs in All4x4Tables):
{"explicit_proof_true": 28263,
"implicit_proof_true": 5457962,
"unknown": 2744422,
"implicit_proof_false": 13185894,
"explicit_proof_false": 645268
}
```

To reproduce,

1. Generate an `implications.json` using
 `lake exe extract_implications  --json --only-implications equational_theories`

2. Run the version of `generate_lean.py` from this commit.

3. Build the proofs, then inspect the output of
 `lake exe extract_implications outcomes --hist`.
  • Loading branch information
zaklogician committed Oct 4, 2024
1 parent d0746fb commit 63355c2
Show file tree
Hide file tree
Showing 542 changed files with 1,564 additions and 1,228 deletions.
34 changes: 0 additions & 34 deletions equational_theories/Generated/All4x4Tables.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 3 additions & 1 deletion equational_theories/Generated/All4x4Tables/Refutation0.lean

Large diffs are not rendered by default.

4 changes: 3 additions & 1 deletion equational_theories/Generated/All4x4Tables/Refutation1.lean

Large diffs are not rendered by default.

4 changes: 3 additions & 1 deletion equational_theories/Generated/All4x4Tables/Refutation10.lean

Large diffs are not rendered by default.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading

0 comments on commit 63355c2

Please sign in to comment.