imp_iff_self_imp

Stream: Is there code for X?

[Kim Morrison]

I can't seem to find

theorem imp_iff_self_imp : ((P → Q) ↔ (P → R)) ↔ (P → (Q ↔ R)) :=
  { mp := fun h p => { mp := fun q => h.mp (fun _ => q) p, mpr := fun r => h.mpr (fun _ => r) p },
    mpr := fun h => { mp := fun h' p => (h p).mp (h' p), mpr := fun h' p => (h p).mpr (h' p) } }

Is it hiding somewhere? What should it be called?

[Yaël Dillies]

I was expecting it to be imp_congr_right_iff but that doesn't exist

[Daniel Weber]

Why do aesop and tauto fail to prove it?

[Kevin Buzzard]

It's tauto's job to prove it so if tauto doesn't prove it, that's surely a bug?

[Daniel Weber]

Ah, it fails because autoimplicit makes P a Sort u

[Kevin Buzzard]

Autoimplicit is such an interesting thing. 9 times out of 10 it's cool and useful and then one time out of 10 it can be totally catastrophic, wasting people's time and energy

[Kim Morrison]

(In this case, I think autoimplicit is doing the right thing. It would be silly to prove this result only for Prop. :-)

[Kevin Buzzard]

I was misled by the notation :-) but you do have a good point here!

[Daniel Weber]

This is still true if one of Q or R is dependent, right? Maybe that exists?