Style question: iff, or both directions *and* iff

Stream: maths

[Patrick Stevens]

This is about https://github.com/leanprover-community/mathlib/pull/9815, which adds the lemma:

 lemma log_eq_zero {x : ℝ} (h : log x = 0) : x = 0 ∨ x = 1 ∨ x = -1 := by sorry

Mathlib convention is to phrase this as an iff instead. My question is: what would Mathlib say about providing this lemma as well as the iff version (where the iff version just cases and then calls out to log_eq_zero)? Or should I only give the iff version?

[Kyle Miller]

Having it be an iff means you can rewrite with it, which can be rather useful even if you never use its converse.

[Floris van Doorn]

We don't disallow giving the version in one direction, and if the easiest proof of the iff is to do each implication separately, it's very common to also have one or both of the implications. That said, naming the non-iff version is tricky; the current name does not follow our #naming conventions. (eq_or_eq_or_eq_of_log_eq_zero is quite long, but probably the "best" name)

[Ruben Van de Velde]

Or log_eq_zero and log_eq_zero_iff? I'd say it's mostly interesting to have a particular direction stated separately if you can then drop an assumption

[Kyle Miller]

The iff version is only a few lines longer:

lemma log_eq_zero {x : ℝ} : log x = 0 ↔ x = 0 ∨ x = 1 ∨ x = -1 :=
begin
  split,
  { intro h,
    rcases lt_trichotomy x 0 with x_lt_zero | rfl | x_gt_zero,
    { refine or.inr (or.inr (eq_neg_iff_eq_neg.mp _)),
      rw [←log_neg_eq_log x] at h,
      exact (eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h).symm, },
    { exact or.inl rfl },
    { exact or.inr (or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h)), } },
  { rintro (rfl|rfl|rfl); simp, },
end

[Patrick Stevens]

I decided it wasn't worth the bikeshed and just did exactly as Kyle demonstrated, thanks

[Patrick Stevens]

I recognised the naming conventions problem, but decided that three disjunctions in a name was too much :P

[Alex J. Best]

You can use the alias command to autogenerate the implications from an iff btw https://leanprover-community.github.io/mathlib_docs/tactic/alias.html