Zulip Chat Archive
Stream: mathlib4
Topic: count_eq_card_filter_eq
Xavier Roblot (Jan 30 2023 at 13:56):
The statement of the lemma count_eq_card_filter_eq
in Data.Multiset.Basic has been changed from
s.count a = (s.filter (eq a)).card
to
s.count a = card (s.filter (· = a))
But, if I am not mistaken, eq a
is not defeq to (· = a)
but to (a = ·)
so this causes problem down the road.
Was that changed on purpose?
Reid Barton (Jan 30 2023 at 14:07):
I also saw something like this in Data.List and I was confused. I agree it should be (a = .)
.
Ruben Van de Velde (Jan 30 2023 at 14:14):
Looks like Johan changed it in https://github.com/leanprover-community/mathlib4/pull/1491/commits/e1ec67869407977d4a14f33d3fab3d428cf3d1d7
Reid Barton (Jan 30 2023 at 14:21):
It might be worth trying to change the definition of Multiset.count
back to using a = .
and fixing whatever breaks as a result
Xavier Roblot (Jan 30 2023 at 14:56):
Hum, the problem goes all the way down to the definition of List.count
where eq a
was replaced by (· == a)
Let see what happens if I switch the equality...
Johan Commelin (Jan 30 2023 at 14:57):
@Xavier Roblot Yes, but we decided that List
is CS world, so there we use Bool
-valued stuff.
Reid Barton (Jan 30 2023 at 14:57):
Oh I searched for this but there are no lemmas about it in Data.List.Basic so I concluded it doesn't exist.
Reid Barton (Jan 30 2023 at 14:57):
The issue (or one issue) is the order of the equality
Johan Commelin (Jan 30 2023 at 14:58):
Aha, I see. And I guess List.count
is in Std?
Reid Barton (Jan 30 2023 at 14:58):
In that case we should make the definition of Multiset.count
agree with the Lean 3 definition, and fix any resulting mismatches with List.count
there.
Johan Commelin (Jan 30 2023 at 14:59):
Otoh, maybe Std would be open to swapping the order?
Reid Barton (Jan 30 2023 at 15:00):
It may also be, in which case we can then unfix the mismatches
Xavier Roblot (Jan 30 2023 at 15:02):
I am afraid if we don't switch the order it will cause more problems down the road.
Reid Barton (Jan 30 2023 at 15:03):
You mean switch from the current mathlib 4 definition of Multiset.count
to the original definition as in mathlib 3, right?
Xavier Roblot (Jan 30 2023 at 15:04):
You mean switch from the current mathlib 4 definition of
Multiset.count
to the original definition as in mathlib 3, right?
Yes, lot of lemmas assume that the order in the same as the one of eq
as it was in mathlib3
Reid Barton (Jan 30 2023 at 15:05):
Yes, then we agree
Xavier Roblot (Jan 30 2023 at 15:25):
As expected, changing the definition of List.count
breaks a lot of things...
Johan Commelin (Jan 30 2023 at 16:20):
Yeah, I think you should just make the change at the Multiset
boundary.
Xavier Roblot (Jan 30 2023 at 16:38):
It is still not so easy since List.count
is used all over the place in Multiset.Basic
and the two definitions would not agree anymore. I guess one way to fix it would be to have both definitions for Multiset.count
and prove they are equal...
Eric Wieser (Jan 30 2023 at 16:40):
Xavier Roblot said:
As expected, changing the definition of
List.count
breaks a lot of things...
Can we fix those things? This sounds like we made the mistake of working around a problem when porting instead of diagnosing it, and now we're diagnosing it after already hacking everything to work.
Xavier Roblot (Jan 30 2023 at 20:12):
Eric Wieser said:
Xavier Roblot said:
As expected, changing the definition of
List.count
breaks a lot of things...Can we fix those things? This sounds like we made the mistake of working around a problem when porting instead of diagnosing it, and now we're diagnosing it after already hacking everything to work.
Well, there are not that many errors but some of those have to do with things like decide (a = b)
and I am not sure how to handle those. In any case, as Johan pointed out , the definition of List.count
is part of Std.
Xavier Roblot (Jan 31 2023 at 10:38):
At this point, I see 3 possibilities:
- Leave the definitions of
List.count
andMultiset.count
as they are and just fix proofs as we do the porting - Fix only the definition of
Multiset.count
and use some auxiliary result to show thatList.count
andMultiset.count
agree - Fix the definitions of both
List.count
andMultiset.count
Solution 1. is probably the easiest solution but I think 3. is the right solution. I am not a big fan of solution 2 but I think it is still better than solution 1. I am willing to work on some PR to implement solution 2 or 3 but for solution 3, as mentioned above, since List.count
is part of Std, that would first require that Lean 4 people agree with the change.
Johan Commelin (Jan 31 2023 at 18:45):
@Mario Carneiro Do you think Std would welcome a change in the defn of List.count
?
Mario Carneiro (Jan 31 2023 at 18:47):
what change?
Mario Carneiro (Jan 31 2023 at 18:48):
swapping the order of arguments to beq I think is fine, but changing it to use eq is less so
Johan Commelin (Jan 31 2023 at 18:49):
I think @Xavier Roblot is mostly interested in changing the order of the arguments, atm
Mario Carneiro (Jan 31 2023 at 18:50):
are there specific arguments other than mathlib3 compatibility for the argument order one way or another?
Mario Carneiro (Jan 31 2023 at 18:51):
it would be nice to be consistent about this
Xavier Roblot (Jan 31 2023 at 18:54):
Well, I thought the compatibility with ‘eq’ could also be important since it is used in mathlib.
Ruben Van de Velde (Mar 24 2023 at 20:29):
I ran into this again and submitted https://github.com/leanprover-community/mathlib4/pull/3088
Last updated: Dec 20 2023 at 11:08 UTC