BEq instance for sigma

Stream: Is there code for X?

[Adam Topaz]

I'm surprised that I couldn't find the following:

instance {α : Type} [BEq α] [LawfulBEq α] {β : α → Type} [∀ a, BEq (β a)] :
    BEq ((a : α) × β a) where
  beq := fun ⟨a,b⟩ ⟨a',b'⟩ =>
    match h : a == a' with
      | true =>
        match eq_of_beq h with
          | rfl => b == b'
      | false => false

Do we really not have this in mathlib (or even std)?

[Ruben Van de Velde]

Do we have anything about BEq in mathlib?

[Adam Topaz]

maybe not. but std does, right?

[Adam Topaz]

OTOH, mathlib does have some programmy things about Sigma like docs#Sigma.instDecidableEqSigma

[Eric Wieser]

I thought we were still waiting for a solution to the decidable/BEq diamonds before adopting BEq anywhere in mathlib

[Adam Topaz]

BTW, I'm getting some motive is not type correct issues trying to prove the following sorry:

instance {α : Type} [BEq α] [LawfulBEq α] {β : α → Type} [∀ a, BEq (β a)] :
    BEq ((a : α) × β a) where
  beq := fun ⟨a,b⟩ ⟨a',b'⟩ =>
    match h : a == a' with
      | true =>
        match eq_of_beq h with
          | rfl => b == b'
      | false => false

instance {α : Type} [BEq α] [LawfulBEq α]
    {β : α → Type} [∀ a, BEq (β a)]
    [∀ a, LawfulBEq (β a)] :
    LawfulBEq ((a : α) × β a) := sorry

Does anyone see a slick way to prove this?

[Kyle Miller]

It's not pretty, but here's a proof:

instance {α : Type} [BEq α] [LawfulBEq α]
    {β : α → Type} [∀ a, BEq (β a)]
    [∀ a, LawfulBEq (β a)] :
    LawfulBEq ((a : α) × β a) where
  rfl := by intro ⟨a, b⟩; unfold_projs; simp; split; rfl; rename_i h; simp at h
  eq_of_beq := @fun ⟨a, b⟩ ⟨a', b'⟩ => by
    unfold_projs
    simp
    split
    · split
      subst_vars
      simp
    · simp

[Yury G. Kudryashov]

Can we teach simp to simplify match?

[Kyle Miller]

Here's another definition:

instance {α : Type} [BEq α] [LawfulBEq α] {β : α → Type} [∀ a, BEq (β a)] :
    BEq ((a : α) × β a) where
  beq
  | ⟨a, b⟩, ⟨a', b'⟩ => if h : a == a' then (eq_of_beq h ▸ b) == b' else false

instance {α : Type} [BEq α] [LawfulBEq α]
    {β : α → Type} [∀ a, BEq (β a)]
    [∀ a, LawfulBEq (β a)] :
    LawfulBEq ((a : α) × β a) where
  rfl := by intro ⟨a, b⟩; unfold_projs; simp
  eq_of_beq := @fun ⟨a, b⟩ ⟨a', b'⟩ => by
    unfold_projs
    simp
    split
    · rename_i h
      simp at h
      subst_vars
      simp
    · simp

[Adam Topaz]

Thanks Kyle!