instBEqNat = instBEq := rfl --fails

Stream: lean4

[Johan Commelin]

src4#instBEq src4#instBEqNat are both in Init/Prelude and don't seem to be defeq. Is that intentional, or should it be fixed?

example : instBEqNat = instBEq := rfl --fails

See also https://github.com/leanprover-community/mathlib4/pull/1479/files/21bb12498a3bda1e0c3f2045eb3d62e2d25e6f9f..132baa12e953e9c29bffae5953881ac115ef2fb0#r1066580684

[Sebastian Ullrich]

It does look intentional: https://github.com/leanprover/lean4/commit/da55789c26d7e6030927eb0815796f93c8fa8f50

[Johan Commelin]

Hmm, so do you have a recommendation for the issue I linked to?

[Johan Commelin]

Should we just pass the instance around explicitly, in cases like this?

[Sebastian Ullrich]

I'm not sure. Note that with instBEq you lose the accelerated kernel reduction, which I think is the whole reason for this particular setup

[Sebastian Ullrich]

Why do the used lemmas demand instBEq? It would be nicer if they merely demanded LawfulBEq.

[Johan Commelin]

I guess it's just the instance that TC found...

[Gabriel Ebner]

We've been talking about making Decidable extend BEq in core, which would fix this diamond.

[Gabriel Ebner]

I wanted to wait with this change until after the port, because I expect some (easily fixable) breakage in mathlib. (For example, cases h with h : Decidable p would no longer be the moral equivalent of by_cases p).

[Yury G. Kudryashov]

Do you mean something like this (not tested)?

class Decidable (p : Prop) :=
(decide : Bool)
(decide_iff : decide ↔ p)

With this definition, will we still need BEq?

[Chris Hughes]

The difficulty is that Lean is supposed to be a programming language to also be used by people who have no interest in proof and those people probably never want to see Prop at all.

[Mario Carneiro]

Importantly, Decidable can't replace BEq because a BEq is not necessarily lawful. Gabriel's proposal can eliminate LawfulBEq however, making it equivalent to DecidableEq.

[Yury G. Kudryashov]

With this definition we can have

class DecidableEq (α : Type*) extends BEq α :=
  (beq_iff_eq : ∀ x y : α, x == y ↔ x = y)

instance [DecidableEq α] {x y : α} : Decidable (x = y) where
  decide := x == y
  decide_iff := DecidableEq.beq_iff_eq x y

[Mario Carneiro]

right

[Mario Carneiro]

that's what Gabriel's PR lean4#2038 implements

[Kevin Buzzard]

Someone else just independently discovered this issue (and mentioned it to me on the Discord). The idea was to wait until after the port -- is that now?