## Stream: new members

### Topic: two instances of decidable_eq are equal

#### Kenny Lau (Jun 21 2020 at 04:42):

example {α : Sort*} (h1 h2 : decidable_eq α) : h1 = h2 := sorry


#### Kenny Lau (Jun 21 2020 at 04:42):

rfl doesn't work here, and this is causing issues where two terms that are equal except for the decidable_eq terms cannot be unified (#xy)

#### Kenny Lau (Jun 21 2020 at 04:44):

obviously I can prove it like this:

example {α : Sort*} (h1 h2 : decidable_eq α) : h1 = h2 :=
funext $λ x, funext$ λ y, by cases h1 x y; cases h2 x y; cc


but this doesn't solve the unification issue

#### Kenny Lau (Jun 21 2020 at 04:47):

I guess another solution is to just remove decidable_eq from everything and use open_locale classical

#### Kenny Lau (Jun 21 2020 at 04:47):

but the problem is that I'm in a file where this hasn't been used

#### Kenny Lau (Jun 21 2020 at 04:48):

so using classical for new definitions only push the problem back one level at a time

#### Kenny Lau (Jun 21 2020 at 05:01):

constant foo : Π {α : Sort*}, decidable_eq α → ℕ

example {α : Sort*} (h1 h2 : decidable_eq α) : h1 = h2 := by congr -- fails
example {α : Sort*} (h1 h2 : decidable_eq α) : foo h1 = foo h2 := by congr -- works


#### Kenny Lau (Jun 21 2020 at 05:01):

I don't understand this

#### Kenny Lau (Jun 21 2020 at 05:03):

example {α : Sort*} (h1 h2 : decidable_eq α) : h1 = h2 := by congr --fails
example {α : Sort*} (h1 h2 : decidable_eq α) : id h1 = id h2 := by congr --works


#### Kenny Lau (Jun 21 2020 at 05:03):

@Mario Carneiro what's going on here?

#### Mario Carneiro (Jun 21 2020 at 05:07):

I think decidable_eq A should be a subsingleton

#### Kenny Lau (Jun 21 2020 at 05:08):

theorem test2 : ∀ {α : Sort u_1} (h1 h2 : decidable_eq α), id h1 = id h2 :=
λ {α : Sort u_1} (h1 h2 : decidable_eq α),
(λ (a a_1 : decidable_eq α),
((λ (a : decidable_eq α), eq.refl (id a)) a).trans (congr (eq.refl id) (subsingleton.elim a a_1)))
h1
h2


#### Mario Carneiro (Jun 21 2020 at 05:08):

This works:

variable (A : Type)
#check (by apply_instance : subsingleton (decidable_eq A))


#### Kenny Lau (Jun 21 2020 at 05:08):

yeah but for my usecase it just times out

#### Mario Carneiro (Jun 21 2020 at 05:09):

Apparently congr doesn't think to apply subsingleton.elim immediately, but it does apply it on subgoals

#### Kenny Lau (Jun 21 2020 at 05:09):

and convert fails:

import tactic
theorem test2 {α : Sort*} (h1 h2 : decidable_eq α) : id h1 = id h2 := by convert rfl --fails


#### Mario Carneiro (Jun 21 2020 at 05:09):

hence why id x = id y works

#### Mario Carneiro (Jun 21 2020 at 05:10):

I'm confused what the goal is here now

#### Mario Carneiro (Jun 21 2020 at 05:10):

two instances of decidable_eq are indeed equal, and the typeclass system knows this

#### Mario Carneiro (Jun 21 2020 at 05:10):

so where is the problem?

#### Kenny Lau (Jun 21 2020 at 05:12):

I can't produce an MWE yet, but it times out

#### Kenny Lau (Jun 21 2020 at 05:18):

ok I found a workaround

Last updated: May 06 2021 at 21:09 UTC