cleaning up this tactic proof (regarding closures)

Stream: new members

[Kevin Doran]

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₃,
    unfold is_adherent at 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]

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]

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

[Kevin Buzzard]

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]

What you need is abs_add I guess.

[Yury G. Kudryashov]

This structure is defined in normed_space.basic

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Doran]

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]

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

[Kevin Doran]

Also, I would love a real number game.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Doran]

Thanks a million!

[Kevin Buzzard]

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

[Kevin Buzzard]

The same is true for closure_closure

[Kevin Buzzard]

It's just a 2epsilon proof

[Patrick Massot]

Can I vote twice for proving closure_mono first?

[Patrick Massot]

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

[Kevin Doran]

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]

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]

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

[Kevin Buzzard]

@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]

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]

The only tactics this proof uses are trivialities.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Formalising reveals an underlying elegance which humans often miss.

[Kevin Buzzard]

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

[Patrick Massot]

Why do you tag all your definitions as reducible?

[Patrick Massot]

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

[Kevin Doran]

@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]

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]

In term mode the rcases becomes a let.

[Patrick Massot]

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]

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]

It does look like a literal translation from French.

[Patrick Massot]

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]

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]

Is there a way of writing this without the let?

[Kevin Buzzard]

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]

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]

I think "destructuring let" (with a pattern match on the left) doesn't actually translate to a let in the usual sense.

[Kevin Buzzard]

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]

I hadn't realised that one needed let. I was just trying to do (haX ε hε).1 and it wouldn't work.

[Reid Barton]

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]

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]

(Maybe multiple applications of recursors.)

[Kevin Buzzard]

I hadn't realised this. Thanks!

[Kevin Doran]

@Kevin Buzzard , the example is beautiful, thanks. It's funny to look back now at my original monolith.

[Kevin Doran]

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]

I've seen people write things like split; intro h before but I never thought it was particularly good style

[Kevin Buzzard]

This way the intro gets applied to both strands of the proof

[Kevin Doran]

[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]

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]

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

[Kevin Doran]

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

[Kevin Buzzard]

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]

That's become very apparent to me.

[Reid Barton]

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]

@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]

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

[Patrick Massot]

This is useless splitting

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

what import does that use?

[Patrick Massot]

Nothing beyond data.real.basic

[Patrick Massot]

And Kevin's definition of closure of course

[Patrick Massot]

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]

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]

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

[Kevin Buzzard]

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]

It's Tao's Analysis I.

[Patrick Massot]

We need to have a conversation with that guy.

[Andrew Ashworth]

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]

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

[Kevin Buzzard]

@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]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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]

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

[Ryan Lahfa]

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]

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.

I'm really curious about this super-hard level :D… Please post it when it's ready!

[Patrick Massot]

Do you help students learning Lean or BW?

[Ryan Lahfa]

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]

Where did you find those students?

[Patrick Massot]

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

[Ryan Lahfa]

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]

@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]

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]

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

[Kevin Buzzard]

and then throw it into Patrick's tutorial project.

[Patrick Massot]

Oh yes, I remembered you mentioned working with Paugam.

[Jason KY.]

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]

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]

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]

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]

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

[Patrick Massot]

So that would be a very nice follow-up

[Kevin Buzzard]

Metric space is a great example of a structure.

[Ryan Lahfa]

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]

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]

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]

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]

What does that mean?

[Ryan Lahfa]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Ryan Lahfa]

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]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

to keep track of progress :-)

[Alex J. Best]

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]

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

@[simp]
lemma head_add_tail_sum (L : list ℕ) : L.head + L.tail.sum = L.sum :=
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
  have := head_add_tail_sum L,
  omega,
end

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

That's a good counterpoint :-)

[Scott Morrison]

sedenions!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

wow so actually they do have a point :-)

[Kevin Buzzard]

Oh wait -- homeomorphic? No group structure?

[Ryan Lahfa]

Do we even have Clifford algebras?

[Johan Commelin]

Not in mathlib

[Ryan Lahfa]

But in perfectoid I suppose?

[Kevin Buzzard]

nope

[Ryan Lahfa]

Oh okay

[Johan Commelin]

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

[Patrick Massot]

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

[Ryan Lahfa]

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]

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]

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

[Patrick Massot]

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]

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.