BEq Subtype

Stream: lean4

[Marcus Rossel]

Along the lines of Hashable Subtype, does anyone see any problems with this?:

instance [BEq α] {p : α → Prop} : BEq { a : α // p a } where
  beq a₁ a₂ := BEq.beq a₁.val a₂.val

[Jannis Limperg]

(wrong topic, sorry)

[Gabriel Ebner]

The only issue I see is the potential diamond with these instances:

instance [DecidableEq α] : BEq α
instance {p : α → Prop} [DecidableEq α] : DecidableEq { a // p a }

[Mario Carneiro]

ugh, that seems like something we are going to have to deal with eventually by adding beq as a field in DecidableEq

[Mario Carneiro]

either that or don't have the [DecidableEq α] : BEq α instance

[Gabriel Ebner]

Dropping this instance is painful. Everything uses BEq these days, List.contains, Array.indexOf?, you name it.

[Mario Carneiro]

I guess we want DecidableEq to just be the same as LawfulBEq then

[Gabriel Ebner]

Bingo! And we can also drop all of the compiler hacks that identify Decidable and Bool under the hood.

[Mario Carneiro]

Well, we still need that for other decidable things

[Gabriel Ebner]

Well, obviously Decidable should be defined like this as well:

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

[Mario Carneiro]

Oh, also with a slight change to the equality instance for bool we could make example (b : Bool) : decide b = b := rfl work

[Gabriel Ebner]

Or with a change to the Bool-to-Prop coercion (coercing to true = b instead of b = true). I like the approach that Sebastian brought forward a while back of having a Bool.toProp function (forgot about the details), which would mostly hide this implementation detail (of which way the equation is oriented).

[Mario Carneiro]

b = true is good for rewrites though

[Mario Carneiro]

Bool.toProp would be more in line with the lean 3 way I think

[Gabriel Ebner]

Although it's really awful for pretty-printing. We don't want to show all b = true terms as ↑ b or even b. But we could unconditionally hide Bool.toProp b.

[Mario Carneiro]

heh, this will break some recent simp lemmas I wrote that use b instead of b = true

[Mario Carneiro]

well, maybe not if it's reducible

[Gabriel Ebner]

Either reducible, or with an extra simp lemma b → b = true.

[Mario Carneiro]

the second option wouldn't work if your simp lemma itself is of type @[simp] theorem foo : toProp ... := ...

[Mario Carneiro]

but I'm also okay with declaring these as illegal simp lemmas and require writing them as b = true

[Gabriel Ebner]

simp only [foo, eq_true_of_toProp] would still work. The extra lemma is conditional.

[Gabriel Ebner]

Oh, and looping..