mysterious decidable_of_decidable_of_iff

Stream: general

[Sean Leather]

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]

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]

rw decidable_of_decidable_of_iff_refl could work

[Sean Leather]

rw decidable_of_decidable_of_iff_refl _, apply_instance works

[Gabriel Ebner]

Have you tried congr on the original goal?

[Sean Leather]

Ah, that works.

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Gabriel Ebner]

@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]

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