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:

  1. Leave the definitions of List.count and Multiset.count as they are and just fix proofs as we do the porting
  2. Fix only the definition of Multiset.count and use some auxiliary result to show that List.count and Multiset.count agree
  3. Fix the definitions of both List.count and Multiset.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