Zulip Chat Archive

Stream: maths

Topic: Math education question (teaching textbook proofs in Lean)


view this post on Zulip Chris B (Oct 02 2019 at 18:58):

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!

view this post on Zulip Chris Hughes (Oct 02 2019 at 19:21):

We certainly don't worry about being constructive. Usually

view this post on Zulip Chris Hughes (Oct 02 2019 at 19:23):

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.

view this post on Zulip Johan Commelin (Oct 02 2019 at 19:40):

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

view this post on Zulip Johan Commelin (Oct 02 2019 at 19:41):

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

view this post on Zulip Patrick Massot (Oct 02 2019 at 19:52):

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

view this post on Zulip Patrick Massot (Oct 02 2019 at 19:53):

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

view this post on Zulip Chris B (Oct 02 2019 at 19:55):

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

view this post on Zulip Patrick Massot (Oct 02 2019 at 19:58):

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

view this post on Zulip Johan Commelin (Oct 02 2019 at 19:58):

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.

view this post on Zulip Chris B (Oct 02 2019 at 21:01):

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

view this post on Zulip Chris B (Oct 02 2019 at 21:03):

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

view this post on Zulip Patrick Massot (Oct 02 2019 at 21:26):

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

view this post on Zulip Chris B (Oct 02 2019 at 22:17):

Interesting, thanks for that insight.

view this post on Zulip Tim Daly (Oct 03 2019 at 02:37):

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

view this post on Zulip Jesse Michael Han (Oct 03 2019 at 03:18):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 01:19):

@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

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:06):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:07):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:14):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:16):

lol how do I express infinity in this thing

view this post on Zulip Alex J. Best (Oct 17 2019 at 02:28):

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)

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:30):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:30):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:31):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:33):

@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 R\infty \in \mathbb{R} either. So they must have explained somewhere what they mean when the abuse notation like this.

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:37):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:38):

Oh wait there is a subsection defining the infinity case separately

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:39):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:41):

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 ) < ε .

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:42):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:43):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:44):

Yep, that's right

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:52):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:52):

Also wikipedia language so redundant

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:53):

Try \|| I think

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:56):

k

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:56):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:56):

You only want the positive one

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:56):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 02:57):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:57):

oh ok! thanks for simplifying :D

view this post on Zulip Yufan Lou (Oct 17 2019 at 02:59):

\|| gives me unexpected token tho

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:00):

I still need the other abs right?

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:06):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:06):

gotcha

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:08):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:08):

missing import?

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:09):

Wouldn't think so...

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:09):

also I cannot multiply a function directly with a real LOL

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:10):

No... they are different things, right?

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:10):

You can try r \bu f

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:10):

Where r is real and f a function

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:10):

I understand LOL just musing

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:10):

oh! let me try

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:11):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:12):

unknown identifier 'normed_field' missing import it is

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:12):

/me never really works with real numbers

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:13):

import analysis.normed_space.basic fixes it

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:13):

Good

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:14):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:15):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:15):

So that explains why the import fixes it

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:15):

I see

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:16):

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

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:17):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:17):

limnCan=Climnan for CR\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

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:18):

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.

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:18):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:18):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 03:20):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:21):

That fixes it

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:23):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:24):

:sweat: hopefully it's not something too complicated

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:24):

meanwhile I'll continue with my proof I think

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:31):

LOL how to prove 1 > 0

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:32):

@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

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:32):

by norm_num.

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:33):

Ah Thank you!

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:33):

Or by linarith.

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:33):

or by simp :-)

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:34):

How come I forgot simp XD only tried trivial

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:34):

Not trivial enough for Lean

view this post on Zulip Scott Morrison (Oct 17 2019 at 03:34):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:35):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:50):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 03:57):

eh library_search to the rescue

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:07):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 06:11):

I can't parse the last part of your sentence

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:14):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:16):

while by_cases C = 0 is fine

view this post on Zulip Johan Commelin (Oct 17 2019 at 06:16):

by_cases hC : C = 0,

