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.

Sign up for GitHub

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

Jump to bottom

MODIFIED_GREEDY: Refute 1692 -> 47, 1832, 2441, 3050, 3456, 4065 #607

Closed
teorth opened this issue Oct 16, 2024 · 2 comments · Fixed by #1069
Closed

MODIFIED_GREEDY: Refute 1692 -> 47, 1832, 2441, 3050, 3456, 4065 #607

teorth opened this issue Oct 16, 2024 · 2 comments · Fixed by #1069
Assignees
@Aaron1011

Comments

@teorth
Copy link
Owner

teorth commented Oct 16, 2024 •
edited
Loading

See https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Proposed.20new.20target.3A.2063.20and.201692.20.28.22Dupont.20and.20Dupond.22.29/near/477252513 for the human-readable proof.

The formal proof can go in the ManuallyProved folder. ManuallyProved.lean should be updated afterwards, and the appropriate conjectures from Conjectures.lean removed.
@teorth teorth converted this from a draft issue Oct 16, 2024
@Aaron1011
Copy link
Contributor

claim

@teorth teorth moved this from Unclaimed Outstanding Tasks to Claimed Tasks in Equational Theories Project Oct 18, 2024
@teorth teorth changed the title MODIFIED_GREEDY: Formalize all open anti-implications coming from 1692 MODIFIED_GREEDY: Refute all open implications coming from 1692 Oct 23, 2024
@teorth teorth changed the title MODIFIED_GREEDY: Refute all open implications coming from 1692 MODIFIED_GREEDY: Refute 1692 -> 47, 1832, 2441, 3050, 3456, 4065 Nov 1, 2024
@Aaron1011
Copy link
Contributor

propose #1069

@github-actions github-actions bot mentioned this issue Jan 29, 2025
Merged
@teorth teorth moved this from Claimed Tasks to In Progress in Equational Theories Project Jan 29, 2025
teorth pushed a commit that referenced this issue Jan 30, 2025
@Aaron1011 @pitmonticone
Formalize refutations: 1692 -> 47, 1832, 2441, 3050, 3456, 4065 (#1069)
9734e5d 
This is based on this paper describing a proof strategy for the above
non-implications:

https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Proposed.20new.20target.3A.2063.20and.201692.20.28.22Dupont.20and.20Dupond.22.29/near/477252513

There's still quite a bit of room for cleanup (e.g. factoring out common
code from several `match` branches). It's also very likely that there
are simpler ways to prove some of the longer lemmas (e.g.
`partial_function`), as I wasn't working off of the above paper for
those proofs. However, this is now in a state where it's ready for
review - I'm happy to spend more time minimizing this if it would be
useful.

Closes #607

---------

Co-authored-by: Pietro Monticone <[email protected]>
@github-project-automation github-project-automation bot moved this from In Progress to Completed Tasks in Equational Theories Project Jan 30, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Aaron1011 Aaron1011

Labels
None yet
Projects
Equational Theories Project
Status: Completed Tasks
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Formalize refutations: 1692 -> 47, 1832, 2441, 3050, 3456, 4065 Aaron1011/equational_theories
2 participants
@teorth @Aaron1011