Math education question (teaching textbook proofs in Lean)

Stream: maths

[Chris B]

Hi. I'm from the computer science contingency of Lean users, but I'm going through 'Understanding Analysis' to try some very basic 'proper math' in Lean. Many of the proofs use arguments that are classics, but either aren't very Lean-friendly or aren't constructive. As an example, the proof of irrat (sqrt 2) used in the book is the proof by contradiction/infinite descent.

Is the approach you guys have taken (or would take) for math education to say "Well here's how these are done in Lean/mathlib, the sooner you get used to doing things this way the better", or is it to try and power through the classic definitions in Lean? Or are you trying to give equal time to both approaches?

Thanks!

[Chris Hughes]

We certainly don't worry about being constructive. Usually

[Chris Hughes]

If something in mathlib differs from theclassical definition it's because it's in a greater generality, in which case the classical definition is better to formalize.

[Johan Commelin]

@Chris B What do you mean when you say "Many of the proofs ... either aren't very Lean-friendly"? If there are proofs in the library that can be optimized to become more Lean friendly, I think we very much welcome those.

[Johan Commelin]

Some of our contributors care more about being constructive than others. But in general, we unashamedly celebrate the axiom of choice.

[Patrick Massot]

Do you refer to https://www.amazon.com/Understanding-Analysis-Undergraduate-Texts-Mathematics/dp/1493927116?

[Patrick Massot]

Note that I don't understand your question either way.

[Chris B]

@Johan Commelin Sorry, I meant "the proofs in the textbook aren't always Lean-friendly" in that some of the things they take for granted don't seem trivial in Lean. I'm sure the ones in mathlib are great.

[Patrick Massot]

What is an example of a non-Lean friendly proof? I don't understand the issue with the irrationality of sqrt 2 example.

[Johan Commelin]

Aha... I see. And I'm sure there are also lots of proofs in mathlib that could be improved. But yes... most maths is not "designed to be formalised" to quote Mario out of context.

[Chris B]

@Patrick Massot Yes, that's the book. Maybe 'lean-aware' is a better choice of words than 'lean friendly'. The irrat sqrt 2 proof is simple, but it's not aware of the behavior/interaction between Lean's number types or the fact that rewriting terms in Lean is not always as easy as it is on paper, so as someone who's not super familiar with mathlib it's not trivial to recreate in terms of time and might end up brittle, ugly etc. On the other hand, there is also a definition of irrat sqrt 2 in mathlib that is different but was written by someone who IS aware of those things.

The question was whether educators who were using Lean and had a similar pair of proofs (one from mathlib and one from a textbook) were choosing to focus on one or the other.

[Chris B]

@Chris Hughes That's good to know going forward, thanks.

[Patrick Massot]

Maybe we should move this conversation to the "Lean for teaching" stream. When I use Lean for teaching I only use mathlib for its tactics and definition of real numbers. For instance I redefine limits of sequences and functions. I cannot expect my first year students to understand mathlib's use of filters and uniform spaces... This is the same reason we don't use Bourbaki for teaching. The good news is we can still use Lean (and mathlib tactics).

[Chris B]

Interesting, thanks for that insight.

[Tim Daly]

@Patrick Massot I understand, from a lecture by Kevin Buzzard, that you have written python code to convert lean-related material to an interactive webpage, a "literate form" of input involving latex. Where can I get this?

[Jesse Michael Han]

I believe it's https://github.com/leanprover-community/format_lean

[Yufan Lou]

@Patrick Massot

For instance I redefine limits of sequences and functions.

I want to show my friend in advanced calculus the power of LEAN but I haven't got the hang of it yet. Could you show me how you redefined the limits? Btw the theorem I am working on is

$\lim_{n\to\infty} C \cdot a_n = C \cdot \lim_{n\to\infty} a_n \text{ for } C \in \mathbb{R}$

[Yufan Lou]

I am trying to define it according to https://en.wikipedia.org/wiki/(%CE%B5,_%CE%B4)-definition_of_limit

[Yufan Lou]

But it involves an equation and I am kinda stuck on this

import data.real.basic

def lim (x : ℝ) (c : ℝ) (f : ℝ → ℝ) : Prop := ∀ ε > 0, ∃ δ > 0, 0 < abs (x - c) < δ → abs (f x - )

[Yufan Lou]

Oh ok this seems to work

def lim (x : ℝ) (c : ℝ) (f : ℝ → ℝ) (L : ℝ) :=
  ∀ ε > 0, ∃ δ > (0 : ℝ),
    0 < abs (x - c) ∧ abs (x - c) < δ →
    abs (f x - L) < ε

[Yufan Lou]

lol how do I express infinity in this thing

[Alex J. Best]

There is a type ennreal in mathlib that represents non-negative reals with a positive infinity, possibly this does what you want?

import data.real.ennreal