view this post on Zulip Johan Commelin (Oct 17 2019 at 06:17):

Yeah, the syntax is not always uniform :sad:

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:17):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 06:18):

Ok. @Jeremy Avigad :upper_right:

view this post on Zulip Floris van Doorn (Oct 17 2019 at 06:20):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:25):

XD I see thanks

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:31):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 06:31):

I am sticking with the lambda version for now

view this post on Zulip Yufan Lou (Oct 17 2019 at 07:17):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:21):

Yeah, those things are really annoying

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:22):

You'll need things like norm_div and norm_nonneg and mul_lt_mul_left

view this post on Zulip Yufan Lou (Oct 17 2019 at 07:27):

Hmm, let me try

view this post on Zulip Yufan Lou (Oct 17 2019 at 07:27):

What should I import

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:27):

I would think most of those things are already there

view this post on Zulip Yufan Lou (Oct 17 2019 at 07:28):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:30):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:30):

You might need to prefix it with something

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:30):

Or open a namespace

view this post on Zulip Yufan Lou (Oct 17 2019 at 07:30):

k

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:30):

Are you using VScode?

view this post on Zulip Johan Commelin (Oct 17 2019 at 07:31):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 07:32):

found it, thank you!

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:01):

OMGGGGG I actually finished this

view this post on Zulip Johan Commelin (Oct 17 2019 at 08:02):

Now go and read the wiki page on Stockholm syndrome

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:03):

LOOOOOOOL

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:07):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:08):

Comments welcome!

view this post on Zulip Kenny Lau (Oct 17 2019 at 08:22):

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

view this post on Zulip Kenny Lau (Oct 17 2019 at 08:25):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:31):

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

view this post on Zulip Kenny Lau (Oct 17 2019 at 08:33):

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 (ε : ) ( : ε > 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  },
  { 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 ,
    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

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:36):

Ah! specialize!

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:37):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:37):

Thank you so much!

view this post on Zulip Johan Commelin (Oct 17 2019 at 08:48):

You can even merge those two lines if you want

view this post on Zulip Patrick Massot (Oct 17 2019 at 08:54):

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

view this post on Zulip Patrick Massot (Oct 17 2019 at 08:54):

Why specializing right before an exact?

view this post on Zulip Patrick Massot (Oct 17 2019 at 08:54):

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 ε ,
  by_cases HC : C = 0,
  { use [1, by norm_num],
    intros,
    simpa [HC] using  },
  { have HnC : C⁻¹ > 0, from abs_pos_of_ne_zero (inv_ne_zero HC),
    have HnCε : C⁻¹ * ε > 0, from mul_pos' HnC ,
    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

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:58):

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.

view this post on Zulip Johan Commelin (Oct 17 2019 at 08:58):

@Yufan Lou In that case, you will love show

view this post on Zulip Johan Commelin (Oct 17 2019 at 08:59):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 08:59):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 09:00):

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

view this post on Zulip Johan Commelin (Oct 17 2019 at 09:01):

show restates the goal

view this post on Zulip Yufan Lou (Oct 17 2019 at 09:03):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 09:05):

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

view this post on Zulip Yufan Lou (Oct 17 2019 at 09:05):

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

view this post on Zulip Patrick Massot (Oct 17 2019 at 09:16):

Sure you can use a calc block, ending like

view this post on Zulip Patrick Massot (Oct 17 2019 at 09:16):

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

view this post on Zulip Patrick Massot (Oct 17 2019 at 09:16):

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

view this post on Zulip Patrick Massot (Oct 17 2019 at 09:18):

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?

view this post on Zulip Yufan Lou (Oct 17 2019 at 09:34):

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.

view this post on Zulip Rob Lewis (Oct 17 2019 at 09:40):

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.

view this post on Zulip Jeremy Avigad (Oct 17 2019 at 13:07):

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

view this post on Zulip Kevin Buzzard (Oct 17 2019 at 22:10):

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.


Last updated: May 10 2021 at 08:14 UTC