Zulip Chat Archive

Stream: new members

Topic: simp or term proof in library


view this post on Zulip Anatole Dedecker (Jul 21 2020 at 22:20):

When writing lemmas for the library, should we prefer a one-line simp proof (squeezified if necessary) or a few lines of term proof ? I know the term way is probably the fastest, but maybe there are other citerions to choose ?

view this post on Zulip Anatole Dedecker (Jul 21 2020 at 22:30):

Example : which should I choose here ?

import order.filter.basic

open filter
open_locale filter

lemma tendsto_sup {α β : Type*} (F G : filter α) (l : filter β) (f : α  β) :
  (tendsto f (F  G) l  tendsto f F l  tendsto f G l) :=
 λ h,
   tendsto_def.2 (λ s, λ hs, (mem_sup_sets.1 $ tendsto_def.1 h s hs).1),
    tendsto_def.2 (λ s, λ hs, (mem_sup_sets.1 $ tendsto_def.1 h s hs).2) ,
  λ  h1, h2 , tendsto_def.2 $ λ s, λ hs, mem_sup_sets.2  h1 hs, h2 hs  

lemma tendsto_sup' {α β : Type*} (F G : filter α) (l : filter β) (f : α  β) :
  (tendsto f (F  G) l  tendsto f F l  tendsto f G l) :=
by simp only [tendsto, map_sup, sup_le_iff]

view this post on Zulip Scott Morrison (Jul 21 2020 at 22:41):

I read these two proofs as:

  1. "err... I guess I'm going to have to remember exactly how we've defined tendsto in the library before I understand this"
  2. "the statement looks sensible, and apparently it follows easily from stuff we've already done, so lets keep going"

view this post on Zulip Reid Barton (Jul 21 2020 at 22:51):

There are also better term-mode proofs--not necessarily better than the by simp proof though.

view this post on Zulip Anatole Dedecker (Jul 21 2020 at 22:52):

I'm not really good at term mode yet :sweat_smile:

view this post on Zulip Reid Barton (Jul 21 2020 at 22:55):

apparently map_sup turns out to be a definitional equality, so one possibility is

lemma tendsto_sup {α β : Type*} (F G : filter α) (l : filter β) (f : α  β) :
  (tendsto f (F  G) l  tendsto f F l  tendsto f G l) :=
@sup_le_iff _ _ (F.map f) (G.map f) _

view this post on Zulip Reid Barton (Jul 21 2020 at 22:55):

or you can also help out Lean with show


Last updated: May 10 2021 at 17:39 UTC