Stream: new members

Topic: simp or term proof in library

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 ?

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]


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"

Reid Barton (Jul 21 2020 at 22:51):

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

Anatole Dedecker (Jul 21 2020 at 22:52):

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

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


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