# Zulip Chat Archive

## 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?

#### Sean Leather (Mar 01 2018 at 13:20):

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