Boolean equality on nat mismatch

Stream: lean4

[Bhavik Mehta]

import Std.Data.List.Count

example (n : Nat) (l : List Nat) (h : l.count n = 1) : n ∈ l := by
  rw [←List.count_pos_iff_mem]
  rw [h]

Why does the second rw fail here? I'd expect the two BEq instances on Nat here to be the same

[Mauricio Collares]

Related: https://github.com/leanprover/lean4/pull/2041 https://github.com/leanprover/lean4/pull/2038

[Bhavik Mehta]

Ah thanks for those references. Would be great to see progress on this

[Bhavik Mehta]

The fact that this rewrite fails seems undesirable:

import Std.Data.List.Count

example (n : Nat) (l : List Nat) (h : l.count n = 1) : n ∈ l := by
  rw [←List.count_pos_iff_mem]
  rw [h]

This came up in LftCM, and I thought I reported it earlier but I can't find it anywhere now, so I'm making a new thread.

[Bhavik Mehta]

Oops - found the thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Boolean.20equality.20on.20nat.20mismatch. Doesn't seem to have much progress since January though, unfortunately...

[Eric Wieser]

Should we merge the threads?

[Eric Wieser]

attribute [-instance] instBEqNat is a workaround for your issue

[Notification Bot]

4 messages were moved here from #lean4 > DecidableEq Nat mismatch by Eric Wieser.