Zulip Chat Archive

Stream: general

Topic: mysterious decidable_of_decidable_of_iff


view this post on Zulip Sean Leather (Mar 01 2018 at 13:13):

This is also peculiar. I came upon the following which didn't resolve with refl or simp:

 ite (y = x) t₂ (varf y) = ite (y = x) t₂ (varf y)

Upon further inspection with set_option pp.all true, I found:

 @eq.{1} (tts.typ V)
    (@ite.{1} (@eq.{1} V y x)
      (_inst_1 y x)
      (tts.typ V)
      t₂
      (@tts.typ.varf V y))
    (@ite.{1} (@eq.{1} V y x)
      (@decidable_of_decidable_of_iff (@eq.{1} V y x) (@eq.{1} V y x) (_inst_1 y x) (iff.refl (@eq.{1} V y x)))
      (tts.typ V)
      t₂
      (@tts.typ.varf V y))

Of course, the goal can be reached with:

by_cases h : y = x; simp [h]

But what I'm curious about is (1) why it's there in the first place and (2) why it isn't resolved with refl (why is it not defeq?).

My guess for (1) is that it came from one of the congr theorems in library/init/logic.lean.

As for (2), I tried adding:

@[simp] theorem decidable_of_decidable_of_iff_refl :
   (d : decidable p), decidable_of_decidable_of_iff d (iff.refl p) = d
| (is_true _)  := rfl
| (is_false _) := rfl

and:

simp [decidable_of_decidable_of_iff_refl _]

but nothing changed, and decidable_of_decidable_of_iff_refl didn't show up with set_option trace.simplify true.

view this post on Zulip Gabriel Ebner (Mar 01 2018 at 13:19):

simp only allows you to rewrite at positions that you can "reach" via congruence lemmas. Since congruence lemmas typically skip subsingletons (such as decidability instances), you can't simp there.

view this post on Zulip Gabriel Ebner (Mar 01 2018 at 13:19):

rw decidable_of_decidable_of_iff_refl could work

view this post on Zulip Sean Leather (Mar 01 2018 at 13:19):

rw decidable_of_decidable_of_iff_refl _, apply_instance works

view this post on Zulip Gabriel Ebner (Mar 01 2018 at 13:19):

Have you tried congr on the original goal?

view this post on Zulip Sean Leather (Mar 01 2018 at 13:20):

Ah, that works.

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 13:20):

I suppose this shows that simp should really use refl as a rule instead of just at the very end

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 13:21):

Then it should be able to close that goal together with if_congr

view this post on Zulip Gabriel Ebner (Mar 01 2018 at 13:23):

@Sebastian Ullrich Can you elaborate on how refl would work here? Neither side of the equation can be simplified, not even with refl. AFAICT the only thing that would help is if simp applied the congruence lemmas to the equation (like backchaining).

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 13:28):

@Gabriel Ebner You're right, I was confused about the role of congr lemmas in simp


Last updated: May 12 2021 at 23:13 UTC