Zulip Chat Archive

Stream: new members

Topic: Counting occurrences without decidable_eq


Martin Dvořák (Nov 11 2022 at 14:57):

I have been using the following function for counting occurrences of an element in a list.

def count_in {α : Type*} [decidable_eq α] (l : list α) (a : α) :  :=
list.sum (list.map (λ s, ite (s = a) 1 0) l)

Is it possibly to write an equivalent function where decidable_eq is not needed? I don't want to execute the function; I want to use it in theorems, but now I don't have decidable_eq instance .

Yaël Dillies (Nov 11 2022 at 15:07):

Is this not just docs#list.count?

Eric Wieser (Nov 11 2022 at 15:11):

How could it be possible? What would count_in [a] b use as the algorithm to decide whether b appears in the list?

Eric Wieser (Nov 11 2022 at 15:14):

I want to use it in theorems

In statements of theorems or in proofs of theorems?

Martin Dvořák (Nov 11 2022 at 15:16):

I want to use it in proofs. Do I need [decidable_eq α] for the sake of claiming stuff like "if two lists have unequal number of 0s, they cannot be equal"?

Martin Dvořák (Nov 11 2022 at 15:18):

Yaël Dillies said:

Is this not just docs#list.count?

I swear I was searching for it with library_search but I didn't find it, so I reimplemented it myself.

Martin Dvořák (Nov 11 2022 at 15:20):

Eric Wieser said:

I want to use it in theorems

In statements of theorems or in proofs of theorems?

For example, I used it in my counterexample (proof) that the class of context-free languages is not closed under intersection:
https://github.com/madvorak/grammars/blob/main/src/context_free/closure_properties/binary/CF_intersection_CF.lean

Martin Dvořák (Nov 11 2022 at 15:21):

However, I want to use it for a more general datatype now.

Martin Dvořák (Nov 11 2022 at 15:23):

Yaël Dillies said:

Is this not just docs#list.count?

Would mathlib be interested in having lemmata for list.count too? I have several trivial observations (which were useful for me):
https://github.com/madvorak/grammars/blob/decbbe93874769b8e8bd0230813a77b7787538b9/src/list_utils.lean#L129

Yaël Dillies (Nov 11 2022 at 15:40):

Yes of course, but I think we have most of your lemmas already.

Martin Dvořák (Nov 11 2022 at 15:40):

Yaël Dillies said:

Yes of course, but I think we have most of your lemmas already.

Again, I failed to find them. How did you search for them?

Yaël Dillies (Nov 11 2022 at 15:42):

Did you have a look at file#data/list/count?

Yaël Dillies (Nov 11 2022 at 15:42):

docs#list.count_append

Martin Dvořák (Nov 11 2022 at 15:46):

Yaël Dillies said:

Did you have a look at file#data/list/count?

I didn't. My bad!

Eric Wieser (Nov 11 2022 at 15:49):

Martin Dvořák said:

I want to use it in proofs. Do I need [decidable_eq α] for the sake of claiming stuff like "if two lists have unequal number of 0s, they cannot be equal"?

Claims are statements not proofs. You do need that argument for such a claim, because what you're actually claiming is that that statement is true whatever your algorithm is for counting zeros.

Eric Wieser (Nov 11 2022 at 15:50):

If your "claim" only appears as a have line within your proof, then you can use tactic#classical to conjure a decidable_eq instance

Martin Dvořák (Nov 11 2022 at 16:29):

Did I get it right? Could you please tell me how to rewrite the following 17 lines in a way that is not so extremely awkward?
https://github.com/madvorak/grammars/blob/1737b1049868bb7d78bbc4241cbab9d7b1cf0ad2/src/unrestricted/closure_properties/unary/star_RE.lean#L169

Eric Wieser (Nov 11 2022 at 16:38):

I would guess that https://github.com/madvorak/grammars/blob/1737b1049868bb7d78bbc4241cbab9d7b1cf0ad2/src/unrestricted/closure_properties/unary/star_RE.lean#L169-L173 can be replaced by the tactic classical, by itself

Eric Wieser (Nov 11 2022 at 16:39):

You made things hard for yourself by using have rather than let or letI

Eric Wieser (Nov 11 2022 at 16:39):

Why don't you just make ns decidable_eq though?

Martin Dvořák (Nov 11 2022 at 16:49):

Eric Wieser said:

I would guess that https://github.com/madvorak/grammars/blob/1737b1049868bb7d78bbc4241cbab9d7b1cf0ad2/src/unrestricted/closure_properties/unary/star_RE.lean#L169-L173 can be replaced by the tactic classical, by itself

Thanks a lot!!

BTW, how do you quote a segment of code from GitHub? Did you edit the URL by hand?

Martin Dvořák (Nov 11 2022 at 16:53):

Eric Wieser said:

Why don't you just make ns decidable_eq though?

I don't think I can. The definition is essentially:

def ns (T N : Type) : Type :=
sum T (N  fin 3)

Even thought the three special values (one of which is abstracted as H) come from a decidable_eq type (and I use those values in my list.count_in juggling), I don't want to restrict what T and N are.

Yaël Dillies (Nov 11 2022 at 16:55):

If you have decidable_eq on T and N, then you have it on ns.

Martin Dvořák (Nov 11 2022 at 16:55):

Yaël Dillies said:

If you have decidable_eq on T and N, then you have it on ns.

I don't.

Eric Wieser (Nov 11 2022 at 17:33):

You could write the instance that has that implication anyway, and things might be slightly easier for you

Martin Dvořák (Nov 11 2022 at 17:34):

On which level should I write the instance? Inside a concrete proof?

Eric Wieser (Nov 11 2022 at 17:46):

Globally, with instance

Matt Diamond (Nov 11 2022 at 18:37):

how do you quote a segment of code from GitHub? Did you edit the URL by hand?

@Martin Dvořák it's pretty simple, here's how:

1) Click the line number you want to start from
2) Shift-click the line number you want to end at
3) Click the three-dot button and select "Copy permalink"


Last updated: Dec 20 2023 at 11:08 UTC