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

Fix FieldTheory.RatFunc #4513

Closed
urkud opened this issue May 31, 2023 · 13 comments
Closed

Fix FieldTheory.RatFunc #4513

urkud opened this issue May 31, 2023 · 13 comments

Comments

@urkud
Copy link
Member

urkud commented May 31, 2023

In the original file, sometimes K is a field and sometimes K is a
commutative ring (optionally, a domain). In some sections, this was
incorrectly translated to Lean 4 in #4293. This blocks #4512
@urkud urkud mentioned this issue May 31, 2023
Closed
1 task
@adomani
Copy link
Collaborator

adomani commented May 31, 2023

Yuri, I already had some suspicions that something like this could be happening, and I had a PR with a beginning of a cleanup: #4373.

Naïvely, I just trusted that Lean would pick up the right combination of typeclasses, without having to check it, but it seems that I was wrong.

Still, this is very laborious to check by hand, since in the local context you always have all the available variables, and only after elaboration, the final declaration looses the "irrelevant" ones. So, my approach would be to #print every theorem and check that it got the right typeclasses... Maybe this could be automated, flagging a discrepancy with mathlib3, when there is one?

@adomani
Copy link
Collaborator

adomani commented May 31, 2023

Let me also ping @eric-wieser and @Vierkantor, since they were also in the loop for these issues.

@eric-wieser
Copy link
Member

Maybe it would be reasonable to refactor this in mathlib3 to use sections, and then re-port the file from scratch?

@adomani
Copy link
Collaborator

adomani commented May 31, 2023

Eric, you are probably right. I find this issue of auto-include/omit more subtle than the autoImplicit ones. Is it possible to disable it?

@eric-wieser
Copy link
Member

No, I don't think so. The exact behavior as I understand it is "all the variables that exist are available inside the proof, but the ones you don't use are removed automatically"

@adomani
Copy link
Collaborator

adomani commented May 31, 2023 •
edited
Loading

I started on branch#adomani_section_ratfunc but won't have time to finish in a few hours.

@adomani adomani mentioned this issue May 31, 2023
Closed
@adomani
Copy link
Collaborator

adomani commented May 31, 2023 •
edited
Loading

I finished the sectioning of field_theory/ratfunc: #19133.

EDIT: it passes CI.

bors bot pushed a commit to leanprover-community/mathlib that referenced this issue Jun 1, 2023
@adomani
chore(field_theory/ratfunc): use section instead of omit/include (#…
f9b523e 
…19133)

This hopefully closes [#4513](leanprover-community/mathlib4#4513) (or at least mitigates it) and will settle [!4#4373](leanprover-community/mathlib4#4373) in mathlib3.
bors bot pushed a commit to leanprover-community/mathlib that referenced this issue Jun 1, 2023
@adomani @Vierkantor
chore(field_theory/ratfunc): use section instead of omit/include (#…
6723746 
…19133)

This hopefully closes [#4513](leanprover-community/mathlib4#4513) (or at least mitigates it) and will settle [!4#4373](leanprover-community/mathlib4#4373) in mathlib3.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@adomani
Copy link
Collaborator

adomani commented Jun 1, 2023

An update: @Vierkantor approved the mathlib3 PR.

Once it merges, I'll prepare the matching mathlib4 port of RatFunc and hopefully this will fix Yuri's porting problems!

@adomani adomani mentioned this issue Jun 2, 2023
Closed
@adomani
Copy link
Collaborator

adomani commented Jun 2, 2023

I finished the forward-port PR: #4580. Once CI is happy, I will try to merge it into Yuri's #4512 and see if it improves the situation!

@adomani
Copy link
Collaborator

adomani commented Jun 2, 2023

#4580 passes CI, I merged it into Yuri's PR and it builds locally and passed the building step of CI. It's all looking good!

bors bot pushed a commit that referenced this issue Jun 3, 2023
@adomani @eric-wieser
chore(FieldTheory.Ratfunc): forward-port #19133 (#4580)
b4fa258 
This PR re-ports `FieldTheory/RatFunc`, now that the mathlib3 version uses `section`s, after PR[#19133](leanprover-community/mathlib#19133).

This closes [#4513](#4513) and closes #4373.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@adomani
Copy link
Collaborator

adomani commented Jun 5, 2023

@urkud, I'm guessing that this issue can now be closed, right?

@urkud
Copy link
Member Author

urkud commented Jun 6, 2023

Yes, indeed. I guess, it was not auto closed because Github doesn't know that your PR was merged, not discarded.

@urkud urkud closed this as completed Jun 6, 2023
@adomani
Copy link
Collaborator

adomani commented Jun 6, 2023

Probably, but the other PR did autoclose!

qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this issue Jun 12, 2023
@adomani @eric-wieser @qawbecrdtey
chore(FieldTheory.Ratfunc): forward-port #19133 (leanprover-community…
b0bd281 
…#4580)

This PR re-ports `FieldTheory/RatFunc`, now that the mathlib3 version uses `section`s, after PR[#19133](leanprover-community/mathlib#19133).

This closes [leanprover-community#4513](leanprover-community#4513) and closes leanprover-community#4373.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
3 participants
@urkud @eric-wieser @adomani