open ennreal
open_locale ennreal

#check (∞ : ennreal)

[Johan Commelin]

@Yufan Lou There are two answers... the first (which is what mathlib does) is to step back, generalize everything and use so-called filters, instead of the epsilon-delta-sequence definition. The second would be to say that some statement is true for x sufficiently close to infty, in other words, for x sufficiently large.

[Johan Commelin]

Btw, the 0 < abs (x - c) doesn't seem very useful in your definition.

[Johan Commelin]

I personally don't think that using ennreal would lead to a nice experience.

[Johan Commelin]

@Yufan Lou What do mathematicians actually mean when that say that f has a limit as x tends to infty? After all, they don't have $\infty \in \mathbb{R}$ either. So they must have explained somewhere what they mean when the abuse notation like this.

[Yufan Lou]

LOL That's a great question, but I don't have a mathematician around to ask

[Yufan Lou]

Oh wait there is a subsection defining the infinity case separately

[Yufan Lou]

Ah... that goes into metric space which I don't understand tho

[Yufan Lou]

The precise statement for limits at infinity is as follows:[16]

Suppose f is defined on a subset D of a metric space X with a metric d X ( x , y ) and maps into a metric space Y with a metric d Y ( x , y ) . Let L ∈ Y.

We say that

lim x → ∞ f ( x ) = L

if for every ε > 0 , there is a real number N > 0 such that there is an x ∈ D where d X ( x , 0 ) > N and such that if d X ( x , 0 ) > N and x ∈ D, then d Y ( f ( x ) , L ) < ε .

[Yufan Lou]

Ok metric space basically redefines absolute value aka "distance" right

[Yufan Lou]

if I only need real number I just replace d X with abs

[Johan Commelin]

Yep, that's right

[Yufan Lou]

Yeah!

def lim_inf (f : ℝ → ℝ) (L : ℝ) :=
  ∀ ε > 0, ∃ N > (0 : ℝ),
    ∃ (x : ℝ) (H : abs (x - 0) > N), abs (f x - L) < ε

How to type the maths abs notation tho

[Yufan Lou]

Also wikipedia language so redundant

[Johan Commelin]

Try \|| I think

[Yufan Lou]

k

[Johan Commelin]

Btw, I think this is taking the limit at all infinities

[Johan Commelin]

You only want the positive one

[Johan Commelin]

In a general metric space you can't really talk of positive and negative infinity

[Johan Commelin]

But you want x > N not abs (x - 0) > N

[Yufan Lou]

oh ok! thanks for simplifying :D

[Yufan Lou]

\|| gives me unexpected token tho

[Yufan Lou]

I still need the other abs right?

[Johan Commelin]

Search mathlib for norm. You'll see the double-bar symbol show up a lot. But I forgot how to input it.

[Yufan Lou]

gotcha

[Yufan Lou]

I see it, it's the same, but I still get unexpected token

[Yufan Lou]

missing import?

[Johan Commelin]

Wouldn't think so...

[Yufan Lou]

also I cannot multiply a function directly with a real LOL

[Johan Commelin]

No... they are different things, right?

[Johan Commelin]

You can try r \bu f

[Johan Commelin]

Where r is real and f a function

[Yufan Lou]

I understand LOL just musing

[Yufan Lou]

oh! let me try

[Johan Commelin]

What does example : normed_field real := by apply_instance give you? If it gives an error, then there is a missing import.

[Yufan Lou]

unknown identifier 'normed_field' missing import it is

[Johan Commelin]

/me never really works with real numbers

[Yufan Lou]

import analysis.normed_space.basic fixes it

[Johan Commelin]

Good

[Yufan Lou]

The name is kinda scary XD I hope it doesn't make proof harder to write

[Johan Commelin]

This is the line that you needed: https://github.com/leanprover-community/mathlib/blob/master/src/analysis/normed_space/basic.lean#L370

[Johan Commelin]

So that explains why the import fixes it

[Yufan Lou]

I see

[Yufan Lou]

Ahh I am getting (deterministic) timeout on this theorem signature

