Zulip Chat Archive

Stream: new members

Topic: Proof style


view this post on Zulip Anatole Dedecker (Jul 28 2020 at 21:56):

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

view this post on Zulip Pedro Minicz (Jul 28 2020 at 22:02):

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).

view this post on Zulip Anatole Dedecker (Jul 28 2020 at 22:05):

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

view this post on Zulip Patrick Massot (Jul 28 2020 at 22:18):

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.

view this post on Zulip Patrick Massot (Jul 28 2020 at 22:21):

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,

view this post on Zulip Anatole Dedecker (Jul 28 2020 at 22:23):

That's way better indeed

view this post on Zulip Scott Morrison (Jul 28 2020 at 22:50):

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

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 05:45):

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 ∀....


Last updated: May 14 2021 at 21:11 UTC