Counting occurrences without decidable_eq

Stream: new members

[Martin Dvořák]

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]

Is this not just docs#list.count?

[Eric Wieser]

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]

I want to use it in theorems

In statements of theorems or in proofs of theorems?

[Martin Dvořák]

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]

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]

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]

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

[Martin Dvořák]

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]

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

[Martin Dvořák]

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]

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

[Yaël Dillies]

docs#list.count_append

[Martin Dvořák]

Yaël Dillies said:

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

I didn't. My bad!

[Eric Wieser]

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]

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]

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]

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]

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

[Eric Wieser]

Why don't you just make ns decidable_eq though?

[Martin Dvořák]

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]

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]

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

[Martin Dvořák]

Yaël Dillies said:

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

I don't.

[Eric Wieser]

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

[Martin Dvořák]

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

[Eric Wieser]

Globally, with instance

[Matt Diamond]

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"