Zulip Chat Archive

Stream: new members

Topic: two instances of decidable_eq are equal


view this post on Zulip Kenny Lau (Jun 21 2020 at 04:42):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 21 2020 at 04:47):

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

view this post on Zulip Kenny Lau (Jun 21 2020 at 04:48):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 21 2020 at 05:01):

I don't understand this

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 21 2020 at 05:03):

@Mario Carneiro what's going on here?

view this post on Zulip Mario Carneiro (Jun 21 2020 at 05:07):

I think decidable_eq A should be a subsingleton

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 21 2020 at 05:08):

This works:

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

view this post on Zulip Kenny Lau (Jun 21 2020 at 05:08):

yeah but for my usecase it just times out

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 21 2020 at 05:09):

hence why id x = id y works

view this post on Zulip Mario Carneiro (Jun 21 2020 at 05:10):

I'm confused what the goal is here now

view this post on Zulip Mario Carneiro (Jun 21 2020 at 05:10):

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

view this post on Zulip Mario Carneiro (Jun 21 2020 at 05:10):

so where is the problem?

view this post on Zulip Kenny Lau (Jun 21 2020 at 05:12):

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

view this post on Zulip Kenny Lau (Jun 21 2020 at 05:18):

ok I found a workaround


Last updated: May 06 2021 at 21:09 UTC