Proof style

Stream: new members

[Anatole Dedecker]

Focusing on style, which of the following proof would be preferred, e.g for a contribution to mathlib ?

lemma exists_has_deriv_at_eq_zero' (f f' : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
  (hfa : tendsto f (nhds_within a $ Ioi a) (nhds l)) (hfb : tendsto f (nhds_within b $ Iio b) (nhds l))
  (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) :
  ∃ c ∈ Ioo a b, f' c = 0 :=
have ∃ c ∈ Ioo a b, is_local_extr (λ x, if x ≤ a then l else if b ≤ x then l else f x) c, from
  exists_local_extr_Ioo
    (λ x, if x ≤ a then l else if b ≤ x then l else f x)
    hab
    ( continuous_on_Icc_of_extend_continuous_Ioo hab
      ( λ x hx, (hff' x hx).continuous_at.continuous_within_at )
      hfa hfb )
    ( by simp only [le_refl, if_true, if_t_t] ),
let ⟨c, hc, hcextr⟩ := this in
  have heq : (λ (x : ℝ), ite (x ≤ a) l (ite (b ≤ x) l (f x))) =ᶠ[𝓝 c] f :=
    eventually_eq_iff_exists_mem.mpr
    ⟨ Ioo a b,
      Ioo_mem_nhds hc.1 hc.2,
      λ x hx, by simp only [not_le_of_lt hx.1, not_le_of_lt hx.2, if_false] ⟩,
  ⟨c, hc, ( hcextr.congr heq ).has_deriv_at_eq_zero $ hff' c hc ⟩

lemma exists_has_deriv_at_eq_zero'' (f f' : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
  (hfa : tendsto f (nhds_within a $ Ioi a) (nhds l)) (hfb : tendsto f (nhds_within b $ Iio b) (nhds l))
  (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) :
  ∃ c ∈ Ioo a b, f' c = 0 :=
begin
  have := exists_local_extr_Ioo
    (λ x, if x ≤ a then l else if b ≤ x then l else f x)
    hab
    ( continuous_on_Icc_of_extend_continuous_Ioo hab
      ( λ x hx, (hff' x hx).continuous_at.continuous_within_at )
      hfa hfb )
    (by simp only [le_refl, if_true, if_t_t]),
  rcases this with ⟨c, hc, hcextr⟩,
  use c, use hc,
  apply ( hcextr.congr _ ).has_deriv_at_eq_zero (hff' c hc),
  apply eventually_eq_iff_exists_mem.mpr,
  use Ioo a b,
  use Ioo_mem_nhds hc.1 hc.2,
  exact λ x hx, by simp only [not_le_of_lt hx.1, not_le_of_lt hx.2, if_false],
end

[Pedro Minicz]

I know its a bit off topic, but I prefer the tactic mode proof, as I find it more legible. Looking at mathlib, it seems to have a fair share of both styles, although I have never seen a long tactic mode proof there (there are long term mode proofs, which is a bit unfortunate, again, because of my readability preferences).

[Anatole Dedecker]

I agree that tactic proofs are much easier to read if you have lean turned-on to see the tactic state. But if you have to read them as pure text, I honestly don't know which one is more readable

[Patrick Massot]

Anatole, you can write tactic proofs that are as readable as pure text as what you can get in term mode. You only need to put more type annotation to have or use obtain instead of rcases.

[Patrick Massot]

For instance you can hopefully start the above proof with:

obtain ⟨c, hc, hcextr⟩ :
    ∃ c ∈ Ioo a b, is_local_extr (λ x, if x ≤ a then l else if b ≤ x then l else f x) c,

[Anatole Dedecker]

That's way better indeed

[Scott Morrison]

I prefer the tactic style for readability/maintainability. Even better is a tactic style proof interspersed with comments!

[Yury G. Kudryashov]

BTW, we have src#has_deriv_at_of_has_deriv_at_of_ne
Possibly it should be modified to require ∀ᶠ y in nhds_within x {y | y ≠ x}, has_deriv_at f (g y) y instead of ∀....