## Stream: new members

### Topic: cleaning up this tactic proof (regarding closures)

#### Kevin Doran (Mar 31 2020 at 02:17):

I've got most of the way through the following proof; however, I'm stuck at one section (Q6). In addition, I was wondering if you could help me clean up the existing code. (live in web editor: https://tinyurl.com/upkybhm). Any help greatly appreciated.

import data.real.basic
import data.set
import analysis.normed_space.basic

-- Q0. Notation for absolute. Should I reuse this from somewhere in Lean or mathlib?
local notation |x| := abs x

@[reducible]
def is_adherent (x : ℝ) (X : set ℝ) : Prop :=
∀ ε > 0, ∃y ∈ X, |x - y| ≤ ε

infix is_adherent_to :55 := is_adherent

@[reducible]
def closure(X : set ℝ) : set ℝ :=
{x : ℝ | x is_adherent_to X }

lemma closure_squeeze
(X Y : set ℝ)
(h₁ : X ⊆ Y)
(h₂ : Y ⊆ closure(X)) :
closure(X) = closure(Y) :=
begin
-- Q1. Should all unfolds be removed when finished? Are they superfluous?
--unfold closure,
apply set.eq_of_subset_of_subset,
{
intro x,
-- Q2. intro vs. assume, which is preferred? assume has the benefit of optionally being
-- explicit in what is being introduced.
assume h₃ : x ∈ closure(X),
intro ε,
assume hε : ε > 0,
have h₄ : x is_adherent_to X, from h₃,
have h₅ : ∃x' ∈ X, |x-x'| ≤ ε, from h₃ ε hε,
apply exists.elim h₅,
intros x' h_exists_temp,
apply exists.elim h_exists_temp,
intros h₆ h₇,
have h₈ : x' ∈ Y, from h₁ h₆,
use x',
exact and.intro h₈ h₇
},
{
intro y,
assume h₃ : y ∈ closure(Y),
intro ε,
assume hε : ε > 0,
-- Q3. What is a better way to get a δ = ε/3? It takes...
have h₄ : ∃δ : ℝ, δ = ε/3, from exists_eq,
apply exists.elim h₄,
intro δ,
assume hδ : δ = ε/3,
-- ... me 4 lines.
-- Q4. What is the proof for h₅ exactly? library_search doesn't turn up anything.
have h₅ : δ > 0, by linarith,
have h₆ : ∃y' ∈ Y, |y - y'| ≤ δ, from h₃ δ h₅,
-- Q5. Is there a better way to access the two proofs (hy' and h₇)? It takes ...
apply exists.elim h₆,
intro y',
intro temp,
apply exists.elim temp,
assume hy' : y' ∈ Y,
assume h₇ : |y - y'| ≤ δ,
--- ... me 6 lines.
have h₈ : y' ∈ closure(X), from h₂ hy',
-- This next bit is a repeat of Q5..
have h₉ : ∃x ∈ X, |y' - x| ≤ δ, from h₈ δ h₅,
apply exists.elim h₉,
intro x,
intro temp,
apply exists.elim temp,
assume hx : x ∈ X,
assume h₁₀ : |y' - x| ≤ δ,
-- ... another 6 lines.
-- Q6. I'm a bit stuck on the following line. I think, what is needed is something like:
--    norm_add_le_of_le (by apply_instance) h₇ h₁₀,
have h₁₁ : |y - x| ≤ 2*δ, from sorry,
have h₁₂ : |y - x| ≤ ε, by linarith,
use x,
exact and.intro hx h₁₂
}
end


#### Kevin Buzzard (Mar 31 2020 at 07:22):

Which version of mathlib are you using? I get an error

invalid definition, a declaration named 'closure' has already been declared


on line 15, and #check @closure gives me

closure : Π {α : Type u_1} [_inst_1 : topological_space α], set α → set α


#### Yury G. Kudryashov (Mar 31 2020 at 07:38):

Yes, we have closure defined for any topological space, not just real numbers.

#### Kevin Buzzard (Mar 31 2020 at 07:53):

Changing closure to closure' throughout the snippet fixes it.

norm_add_le_of_le is a theorem about normed groups. I don't know much about what structures are put on the real numbers, but if I write have ZZZ := norm_add_le_of_le h₇ h₁₀, just before your sorry then the error seems to indicate that nobody has put a normed group structure on the reals with the norm being abs, or perhaps you have not imported the file where this structure is defined.

#### Kevin Buzzard (Mar 31 2020 at 07:55):

What you need is abs_add I guess.

#### Yury G. Kudryashov (Mar 31 2020 at 07:57):

This structure is defined in normed_space.basic

#### Kevin Buzzard (Mar 31 2020 at 07:57):

but I guess you can persuade linarith to do this:

    have h₁₁ : |y - x| ≤ 2*δ,
rw (show y - x = (y - y') + (y' - x), by ring),
linarith,


#### Yury G. Kudryashov (Mar 31 2020 at 07:59):

Actually it fails because for Lean (a - b) + (b - c) is not the same as a - c

#### Yury G. Kudryashov (Mar 31 2020 at 08:01):

So, you need to either rewrite as @Kevin Buzzard suggested, or use dist instead of |a - b|.

#### Kevin Buzzard (Mar 31 2020 at 08:04):

In terms of structure, I would not embark upon a big monolithic proof like this. Why is your result true? Here is a proof which only uses fundamental facts about closures. Firstly there is closure_mono, the fact that closure is monotonic, which is a fancy way of saying that if $X\subseteq Y$ then $\overline{X}\subseteq\overline{Y}$. Applying this to $h_1$ shows $\overline{X}\subseteq\overline{Y}$ and applying it to $h_2$ shows $\overline{Y}\subseteq$closure(closure(X))Secondly there is closure_closure, saying closure (closure X)=closure X. Applying these two facts shows inclusions in both ways so you're done. This means that the actual proof of closure_squeeze should be three lines long, deducing the result from these more fundamental results, whose proofs would obviously be where more of the work is. But you should try and make your proofs as modular as possible. Note that I used closure_mono twice in my argument above, and it would not surprise me if in some sense you prove it twice in your argument, meaning that your proof might be much longer than it should be.

#### Kevin Doran (Mar 31 2020 at 08:43):

Apologies, I did not include a namespace in my snippet.

@Kevin Buzzard , thanks for the rw tip! Regarding the monolithic proof, my intention is to follow a textbook, and those closure properties you mention are later proved using this one.

#### Kevin Doran (Mar 31 2020 at 08:44):

Any thoughts on improving the section:

    -- Q3. What is a better way to get a δ = ε/3? It takes...
have h₄ : ∃δ : ℝ, δ = ε/3, from exists_eq,
apply exists.elim h₄,
intro δ,
assume hδ : δ = ε/3,
-- ... me 4 lines.


#### Kevin Buzzard (Mar 31 2020 at 08:52):

Kevin Doran said:

Regarding the monolithic proof, my intention is to follow a textbook, and those closure properties you mention are later proved using this one.

Having spent some time reading mathlib, I would now definitely question whether mathematicians always know best when it comes to ordering of material. You might be right though, I have not thought about how to develop this sort of theory (I probably should, there has been some real number game action recently)

#### Kevin Buzzard (Mar 31 2020 at 08:53):

Chris Hughes pointed out to me that his 2nd year analysis lecturer proved the same result three times over the course of two lectures, as sublemmas or remarks in the middle of other proofs.

#### Kevin Buzzard (Mar 31 2020 at 08:54):

set δ := ε/3 with hδ, is the way to do the delta thing perhaps.

#### Kevin Doran (Mar 31 2020 at 09:03):

I think, no matter which way you choose, at least one of them will require a delta-epsilon formulation, which is where most of my mess above comes from.

The other big eye sore is the double exist-elim:

    -- Q5. Is there a better way to access the two proofs (hy' and h₇)? It takes ...
apply exists.elim h₆,
intro y',
intro temp,
apply exists.elim temp,
assume hy' : y' ∈ Y,
assume h₇ : |y - y'| ≤ δ,
--- ... me 6 lines.


This seems like such a common pattern (working with an proposition, ∃x ∈ X, <something>). Any thoughts on a better way?

#### Kevin Buzzard (Mar 31 2020 at 09:08):

Oh sorry -- I have only just noticed all the questions!

#### Kevin Doran (Mar 31 2020 at 09:10):

Also, I would love a real number game.

#### Kevin Buzzard (Mar 31 2020 at 09:10):

Q1 yeah I'd not bother unfolding. Q2 intro is much more common. Just above Q3: you can just do intros eps heps.

#### Kevin Buzzard (Mar 31 2020 at 09:11):

Q4 the proof is linarith. Maybe there is some result of the form a>0 and b>0 -> a/b>0 but then you'll still need to prove 3>0 (which you can do with norm_num)

#### Kevin Buzzard (Mar 31 2020 at 09:12):

Q5  rcases h₆ with ⟨y', hy', h₇⟩,

#### Kevin Buzzard (Mar 31 2020 at 09:13):

Hopefully that's everything! rcases is a brilliant tactic for this sort of proof.

#### Kevin Doran (Mar 31 2020 at 09:14):

Thanks a million!

#### Kevin Buzzard (Mar 31 2020 at 09:16):

I think closure_mono is very simple to prove by the way. I think it's just a set-theoretic triviality

#### Kevin Buzzard (Mar 31 2020 at 09:17):

The same is true for closure_closure

#### Kevin Buzzard (Mar 31 2020 at 09:17):

It's just a 2epsilon proof

#### Patrick Massot (Mar 31 2020 at 09:31):

Can I vote twice for proving closure_mono first?

#### Patrick Massot (Mar 31 2020 at 09:33):

Everything Kevin wrote about distrusting lecture notes for this kind of things is crucial.

#### Kevin Doran (Mar 31 2020 at 09:45):

To try and argue the position of the author, closure_mono is fine to be proven first, no debate there. The main point of contention is betweenclosure_closure, closure_union or the the above lemma; all follow easily from each other. So far, the author's presentation order has been illuminating.

#### Patrick Massot (Mar 31 2020 at 09:46):

I also think it's worth having a look at mathlib, even if the setup is hugely more general. This is the sequence of lemmas you are interested in. You don't need to understand the proofs, only notice how shorts are the proofs because of the careful ordering of statements.

#### Kevin Doran (Mar 31 2020 at 09:47):

Oh, yea, that's a great spot to study. I went looking before, but I got a bit lost.

#### Kevin Buzzard (Mar 31 2020 at 09:59):

@Kevin Doran do you see how natural the proof below is?

lemma closure'_mono {X Y : set ℝ} (hXY : X ⊆ Y) : closure' X ⊆ closure' Y :=
--λ a haX ε hε, ⟨_, hXY haX, _⟩ #exit
--⟨(haX ε hε).1 _⟩
begin
-- Say a is in the closure of X. We want to show a is in the closure of Y.
-- So say ε > 0. We want to find y ∈ Y such that |a - y| ≤ ε.
intros a haX ε hε,
-- By definition of closure of X, there's x ∈ X with |a - x| ≤ ε.
rcases haX ε hε with ⟨x, haX', h⟩,
-- So let y be x.
use x,
-- Remark:
split,
{ -- x is in Y because it's in X and X ⊆ Y
exact hXY haX', -- hXY is actually a function!
},
-- oh but now one of our assumptions is the conclusion
assumption
end


#### Kevin Buzzard (Mar 31 2020 at 10:00):

lemma closure'_mono {X Y : set ℝ} (hXY : X ⊆ Y) : closure' X ⊆ closure' Y :=
λ a haX ε hε, ⟨_, _⟩


Can you write the proof in term mode?

#### Kevin Buzzard (Mar 31 2020 at 10:00):

The only tactics this proof uses are trivialities.

#### Kevin Buzzard (Mar 31 2020 at 10:02):

Monotonocity is a really natural thing to look for -- we are saying monotonicity is a morphism of posets.

#### Kevin Buzzard (Mar 31 2020 at 10:02):

The squeeze lemma you are trying to prove has a much uglier statement.

#### Kevin Buzzard (Mar 31 2020 at 10:02):

Formalising reveals an underlying elegance which humans often miss.

#### Kevin Buzzard (Mar 31 2020 at 10:04):

closure_closure is the statement that a morphism is idempotent. This is also a much more natural statement than the squeeze lemma.

#### Patrick Massot (Mar 31 2020 at 10:08):

Why do you tag all your definitions as reducible?

#### Patrick Massot (Mar 31 2020 at 10:08):

This is very rarely a good idea, and should certainly not be used when you don't understand what it means.

#### Kevin Doran (Mar 31 2020 at 10:12):

@Kevin Buzzard, that is far more elegant!

Also agreed that the squeeze statement is pretty ugly in itself.

@Patrick Massot , ah I forgot to take that out. I was just playing with the feature to see what it does.

#### Kevin Buzzard (Mar 31 2020 at 10:16):

It is kind of annoying that #print closure'_mono gives a term

theorem closure'_mono : ∀ {X Y : set ℝ}, X ⊆ Y → closure' X ⊆ closure' Y :=
λ {X Y : set ℝ} (hXY : X ⊆ Y),
id
(λ (a : ℝ) (haX : a ∈ closure' X),
id
(λ (ε : ℝ) (hε : ε > 0),
Exists.dcases_on (haX ε hε)
(λ (x : ℝ) (h : ∃ (H : x ∈ X), |a - x| ≤ ε),
Exists.dcases_on h
(λ (haX' : x ∈ X) (h : |a - x| ≤ ε),
Exists.intro x (id (exists_prop.mpr ⟨hXY haX', h⟩))))))


in the pretty printer which does not then compile. I was finding it hard to eliminate the cases in term mode too.

#### Patrick Massot (Mar 31 2020 at 10:19):

In term mode the rcases becomes a let.

#### Patrick Massot (Mar 31 2020 at 10:20):

I'm only half paying attention, do you want me to post the proof term or is it an exercise for the new Kevin?

#### Kevin Buzzard (Mar 31 2020 at 10:25):

infix is_adherent_to :55 := is_adherent


I definitely think you should choose one or the other. Oh I see it's the infix, but don't we want better notation? Is this what they say in French?

#### Patrick Massot (Mar 31 2020 at 10:29):

It does look like a literal translation from French.

#### Patrick Massot (Mar 31 2020 at 10:30):

In the beginning I was also defining a lot of infix notation to make the assumption look like proper sentences, but then I quickly realized this was unsustainable. I don't even do it in my teaching because this obfuscate unfold lines (that have to refer the the actual name, not the notation).

#### Patrick Massot (Mar 31 2020 at 10:31):

The proof term should be assume a haX ε hε, let ⟨x, haX, h⟩ := haX ε hε in ⟨x, hXY haX, h⟩ by the way.

#### Kevin Buzzard (Mar 31 2020 at 10:32):

Is there a way of writing this without the let?

#### Kevin Buzzard (Mar 31 2020 at 10:33):

It did not occur to me to use let. I never normally use it, I think it obfuscates goals. When there are lets around, tactic mode proofs can start getting ugly goals.

#### Kevin Buzzard (Mar 31 2020 at 15:50):

import data.real.basic
import data.set
import analysis.normed_space.basic

-- Q0. Notation for absolute. Should I reuse this from somewhere in Lean or mathlib?
local notation |x| := abs x

def is_adherent (x : ℝ) (X : set ℝ) : Prop :=
∀ ε > 0, ∃y ∈ X, |x - y| ≤ ε

infix is_adherent_to :55 := is_adherent

def closure' (X : set ℝ) : set ℝ :=
{x : ℝ | x is_adherent_to X }

-- closure_mono term proof

/-- If $X\subseteq Y$ then $\overline{X}\subseteq\overline{Y}$ -/
theorem closure'_mono {X Y : set ℝ} (hXY : X ⊆ Y) : closure' X ⊆ closure' Y :=
λ a haX ε hε, let ⟨x, haX', h⟩ := haX ε hε in ⟨x, hXY haX', h⟩

-- closure_mono tactic proof
example {X Y : set ℝ} (hXY : X ⊆ Y) : closure' X ⊆ closure' Y :=
begin
-- Say a is in the closure of X. We want to show a is in the closure of Y.
-- So say ε > 0. We want to find y ∈ Y such that |a - y| ≤ ε.
intros a haX ε hε,
-- By definition of closure of X, there's x ∈ X with |a - x| ≤ ε.
rcases haX ε hε with ⟨x, haX', h⟩,
-- So let y be x.
use x,
-- Remark:
split,
{ -- x is in Y because it's in X and X ⊆ Y
exact hXY haX', -- hXY is actually a function!
},
-- oh but now one of our assumptions is the conclusion
assumption
end

-- subset_closure term proof

/-- For all subsets $X$ of $\mathbb{R}$, we have $X\subseteq\overline{X}$ -/
lemma subset_closure' {X : set ℝ} : X ⊆ closure' X :=
λ x hx ε hε, ⟨x, hx, le_of_lt (by rwa [sub_self, abs_zero])⟩

-- tactic proof

example {X : set ℝ} : X ⊆ closure' X :=
begin
-- Say x ∈ X and ε > 0.
intros x hx ε hε,
-- We need to find y ∈ X with |x - y| ≤ ε. Just use x.
use x,
-- Remark: x ∈ X
split, exact hx,
-- Note also that |x - x| is obviously zero
simp,
-- and because ε > 0 we're done
exact le_of_lt hε
-- Note that that last bit would have been better if your definition of closure'
-- had used < and not ≤
end

-- closure_closure

-- Note: for some reason this is not formalaised as closure ∘ closure = closure
-- I don't know why we have this convention

-- tactic mode proof

/-- The closure of $\overline{X}$ is $\overline{X}$ again -/
lemma closure'_closure' (X : set ℝ) : closure' (closure' X) = closure' X := --
begin
-- We prove inclusions in both directions
ext a,
split,
--
{ -- ⊆ : say $a$ is in the closure of $\overline{X}$.
intro ha,
-- We want to show it's in $\overline{X}$ so say ε > 0, and we want x with |x-a| ≤ ε
intros ε hε,
-- By definition of a, there's some elements $b\in\overline{X}$
-- with |a - b| ≤ ε/2
rcases ha (ε/2) (by linarith) with ⟨b, hb, hab⟩,
-- and by definition of b there's some x ∈ X with |b - x| ≤ ε/2
rcases hb (ε/2) (by linarith) with ⟨x, hx, hbx⟩,
-- Let's use this x
use x,
-- Note it's obviously in X
split, exact hx,
-- and now |a - x| = |(a - b) + (b - x)|
calc |a - x| = |(a - b) + (b - x)| : by ring
-- ≤ ε/2 + ε/2 = ε
...          ≤ |a - b| + |b - x|   : by apply abs_add
...          ≤ ε : by linarith
},
{ -- ⊇ : follows immediately from subset_closure'
intro h, apply subset_closure' h,
}
end

-- closure_squeeze term mode proof
lemma closure'_squeeze {X Y : set ℝ} (h₁ : X ⊆ Y) (h₂ : Y ⊆ closure'(X)) :
closure'(X) = closure'(Y) :=
set.subset.antisymm (closure'_mono h₁) $by rw ←closure'_closure' X; apply closure'_mono h₂ -- tactic mode proof example {X Y : set ℝ} (h₁ : X ⊆ Y) (h₂ : Y ⊆ closure'(X)) : closure'(X) = closure'(Y) := begin -- We prove inclusions in both directions apply set.subset.antisymm, { -- ⊆ is just closure'_mono apply closure'_mono h₁}, { -- ⊇ -- first use closure'_closure' rw ←closure'_closure' X, -- and then it follows from closure'_mono apply closure'_mono h₂}, end  @Kevin Doran #### Reid Barton (Mar 31 2020 at 15:53): I think "destructuring let" (with a pattern match on the left) doesn't actually translate to a let in the usual sense. #### Kevin Buzzard (Mar 31 2020 at 15:53): I think the more mathematically natural definition of adherent is def is_adherent (x : ℝ) (X : set ℝ) : Prop := ∀ ε > 0, ∃y ∈ X, |x - y| < ε  This is because eps > 0 and not eps >= 0. #### Kevin Buzzard (Mar 31 2020 at 15:54): I hadn't realised that one needed let. I was just trying to do (haX ε hε).1 and it wouldn't work. #### Reid Barton (Mar 31 2020 at 15:55): Assuming this is referring to a Prop, there's no reason to avoid this kind of let. If you put _ after in and put your cursor on it you'll see the context is the same as it would be in a tactic proof where you used rcases. #### Reid Barton (Mar 31 2020 at 15:56): Although if you used a "true" let I don't know what the context would look like, actually. But this kind of let must just be translated to an application of the recursor. #### Reid Barton (Mar 31 2020 at 15:57): (Maybe multiple applications of recursors.) #### Kevin Buzzard (Mar 31 2020 at 15:59): I hadn't realised this. Thanks! #### Kevin Doran (Apr 02 2020 at 01:07): @Kevin Buzzard , the example is beautiful, thanks. It's funny to look back now at my original monolith. #### Kevin Doran (Apr 02 2020 at 04:50): I have a follow up question. I'm posting it in the existing thread due to the shared context of closures. When proving a conjunction where both conjuncts share a common quantifier and assumption, can the quantifier and assumption be introduced before the proof splits? Concrete example below: import data.real.basic import data.set namespace my_closure local notation |x| := abs x def is_adherent (x : ℝ) (X : set ℝ) : Prop := ∀ ε > 0, ∃y ∈ X, |x - y| < ε def closure(X : set ℝ) : set ℝ := {x : ℝ | is_adherent x X } lemma closure_inter_subset_inter_closure' (X Y : set ℝ) : closure (X ∩ Y) ⊆ closure X ∩ closure Y := begin intros a ha, split, repeat { intros ε hε, rcases ha ε hε with ⟨xy, hxy, _⟩, use xy, cases hxy with l r, split; assumption } end end my_closure  It want to know how to prove the above without a repeat—have something like a intros a ha ε hε at the begging, then split the conjunction. #### Kevin Buzzard (Apr 02 2020 at 06:09): I've seen people write things like split; intro h before but I never thought it was particularly good style #### Kevin Buzzard (Apr 02 2020 at 06:10): This way the intro gets applied to both strands of the proof #### Kevin Doran (Apr 02 2020 at 06:38): [In the right stream this time] Ah, I see. They it could be taken to the extreme and have all tactics apply to both strands: lemma closure_inter_subset_inter_closure (X Y : set ℝ) : closure (X ∩ Y) ⊆ closure X ∩ closure Y := begin intros a ha, split; intros ε hε; rcases ha ε hε with ⟨xy, hxy, h₁⟩; use xy; cases hxy; split; assumption, end  This too falls into the category of being questionable style? Are there other alternatives (other than repeat)? #### Kenny Lau (Apr 02 2020 at 06:46): if "style" means mathlib style: lemma closure_mono {X Y : set ℝ} (H : X ⊆ Y) : closure X ⊆ closure Y := λ a ha ε hε, let ⟨p, hpx, hapε⟩ := ha ε hε in ⟨p, H hpx, hapε⟩ lemma closure_inter_subset_inter_closure' {X Y : set ℝ} : closure (X ∩ Y) ⊆ closure X ∩ closure Y := set.subset_inter (closure_mono$ set.inter_subset_left X Y)
(closure_mono \$ set.inter_subset_right X Y)


#### Kenny Lau (Apr 02 2020 at 06:47):

and if you insist on using tactics, you can still have the lemma

#### Kevin Doran (Apr 02 2020 at 07:30):

That's pretty. I wish the proofs would come to mind like that, and not as hacks with epsilons.

#### Kevin Buzzard (Apr 02 2020 at 07:44):

You want to move away from the epsilons as soon as possible. This is the whole point of proving things such as closure_mono. There might be a few basic properties such as closure_mono which ultimately end up defining all the key features of your closure function. It's probably something like a Galois insertion or something -- some very abstract combinatorial definition which implies a whole bunch of properties which a mathematician might try and prove with epsilons.

#### Kevin Doran (Apr 02 2020 at 07:48):

That's become very apparent to me.

#### Reid Barton (Apr 02 2020 at 07:54):

Kevin Doran said:

[In the right stream this time]
This too falls into the category of being questionable style? Are there other alternatives (other than repeat)?

After split;, use { }.

#### Kevin Doran (Apr 02 2020 at 07:59):

@Reid Barton, that's better.
Posting the tweaked code for reference.

lemma closure_inter_subset_inter_closure (X Y : set ℝ) :
closure (X ∩ Y) ⊆ closure X ∩ closure Y :=
begin
intros a ha,
split; {
intros ε hε,
rcases ha ε hε with ⟨xy, hxy, h₁⟩,
use xy,
cases hxy,
split;
assumption,
}
end


#### Patrick Massot (Apr 03 2020 at 14:08):

  rcases ha ε hε with ⟨xy, hxy, _⟩,
...
cases hxy with l r,


#### Patrick Massot (Apr 03 2020 at 14:09):

This is useless splitting

#### Patrick Massot (Apr 03 2020 at 14:09):

You can use rcases ha ε hε with ⟨xy, ⟨l, r⟩, _⟩,

#### Patrick Massot (Apr 03 2020 at 14:10):

But of course Kenny's solution to use closure_mono is actually the "right" answer.

#### Patrick Massot (Apr 03 2020 at 14:21):

And now let me introduce you to the next level:

lemma closure_mono : monotone closure :=
λ X Y H a ha ε hε, let ⟨p, hpx, hapε⟩ := ha ε hε in ⟨p, H hpx, hapε⟩

lemma closure_inter_subset_inter_closure' (X Y : set ℝ) :
closure (X ∩ Y) ⊆ closure X ∩ closure Y :=
(closure_mono).map_inf_le _ _


#### Kenny Lau (Apr 03 2020 at 14:26):

what import does that use?

#### Patrick Massot (Apr 03 2020 at 14:26):

Nothing beyond data.real.basic

#### Patrick Massot (Apr 03 2020 at 14:27):

And Kevin's definition of closure of course

#### Patrick Massot (Apr 03 2020 at 14:27):

The full thing is:

import data.real.basic
namespace my_closure

local notation |x| := abs x

def is_adherent (x : ℝ) (X : set ℝ) : Prop :=
∀ ε > 0, ∃y ∈ X, |x - y| < ε

def closure(X : set ℝ) : set ℝ :=
{x : ℝ | is_adherent x X }

lemma closure_mono : monotone closure :=
λ X Y H a ha ε hε, let ⟨p, hpx, hapε⟩ := ha ε hε in ⟨p, H hpx, hapε⟩

lemma closure_inter_subset_inter_closure' (X Y : set ℝ) :
closure (X ∩ Y) ⊆ closure X ∩ closure Y :=
(closure_mono).map_inf_le _ _

end my_closure


#### Kevin Buzzard (Apr 03 2020 at 14:41):

So Reid pointed out this Wikipedia link which seems to say that the three properties isolated earlier (closure_mono, le_closure, closure_closure) seem to be equivalent to saying that the closure operator is a Galois insertion.

#### Kevin Buzzard (Apr 03 2020 at 14:42):

I see so this fundamental idea seems to be actually equivalent to the concept of a Galois insertion.

#### Kevin Buzzard (Apr 05 2020 at 13:15):

Kevin Doran said:

Apologies, I did not include a namespace in my snippet.

Kevin Buzzard , thanks for the rw tip! Regarding the monolithic proof, my intention is to follow a textbook, and those closure properties you mention are later proved using this one.

@Kevin Doran which textbook were you following, out of interest?

#### Kevin Doran (Apr 05 2020 at 13:27):

It's Tao's Analysis I.

#### Patrick Massot (Apr 05 2020 at 13:35):

We need to have a conversation with that guy.

#### Andrew Ashworth (Apr 05 2020 at 17:44):

It's a good book for analysis formalization. I think I got up to chapter 5 before I decided I had more interesting things to do on the weekends. There's also a similarly half-finished version done by someone in Lean 2 lying around somewhere on Github

#### Andrew Ashworth (Apr 05 2020 at 17:46):

If you get far with it I'd be pretty interested in reading your code

#### Kevin Buzzard (Apr 05 2020 at 18:59):

@Andrew Ashworth What's wrong with all this calculus stuff in mathlib? I reckon they've got further than chapter 5 of Tao by now -- they have manifolds!

#### Patrick Massot (Apr 05 2020 at 19:00):

That's a completely different story. All those people doing elementary analysis and topology in Lean without using what's in mathlib are doing exercises, or want to teach.

#### Patrick Massot (Apr 05 2020 at 19:01):

I do it as well. In my lectures, I define limits of a sequence without using mathlib, and ask my students to prove many lemmas that are super special cases of things we already have in mathlib.

#### Kevin Buzzard (Apr 05 2020 at 19:06):

Yes I know. Isn't it interesting? One could ask why people formalise it at all, given that it's all a super-special case of mathlib. If we want people to do exercises or to teach them then we should write some definitive approach where everything gets done in a mathlib-sensible order and then tell people to work through that.

#### Ryan Lahfa (Apr 05 2020 at 19:32):

Kevin Buzzard said:

Yes I know. Isn't it interesting? One could ask why people formalise it at all, given that it's all a super-special case of mathlib. If we want people to do exercises or to teach them then we should write some definitive approach where everything gets done in a mathlib-sensible order and then tell people to work through that.

FWIW, I see two reasons:

(1) mathlib uses machinery that students are not necessarily accustomed to, aware or can even understand (e.g. filters for undergraduate in topology who never know there is such thing as a topological space)
(2) Teachers want you to re-formalize with another approach which is different from mathlib one; it's interesting, but it gets annoying to not be able to rely on the shoulders of giants, but that brings me to the next point.

If someone wanted to start to contribute to Lean or learn how to do advanced things in Lean (after doing the nat games, read the manual, read the docs), how should he proceed? Is there a list of lemmas that are not there? Good first issues for beginners?
Some docs on this (maybe it exist and I just didn't search hard enough…) would be awesome.

If that's possible, then it becomes possible to do school projects around contributing to mathlib.

#### Patrick Massot (Apr 05 2020 at 19:34):

Contributing elementary stuff to mathlib becomes harder and harder. You missed the golden age two years ago.

#### Patrick Massot (Apr 05 2020 at 19:34):

But @Shing Tak Lam still managed to find something with partial derivatives of polynomials.

#### Kevin Buzzard (Apr 05 2020 at 19:35):

When I got interested in Lean in mid-2017 there were a ton of such issues. Lean didn't even have the complex numbers! My first PR to mathlib was a definition of the complex numbers as a pair of real numbers.

But now things are completely different. It's much harder to find undergraduate level gaping holes in mathlib, and many of the undergraduate holes left need very careful consideration by experts, unfortunately. For example, for years we did not have a basic theory of calculus in one variable, and I was always pushing for it, but the people like Patrick and Sebastien who understood analysis properly assured me that we just had to wait and do it properly, with stuff like the Bochner integral and multivariable calculus all done first before the one variable case.

#### Kevin Buzzard (Apr 05 2020 at 19:36):

The partial derivative thing was just a fluke -- we were riffing with this STEP question and thought about the two-variable case and then all of a sudden we ran into this hole.

#### Kevin Buzzard (Apr 05 2020 at 19:37):

Over Easter I plan on doing 1000 things, and amongst them is writing some tutorials for post-natural-number-game people. Until then there's always the stuff on codewars. Right now I am checking that a super-hard codewars level I set this afternoon is actually solvable.

#### Patrick Massot (Apr 05 2020 at 19:38):

Ryan, what happened to your absolute value stuff by the way?

#### Ryan Lahfa (Apr 05 2020 at 19:49):

Patrick Massot said:

Ryan, what happened to your absolute value stuff by the way?

I paused the work on this to help some students on this metric space thing and I used this opportunity to learn more Lean to write the whole machinery for Bolzano Weierstrass, hence my recent questions

I learned a lot and feel like I'll be able to move forward faster for the Ostrowski/absolute value thing

#### Ryan Lahfa (Apr 05 2020 at 19:49):

Kevin Buzzard said:

Over Easter I plan on doing 1000 things, and amongst them is writing some tutorials for post-natural-number-game people. Until then there's always the stuff on codewars. Right now I am checking that a super-hard codewars level I set this afternoon is actually solvable.

#### Patrick Massot (Apr 05 2020 at 19:49):

Do you help students learning Lean or BW?

#### Ryan Lahfa (Apr 05 2020 at 19:50):

Patrick Massot said:

Do you help students learning Lean or BW?

Learning Lean and I decompose some theorems they have to prove as smaller parts while explaining them the maths behind this and the process of proving "a big theorem" (R is a complete, for example)

#### Patrick Massot (Apr 05 2020 at 19:51):

Where did you find those students?

#### Patrick Massot (Apr 05 2020 at 19:51):

Which construction of R do you want to use? Proving completeness of R is very dependent on its construction.

#### Ryan Lahfa (Apr 05 2020 at 19:52):

Kevin Buzzard said:

When I got interested in Lean in mid-2017 there were a ton of such issues. Lean didn't even have the complex numbers! My first PR to mathlib was a definition of the complex numbers as a pair of real numbers.

But now things are completely different. It's much harder to find undergraduate level gaping holes in mathlib, and many of the undergraduate holes left need very careful consideration by experts, unfortunately. For example, for years we did not have a basic theory of calculus in one variable, and I was always pushing for it, but the people like Patrick and Sebastien who understood analysis properly assured me that we just had to wait and do it properly, with stuff like the Bochner integral and multivariable calculus all done first before the one variable case.

Patrick Massot said:

Contributing elementary stuff to mathlib becomes harder and harder. You missed the golden age two years ago.

I definitely see that. But in some schools, complex analysis is considered to be undergraduate level in France AFAIK and isn't this something that mathlib does not have currently?

#### Kevin Buzzard (Apr 05 2020 at 19:53):

@Jason KY. has been learning metric spaces using Lean (he will not go to the metric space course until next year). He just proved that closure was a Galois connection :-) I'm not entirely sure if this statement is covered in the course, but it's where we ended up going...

#### Ryan Lahfa (Apr 05 2020 at 19:53):

Patrick Massot said:

Where did you find those students?

In Jussieu, there is a math project and Frédéric Paugam suggested to work on Lean, so there are two groups of 4 students working on Lean, the plan is to do: natural number games → reworking the metric space file that Frédéric Le Roux initiated to see how to do metric spaces without filters and in a more natural way for undergraduate students

#### Kevin Buzzard (Apr 05 2020 at 19:54):

I am absolutely serious: you should just make the metric space stuff into a tutorial.

#### Kevin Buzzard (Apr 05 2020 at 19:54):

and then throw it into Patrick's tutorial project.

#### Patrick Massot (Apr 05 2020 at 19:54):

Oh yes, I remembered you mentioned working with Paugam.

#### Jason KY. (Apr 05 2020 at 19:54):

Kevin Buzzard said:

Jason KY. has been learning metric spaces using Lean (he will not go to the metric space course until next year). He just proved that closure was a Galois connection :-) I'm not entirely sure if this statement is covered in the course, but it's where we ended up going...

I won't have metric spaces next year :P They replaced the course with Lesbegue measure theory instead!

#### Kevin Buzzard (Apr 05 2020 at 19:55):

I think the metric space stuff in mathlib is hard to read. Even the definition of a metric space is intimidating because all the auto-generated fields are displayed both in mathlib and in the docs.

#### Patrick Massot (Apr 05 2020 at 19:56):

I definitely intend to transform my first year exercises into a tutorial in the near future. But this is even more elementary than metric spaces.

#### Patrick Massot (Apr 05 2020 at 19:56):

What's nice with metric spaces is you need to build structures and classes. This is not at all covered in my class.

#### Kevin Buzzard (Apr 05 2020 at 19:56):

Patrick -- how do you feel about adding a bunch of files with sorrys into the tutorial project? Would this be Ok?

#### Patrick Massot (Apr 05 2020 at 19:56):

So that would be a very nice follow-up

#### Kevin Buzzard (Apr 05 2020 at 19:56):

Metric space is a great example of a structure.

#### Ryan Lahfa (Apr 05 2020 at 19:57):

Patrick Massot said:

Which construction of R do you want to use? Proving completeness of R is very dependent on its construction.

I'm using the usual construction of R coming from mathlib, but I use another definition of convergence, etc ; so I cannot reuse all the cau_seq part from mathlib (though I could prove equivalence).

I didn't bother too much because I wanted a R-agnostic proof, just give me something which looks like R, some sup/inf and here's completeness

But in the metric space file, there are plans to take completed space (using quotient of Cauchy sequences) so we can build R from Q using this and try to prove that our R is isomorphic to mathlib's R (which is cool IMHO).

#### Patrick Massot (Apr 05 2020 at 19:57):

Kevin Buzzard said:

Patrick -- how do you feel about adding a bunch of files with sorrys into the tutorial project? Would this be Ok?

Yes, this is what I want to do. Keep the only existing file as a kind of overview of the basics, then have a lot of exercises.

#### Kevin Buzzard (Apr 05 2020 at 19:57):

We are picking up people who know about the basics of apply and intro exact because of NNG. Getting them working on metric spaces would be great because this is proper mathematics, not like all this Peano nonsense.

#### Ryan Lahfa (Apr 05 2020 at 19:58):

Kevin Buzzard said:

But we are picking up people who know about the basics of apply and intro exact because of NNG. Getting them working on metric spaces would be great because this is proper mathematics, not like all this Peano nonsense.

I want now NNG with ZFC…………… Can I?

#### Kevin Buzzard (Apr 05 2020 at 19:58):

What does that mean?

#### Ryan Lahfa (Apr 05 2020 at 19:58):

Kevin Buzzard said:

Jason KY. has been learning metric spaces using Lean (he will not go to the metric space course until next year). He just proved that closure was a Galois connection :-) I'm not entirely sure if this statement is covered in the course, but it's where we ended up going...

Wow!

#### Kevin Buzzard (Apr 05 2020 at 19:58):

If it means what I think it means, the first thing you should do in ZFC is to prove that induction and recursion work, and then just do things like NNG anyway :-)

#### Ryan Lahfa (Apr 05 2020 at 19:59):

Kevin Buzzard said:

What does that mean?

Building natural numbers with ZFC rather than Peano, but yes, once you have minimal stuff, it becomes like with Peano

#### Kevin Buzzard (Apr 05 2020 at 19:59):

It's not that hard to prove it's a Galois connection. It's one of these things which sounds super-complicated but is just some abstract computer science way of saying some triviality about closures.

#### Ryan Lahfa (Apr 05 2020 at 20:00):

Kevin Buzzard said:

It's not that hard to prove it's a Galois connection. It's one of these things which sounds super-complicated but is just some abstract computer science way of saying some triviality about closures.

Still, it is not expected to see what is a Galois connection, and stuff around order theory (though I really like order theory but that's just me…)

#### Ryan Lahfa (Apr 05 2020 at 20:00):

I really also like the idea that Lean could be used to learn mathematics, but I'm unsure whether it's a good idea (?)

#### Ryan Lahfa (Apr 05 2020 at 20:00):

(I learned a lot of maths thanks to mathlib docs to be honest… :D)

#### Kevin Buzzard (Apr 05 2020 at 20:01):

I think this is an interesting point. The people at Xena seem to be the ones who are on top of the material in the lectures. Athina Thoma specialises in education and she told me that she thinks it's difficult to teach people Lean and equivalence relations at the same time if a student has never heard of either of them before.

#### Kevin Buzzard (Apr 05 2020 at 20:02):

This is why NNG is a nice thing to do because everyone knows natural numbers already, even if they didn't know why addition was commutative. The objects are not intimidating.

#### Patrick Massot (Apr 05 2020 at 20:03):

In my course I don't cover any maths the students haven't met before. But I do cover a lot of maths they didn't understand before (all this "proving" stuff for instance).

#### Kevin Buzzard (Apr 05 2020 at 20:05):

Yes this is exactly what I do in my course, and then the Xena people are the ones who kind of knew what a proof was already. I want to use Lean to teach people what a proof is but I just attract people who know what it is already.

#### Ryan Lahfa (Apr 05 2020 at 20:06):

Definitely, once you have enough experience with Lean, well, the new game is the whole mathematics.

Also, I'm interested in Lean for computer science, proving some correctness of algorithms you see as CS undergraduate, this sort terminates, etc, etc.
But that's something I didn't have time to get in, though doing some maths first was super important because the purpose of those specific mathlib containers which looked like really my std::vector or a list in Haskell was not totally obvious to me at start.

#### Ryan Lahfa (Apr 05 2020 at 20:06):

Kevin Buzzard said:

Yes this is exactly what I do in my course, and then the Xena people are the ones who kind of knew what a proof was already. I want to use Lean to teach people what a proof is but I just attract people who know what it is already.

There is a finite number of people who know what is a proof, so surely, you will attract people who don't know what it is!

#### Patrick Massot (Apr 05 2020 at 20:07):

A couple of weeks ago I heard one student telling the other: "Oh, I think I'm beginning to understand the math101 course" (the one where they studied limits without understanding any proof).

#### Patrick Massot (Apr 05 2020 at 20:08):

But of course the best students in my course were probably the best ones before. It's very frustrating that Covid-19 will completely ruin my hope to measure the impact of my course.

#### Ryan Lahfa (Apr 05 2020 at 20:11):

Patrick Massot said:

But of course the best students in my course were probably the best ones before. It's very frustrating that Covid-19 will completely ruin my hope to measure the impact of my course.

Are exams completely canceled in Orsay? Or are they like bonus marks only?

#### Patrick Massot (Apr 05 2020 at 20:12):

Nobody really knows. But it's already clear that everything will be biased by the lock-down.

#### Ryan Lahfa (Apr 05 2020 at 20:14):

Patrick Massot said:

Nobody really knows. But it's already clear that everything will be biased by the lock-down.

Ah :/
In Jussieu, they decided that everything done during the lock-down can only be beneficial to students, otherwise it'll be ignored.
Meaning, there is no real incentive to continue studying right now ; but at the same time, some parts are unclear, e.g. whether a final exam or not will be performed in June.

#### Patrick Massot (Apr 05 2020 at 20:15):

It seems that roughly half of my students are still working. But the bias is this is most probably the better half.

#### Scott Morrison (Apr 06 2020 at 01:56):

It is pretty worrying that Kevin above has said "all the easy stuff is done". I don't think that's really the case at all, and we need to provide much better "on-ramping" to get new users towards useful things they could contribute.

#### Scott Morrison (Apr 06 2020 at 01:57):

We need a better workflow for turning sorry into an accessible issue marked "needs-help" "new-user" somewhere. :-)

#### Scott Morrison (Apr 06 2020 at 04:34):

... maybe we need a channel here for standalone sorries. :-)

#### Scott Morrison (Apr 06 2020 at 04:35):

We could have some standard set of emojis for "found the lemma in mathlib", "proof provided", "new user issue created", "sounds hard".

#### Scott Morrison (Apr 06 2020 at 04:35):

to keep track of progress :-)

#### Alex J. Best (Apr 06 2020 at 04:38):

I've often wondered about this, how feasible it is to have a natural number game / proving for fun / codewars style website to collaboratively work towards a goal one lemma at a time. Sometimes I want to do some lean for mathlib but not spend several hours on a project.

#### Scott Morrison (Apr 06 2020 at 04:55):

Anyone want to: locate in mathlib / PR / generalize-then-PR:

@[simp]
begin
cases L,
{ simp, refl, },
{ simp, },
end

-- lemma head_le_sum (L : list ℕ) : L.head ≤ L.sum := by library_search -- fails

@[simp]
lemma tail_sum (L : list ℕ) : L.tail.sum = L.sum - L.head :=
begin
omega,
end


#### Scott Morrison (Apr 06 2020 at 04:56):

Is this the sort of thing we could conceivably put on a big list / gamify?

#### Scott Morrison (Apr 06 2020 at 04:58):

Really we need something real time and interactive. :-)

#### Kevin Buzzard (Apr 06 2020 at 06:05):

By "all the easy stuff is done" I mean "it is no longer the case that a beginner eg Kevin in 2017 can just come along and do the complex numbers". The elementary stuff which needs doing typically needs to be done in a certain way which beginners can't do. This at least is my impression

#### Yury G. Kudryashov (Apr 06 2020 at 06:06):

I'm doing quaternions now. It's not much harder than complex numbers...

#### Kevin Buzzard (Apr 06 2020 at 06:08):

That's a good counterpoint :-)

sedenions!

#### Kevin Buzzard (Apr 06 2020 at 09:16):

rofl, I'd never heard of these. A 16-dimensional algebra in which no axioms hold at all!

#### Kevin Buzzard (Apr 06 2020 at 09:16):

Oh I take that back -- it's a distrib! rofl so that's the point of distribs!

#### Johan Commelin (Apr 06 2020 at 09:23):

Lol, also

Moreno (1998) showed that the space of pairs of norm-one sedenions that multiply to zero is homeomorphic to the compact form of the exceptional Lie group G2. (Note that in his paper, a "zero divisor" means a pair of elements that multiply to zero.)

#### Kevin Buzzard (Apr 06 2020 at 09:26):

wow so actually they do have a point :-)

#### Kevin Buzzard (Apr 06 2020 at 09:26):

Oh wait -- homeomorphic? No group structure?

#### Ryan Lahfa (Apr 06 2020 at 11:15):

Do we even have Clifford algebras?

Not in mathlib

#### Ryan Lahfa (Apr 06 2020 at 11:15):

But in perfectoid I suppose?

nope

Oh okay

#### Johan Commelin (Apr 06 2020 at 12:07):

Ok, I should have said "Not in any repo I know of"

#### Patrick Massot (Apr 06 2020 at 12:15):

If you want more algebra I'd suggest doing antisymmetric multilinear forms long before doing Clifford algebras.

#### Ryan Lahfa (Apr 06 2020 at 13:15):

Patrick Massot said:

If you want more algebra I'd suggest doing antisymmetric multilinear forms long before doing Clifford algebras.

Isn't something being worked on? I have seen some commits multilinear/* but I don't know what's the state of all this

#### Patrick Massot (Apr 06 2020 at 13:43):

Yes, Sébastien did a lot on multilinear on his way to higher order derivatives and then analytic functions. But I really mean exterior algebras.

#### Patrick Massot (Apr 06 2020 at 13:43):

In particular we probably want to do it right in full generality, provided this doesn't make elementary examples too painful.

#### Patrick Massot (Apr 06 2020 at 13:45):

There is a tension between having $\Lambda^k V^*$ seen as the subspace of multilinear maps from $V^k$ to the base field which happen to be antisymmetric, which is nice and concrete, and the fact this is clearly wrong in positive characteristic where there is no other choice than seeing it as a quotient of the tensor algebra.

#### Patrick Massot (Apr 06 2020 at 13:47):

So I would say to first have a look at what we have about tensor algebras (I know there are binary tensor product, but I'm afraid maybe not much more). Then try the quotient route. And then think about simpler things.

Last updated: May 13 2021 at 17:42 UTC