# Zulip Chat Archive

## 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