-
Notifications
You must be signed in to change notification settings - Fork 297
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
feat(combinatorics/additive/small_roth): Small Roth numbers #10645
Conversation
This PR/issue depends on: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you make the file more self-contained by expanding greatly the docstrings, to explain what is being computed and what are the properties that are satisfied by everything? In its current state, it is very hard to review.
|
||
namespace roth | ||
|
||
/-- `roth.presalem_spencer a l` returns whether there doesn't exist `b, c ∈ l` such that |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/-- `roth.presalem_spencer a l` returns whether there doesn't exist `b, c ∈ l` such that | |
/-- `roth.presalem_spencer a l` returns true iff there doesn't exist `b, c ∈ l` such that |
namespace roth | ||
|
||
/-- `roth.presalem_spencer a l` returns whether there doesn't exist `b, c ∈ l` such that | ||
`a + c = 2 * b`. `l` is a Salem-Spencer iff `presalem_spencer a l'` holds for all `a ∈ l` with `l'` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
`a + c = 2 * b`. `l` is a Salem-Spencer iff `presalem_spencer a l'` holds for all `a ∈ l` with `l'` | |
`a + c = 2 * b`. The list `l` is a Salem-Spencer iff `presalem_spencer a l'` holds for all `a ∈ l` with `l'` |
something is missing before the iff
.
(H.2.1 hb hc e).not_gt $ hl.rel hb) } | ||
end | ||
|
||
/-- The Roth number algorithm invariant. -/ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you expand the docstring, and give a better name?
Bhavik and I decided that we need to know more about the complexity of Lean 4's operations to decide whether this algorithm is worth pursuing, the tradeoff being that this algorithm does a lot of search (it's a barely optimised DFS), while Lean 4 might let us do a lot of reasoning for little cost. |
This implements the BASIC2 algorithm from that paper.
Co-authored-by: Mario Carneiro
Co-authored-by: Bhavik Mehta bhavikmehta8@gmail.com
An example search is available on branch
roth_demo
. We will add tactics to perform and cache the search automatically later.