example (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (C • a) (C * L) := sorry

[Scott Morrison]

Can you post a MWE (minimal working example, i.e. showing the imports) so someone can investigate for you?

[Yufan Lou]

$\lim_{n\to\infty} C \cdot a_n = C \cdot \lim_{n\to\infty} a_n \text{ for } C \in \mathbb{R}$

This was the theorem I was going for

[Scott Morrison]

I've never used this part of the library myself, but I do remember students seeing deterministic timeouts when working with normed_fields way too often, so it would be good to get to the bottom of this.

[Scott Morrison]

(I meant, show us exactly the code that produces the deterministic timeout, including the imports)

[Yufan Lou]

Ah, sorry, this is the code

import tactic.norm_num
import data.real.basic
import analysis.normed_space.basic

def lim_inf (f : ℝ → ℝ) (L : ℝ) :=
  ∀ ε > 0, ∃ N > (0 : ℝ),
    ∃ x > N, abs (f x - L) < ε

example (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (C • a) (C * L) := sorry

[Johan Commelin]

@Yufan Lou What happens if you replace C \bu a with (\lambda x, C * a x)?

[Yufan Lou]

That fixes it

[Scott Morrison]

Doubling the timeout limit, it works, but is incredibly slow. :-(

[Yufan Lou]

:sweat: hopefully it's not something too complicated

[Yufan Lou]

meanwhile I'll continue with my proof I think

[Yufan Lou]

LOL how to prove 1 > 0

[Scott Morrison]

@Yufan Lou , I posted an issue for you, I have to go soon but hopefully someone will sort it out: https://github.com/leanprover-community/mathlib/issues/1561

[Scott Morrison]

by norm_num.

[Yufan Lou]

Ah Thank you!

[Scott Morrison]

Or by linarith.

[Scott Morrison]

or by simp :-)

[Yufan Lou]

How come I forgot simp XD only tried trivial

[Yufan Lou]

Not trivial enough for Lean

[Scott Morrison]

(simp can only handle the case in nat; if you meant in the reals then use norm_num.)

[Yufan Lou]

Was about to say simp gave me 0 < 1 as a new goal LOL

[Yufan Lou]

Which tactic shall I use to factor C * a 2 - C * L into C * (a 2 - L)

[Yufan Lou]

eh library_search to the rescue

[Yufan Lou]

ahhhh just realized this thing requires by case cuz C = 0 C not = 0

[Johan Commelin]

I can't parse the last part of your sentence

[Yufan Lou]

by_cases C = 0 with Ceq0 gives me invalid 'begin-end' expression, ',' expected

[Yufan Lou]

while by_cases C = 0 is fine

[Johan Commelin]

by_cases hC : C = 0,

[Johan Commelin]

Yeah, the syntax is not always uniform :sad:

[Yufan Lou]

Ah OK, that just means this needs update https://leanprover.github.io/reference/tactics.html#basic-tactics

[Johan Commelin]

Ok. @Jeremy Avigad :upper_right:

[Floris van Doorn]

As posted on the issue, the quick fix for the scalar multiplication is

import analysis.normed_space.basic

attribute [instance, priority 900] algebra.has_scalar
attribute [instance, priority 800] mul_action.to_has_scalar

def lim_inf (f : ℝ → ℝ) (L : ℝ) :=
  ∀ ε > 0, ∃ N > (0 : ℝ),
    ∃ x > N, abs (f x - L) < ε

example (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (C • a) (C * L) := sorry

[Yufan Lou]

XD I see thanks

[Yufan Lou]

Well, thanks for the fix but the C • a version feels at least 10x slower than than the lambda version

[Yufan Lou]

I am sticking with the lambda version for now

[Yufan Lou]

I need this lemma as my final step but I don't know how

example (C : ℝ) (x : ℝ) (ε : ℝ) (H : ε > 0) :
∥x∥ < ∥1 / C∥ * ε → ∥C∥ * ∥x∥ < ε :=
begin
intros,
simp at *,
library_search
end

[Johan Commelin]

Yeah, those things are really annoying

[Johan Commelin]

You'll need things like norm_div and norm_nonneg and mul_lt_mul_left

[Yufan Lou]

Hmm, let me try

[Yufan Lou]

What should I import

[Johan Commelin]

I would think most of those things are already there

[Yufan Lou]

huh, I have import analysis.normed_space.basic but still unknown identifier 'norm_div'

[Johan Commelin]

src/analysis/normed_space/basic.lean:@[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=

[Johan Commelin]

You might need to prefix it with something

[Johan Commelin]

Or open a namespace

[Yufan Lou]

k

[Johan Commelin]

Are you using VScode?

[Johan Commelin]

If so, hit Ctrl-P and then type #norm_div. You'll likely see the full name of the lemma

[Yufan Lou]

found it, thank you!

[Yufan Lou]

OMGGGGG I actually finished this

[Johan Commelin]

Now go and read the wiki page on Stockholm syndrome

[Yufan Lou]

LOOOOOOOL

[Yufan Lou]

https://gist.github.com/louy2/4c5938960dd649d0e49aa53d3f56e07c

[Yufan Lou]

Comments welcome!

[Kenny Lau]

@Yufan Lou there is a proof without casing C=0

[Kenny Lau]

let should be used when the object is not Prop; otherwise use have

[Yufan Lou]

I chose let where I couldn't figure out how to use have

[Kenny Lau]

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
∀ (C : ℝ), lim_inf (λ x, C * a x) (C * L) :=
begin
  assume C : ℝ,
  unfold lim_inf at H ⊢, /- unfold definitions -/
  assume (ε : ℝ) (Hε : ε > 0),
  by_cases HC : C = 0,
  { use [1, by norm_num],
    assume (x : ℝ) (Hx : x > 1),
    rw HC, /- ∥0 * a x - 0 * L∥ < ε -/
    simpa using Hε },
  { have HinvC : C⁻¹ ≠ 0, from inv_ne_zero HC,
    have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero HinvC,
    have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
    specialize H (∥C⁻¹∥ * ε) HnCε,
    rcases H with ⟨N, HN, H⟩,
    use [N, HN],
    assume (x : ℝ) (Hx : x > N),
    specialize H x Hx,
    rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul],
    exact H }
end

[Yufan Lou]

Ah! specialize!

[Yufan Lou]

I fiddled with pattern matching for quite a while too... so rcases is the answer

[Yufan Lou]

Thank you so much!

[Johan Commelin]

You can even merge those two lines if you want

[Patrick Massot]

What's the point of all these type ascriptions? Is it for readability?

[Patrick Massot]

Why specializing right before an exact?

[Patrick Massot]

Anyway, I did a quick compression pass, maybe you'll learn something by studying:

theorem lim_inf_cons_mul_eq (a : ℝ → ℝ) (L : ℝ) (H : lim_inf a L) :
  ∀ C, lim_inf (λ x, C * a x) (C * L) :=
begin
  intros C ε Hε,
  by_cases HC : C = 0,
  { use [1, by norm_num],
    intros,
    simpa [HC] using Hε },
  { have HnC : ∥C⁻¹∥ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC),
    have HnCε : ∥C⁻¹∥ * ε > 0, from mul_pos' HnC Hε,
    rcases H (∥C⁻¹∥ * ε) HnCε with ⟨N, HN, H⟩,
    use [N, HN],
    intros x Hx,
    rw [← mul_sub, ← mul_lt_mul_left HnC, ← norm_mul, ← mul_assoc, inv_mul_cancel HC, one_mul],
    exact H x Hx }
end

[Yufan Lou]

Thanks! Yeah I had readability in mind. I want to share this with my maths friend and try to make it somewhat similar to what we would do by hand. So I wonder if the rw at the end can be done with calc.

[Johan Commelin]

@Yufan Lou In that case, you will love show

[Johan Commelin]

You can write show this = what * the * goal looks like,

[Yufan Lou]

wow what LOL I couldn't tell what's different between show and have

[Johan Commelin]

have introduces a new assumption (but you have to prove it, of course)

[Johan Commelin]

show restates the goal

[Yufan Lou]

Ahhhhhh I suspected that but didn't get it to work for some reason XD

[Yufan Lou]

"unification" :thinking: how far can I restate it

[Yufan Lou]

So far I have only read proofs where show is at the end

[Patrick Massot]

Sure you can use a calc block, ending like

[Patrick Massot]

    intros x Hx,
    calc  ∥ C * a x - C * L∥
        = ∥ C * (a x - L) ∥ : by rw mul_sub
    ... = ∥ C ∥ * ∥a x - L ∥ : norm_mul _ _
    ... < ∥ C ∥ * (∥C⁻¹∥ * ε) : mul_lt_mul_of_pos_left (H x Hx) (abs_pos_of_ne_zero HC)
    ... = ε : by rw [← mul_assoc, ← norm_mul, mul_inv_cancel HC, norm_one, one_mul] }

[Patrick Massot]

or many variation, depending where you want to split steps.

[Patrick Massot]

But this is probably not so good if you want to impress people. Really Lean should need help in all those steps. Stating the steps is ok, by tactics should then crush the proofs. @Rob Lewis is that in scope for polya?

[Yufan Lou]

That's beautiful! Thank you! I can explain that Lean can help with all those, but I feel that without showing the steps my friends would just not know what Lean is doing.

[Rob Lewis]

Rob Lewis is that in scope for polya?

Depending what you have in the context, some of it is. But this looks primarily like a rewriting problem, not an arithmetic one.

[Jeremy Avigad]

@Johan Commelin @Yufan Lou I'll make the correction to the reference manual (I didn't think anyone was using it any more, but I guess people are still finding it). It may take a little while. I have lists of corrections to deal with for TPIL and Logic and Proof as well. I just need to find an afternoon to work through them all.

[Kevin Buzzard]

Thanks! Yeah I had readability in mind. I want to share this with my maths friend and try to make it somewhat similar to what we would do by hand. So I wonder if the rw at the end can be done with calc.

@Yufan Lou if you want to make your code more appealing to your maths friends, you can try Patrick Massot's formatter. I used it to make this Lean proof of the sandwich theorem and I will be using it later on to make Lean notes for the course I am currently involved in. You click on stuff and it opens up Lean code -- click on the grey rectangles to view the tactic state at any point in the proof. In practice this just means adding a bunch of comments (in LaTeX) to your code.