Iff translation

[JOSHCLUNE]

In transPropConst of Auto/IR/TPTP_TH0.lean, Lean's iff statements are translated to (^ [L : $o, R : $o] : L = R) to work around the fact that Zipperposition encounters parsing errors when it receives (<=>). Even though this ought to be equivalent as far as TH0's semantics are concerned, I've found that Zipperposition produces better results when Lean's iff statements are instead just translated to (=). Here are two examples of problems that auto fails to solve (with Zipperposition as a backend) currently, but succeeds in solving if Lean's iff is translated to (=):

set_option auto.smt false in
set_option auto.tptp true in
set_option trace.auto.tptp.printQuery true in
set_option trace.auto.tptp.result true in
set_option auto.native true in
example (t : Type) (f : t → t → t) (one : t)
  (h1 : ∀ x : t, (∀ y : t, f x y = y) → (x = one))
  (h2 : ∀ x : t, (x = one) → (∀ y : t, f x y = y))
  : ∀ x : t, (∀ y : t, f x y = y) ↔ (x = one) := by
  auto [*]

set_option auto.smt false in
set_option auto.tptp true in
set_option trace.auto.tptp.printQuery true in
set_option trace.auto.tptp.result true in
set_option auto.native true in
example (Inhab : Type) (A B C D : Inhab) (Sane Doctor : Inhab → Prop)
  (h1 : Sane A ↔ (Sane B ↔ Sane C))
  (h2 : Sane B ↔ (Sane A ↔ Sane D))
  (h3 : Sane C ↔ ¬ (Doctor C ∧ Doctor D))
  (h4 : A ≠ B ∧ A ≠ C ∧ A ≠ D ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D) :
  (∃ x : Inhab, Sane x ∧ ¬ Doctor x) ∨
  (∃ x : Inhab, ∃ y : Inhab, x ≠ y ∧ (¬ Sane x) ∧ Doctor x ∧ (¬ Sane y) ∧ Doctor y) := by
  auto [*]