Zulip Chat Archive
Stream: mathlib4
Topic: Data.Multiset.Basic mathlib4#1491
Johan Commelin (Jan 12 2023 at 12:40):
This file is now red-error free. Still needs to be linted.
Johan Commelin (Jan 12 2023 at 13:48):
A script just fixed at least 128 warnings.
Johan Commelin (Jan 12 2023 at 13:51):
And I manually fixed the rest
Chris Hughes (Jan 12 2023 at 13:54):
The style lint is still failing
Johan Commelin (Jan 12 2023 at 13:55):
Sure, that's the style linter
Johan Commelin (Jan 12 2023 at 13:55):
I was only talking about the orange warnings that lean yells about
Johan Commelin (Jan 12 2023 at 13:56):
There's also a MOVETHIS at the top of the file
Chris Hughes (Jan 12 2023 at 13:57):
Johan Commelin said:
A script just fixed at least 128 warnings.
What is this magic script?
Reid Barton (Jan 12 2023 at 13:57):
https://github.com/leanprover-community/mathlib4/pull/1506
Johan Commelin (Jan 12 2023 at 14:03):
We still need to do a thorough review of all the names and comments in this file
Johan Commelin (Jan 12 2023 at 19:58):
I will try to #lint this file
Johan Commelin (Jan 12 2023 at 20:03):
Hmm, the simpNF linter is again flagging stuff proved by rfl.
Johan Commelin (Jan 12 2023 at 20:03):
How do dsimp-lemmas work in Lean 4?
Johan Commelin (Jan 12 2023 at 20:55):
I fixed some of the issues. But I'm wrapping up for today.
Johan Commelin (Jan 12 2023 at 20:55):
Feel free to take over
Johan Commelin (Jan 13 2023 at 06:47):
I've fixed all linter issues apart from two rfl-lemmas that are being flagged.
Johan Commelin (Jan 13 2023 at 06:47):
I think we discussed this before, but I don't remember the outcome of the discussion.
Mario Carneiro (Jan 13 2023 at 06:51):
what are the lemmas?
Johan Commelin (Jan 13 2023 at 06:52):
card_zero and repeat_zero
Mario Carneiro (Jan 13 2023 at 06:52):
can you show the statements and linter warning?
Johan Commelin (Jan 13 2023 at 06:53):
linter warnings: https://github.com/leanprover-community/mathlib4/actions/runs/3909072917/jobs/6679787663
Johan Commelin (Jan 13 2023 at 06:53):
Johan Commelin (Jan 13 2023 at 06:54):
Mario Carneiro (Jan 13 2023 at 06:54):
so the issue is that these are rfl lemmas but the linter wants you to prove them by simp?
Mario Carneiro (Jan 13 2023 at 06:54):
Are they provable by dsimp?
Johan Commelin (Jan 13 2023 at 06:54):
nope, at least card_zero isnt
Mario Carneiro (Jan 13 2023 at 06:55):
that at least seems like something the linter could take into account
Mario Carneiro (Jan 13 2023 at 06:56):
that is, if the proof is rfl then it should only use dsimp and dsimp lemmas when trying to check whether it is provable
Johan Commelin (Jan 13 2023 at 06:57):
I agree
Johan Commelin (Jan 13 2023 at 06:57):
Shall I nolint with a porting note?
Mario Carneiro (Jan 13 2023 at 06:58):
you should confirm that dsimp does not prove them
Johan Commelin (Jan 13 2023 at 07:19):
VScode knows how to highlight a bit of code in a comment. /-- hi some `code` here -/. Is there some magic that allows me to jump to the next such code position?
Kevin Buzzard (Jan 13 2023 at 07:23):
In lean 3 there was an issue that perhaps dsimp didn't work at that point in the file but it worked later on in the file (or maybe after other files had been imported?) And the linter would catch this. Is that still an issue
Johan Commelin (Jan 13 2023 at 07:42):
I think this PR is ready for review
Johan Commelin (Jan 13 2023 at 07:42):
Can someone please check the final commit: https://github.com/leanprover-community/mathlib4/pull/1491/commits/463207b5f2fa84a465dabbfb440332fb8ce352fd
Johan Commelin (Jan 13 2023 at 07:42):
It contains some naming fixes that I wasn't sure about
Johan Commelin (Jan 13 2023 at 07:43):
The rest should be uncontroversial
Ruben Van de Velde (Jan 13 2023 at 08:21):
I don't understand why foldrInduction rather than foldr_induction
Ruben Van de Velde (Jan 13 2023 at 08:21):
But also I've seen a few fooInductions before (and didn't understand those either)
Johan Commelin (Jan 13 2023 at 08:21):
Well, there's also Quot.inductionOn2 in its proof
Johan Commelin (Jan 13 2023 at 08:23):
Ooh wait, that was a different induction principle. Let me find it
Johan Commelin (Jan 13 2023 at 08:24):
Johan Commelin (Jan 13 2023 at 08:25):
So I no longer understand when to :camel: and when to :snake:
Mario Carneiro (Jan 13 2023 at 08:27):
What's the scenario?
Johan Commelin (Jan 13 2023 at 08:27):
Johan Commelin said:
Can someone please check the final commit: https://github.com/leanprover-community/mathlib4/pull/1491/commits/463207b5f2fa84a465dabbfb440332fb8ce352fd
:this:
Mario Carneiro (Jan 13 2023 at 08:27):
is it a proof -> snake case
Johan Commelin (Jan 13 2023 at 08:28):
so what about Quotient.inductionOn2?
Johan Commelin (Jan 13 2023 at 08:28):
That's in core, and is :camel:
Johan Commelin (Jan 13 2023 at 08:28):
Is that a bug?
Ruben Van de Velde (Jan 13 2023 at 08:28):
Should we use ¬p or !p for p : Bool?
Mario Carneiro (Jan 13 2023 at 08:28):
is it in core -> assume it hasn't been vetted
Ruben Van de Velde (Jan 13 2023 at 08:28):
Because now we're getting goals like filter p l ++ filter (fun x => decide ¬p x = true) l ~ l
Mario Carneiro (Jan 13 2023 at 08:30):
Ruben Van de Velde said:
Should we use
¬por!pforp : Bool?
¬p
Mario Carneiro (Jan 13 2023 at 08:30):
lemmas using !p might exist but they will be the more specialized ones
Johan Commelin (Jan 13 2023 at 08:38):
I'll fix the foldrInduction name
Johan Commelin (Jan 13 2023 at 08:39):
done
Eric Wieser (Jan 13 2023 at 08:49):
I think I sent a bunch of multiset PRs to mathlib3 bors last night, and forgot to check if there was an open mathlib4 PR
Mario Carneiro (Jan 13 2023 at 08:49):
let's just put those off until the next update
Mario Carneiro (Jan 13 2023 at 08:50):
the mathlib4 PR is basically ready to go
Johan Commelin (Jan 13 2023 at 08:53):
I moved the MOVETHIS section that was at the top of the file
Johan Commelin (Jan 13 2023 at 08:53):
PR should now be ready
Ruben Van de Velde (Jan 13 2023 at 09:12):
Made some more comments on the PR.
(I noticed that #15910 needs a port, but let's wait until this one is merged)
Yaël Dillies (Jan 13 2023 at 09:16):
We can do a pass to catch everything that touched data.multiset.basic in the meantime.
Kevin Buzzard (Jan 13 2023 at 09:39):
Yeah let's get this merged. Well done everyone, these files are hard.
Last updated: Dec 20 2023 at 11:08 UTC