Stream: general

Topic: mysterious decidable_of_decidable_of_iff

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.

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.

Gabriel Ebner (Mar 01 2018 at 13:19):

rw decidable_of_decidable_of_iff_refl could work

Sean Leather (Mar 01 2018 at 13:19):

rw decidable_of_decidable_of_iff_refl _, apply_instance works

Gabriel Ebner (Mar 01 2018 at 13:19):

Have you tried congr on the original goal?

Ah, that works.

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

Sebastian Ullrich (Mar 01 2018 at 13:21):

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

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).

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