Replace ↔ with =

Stream: lean4

[Marcus Rossel]

Is there a nice way to take a given theorem and replace all occurrences of ↔ in the theorem statement with = and fix the proof accordingly? For example, say we know:

theorem t : (0 = 1) ↔ (True ↔ False) :=
  Iff.intro
    (Nat.zero_ne_one.elim · |>.elim)
    (true_iff_false.mp · |>.elim)

Then is there an easy way to generate a proof of (0 = 1) = (True = False)?

[Yakov Pechersky]

docs#iff_eq_eq

[Marcus Rossel]

That won't suffice, as I do not only want to replace top-level ↔s.

[Damiano Testa]

Any translation of a proof to an "equivalent but not identical" proof is bound to be tricky along the edges.

[Yakov Pechersky]

So simp_rw [iff_eq_eq]?

[Yakov Pechersky]

Or if you're saying you already have a related proof, simpa?

[Damiano Testa]

You can scan the expression for the proof, replacing the iff with equalities, prepended by the application of the lemma that Yakov pointed out, but I think that it will be a little painful to get it to work in a robust manner.

[Marcus Rossel]

@Damiano Testa What are your concerns wrt robustness? I was hoping I could traverse the proof term and for every subterm whose type contains a ↔, traverse to the subterm which constructs the ↔ and apply propext to it.

[Damiano Testa]

My concerns are not specific to this situation, but generic: any translation proof --> proof that I tried, not matter how trivial it looked without being the identity, met some resistance somewhere.

[Marcus Rossel]

@Yakov Pechersky Just from trying a handful of examples even simp only seems to do the job.

[Marcus Rossel]

Well, until dependent type stuff enters the game:

def g (q : Prop) : Type := sorry
def f (p : Prop) : g p := sorry
theorem t : f (True = True) = f False := sorry

example : f (True ↔ True) = f False := by
  simp only [t, iff_eq_eq] -- fails

[Damiano Testa]

... enter the edge cases.

[Yakov Pechersky]

Have you tried simpa [iff_eq_eq] using t

[Junyan Xu]

rw [iff_eq_eq, t] actually works here. I've noticed more cases where simp is less powerful than rw recently, most recently here.