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: Dec 20 2023 at 11:08 UTC