some general beginner questions

Stream: new members

[Miek Messerschmidt]

I'm trying out LEAN for the first time and I'm very interested. I'm a functional analyst, so fine with math. I'm a quite accomplished Python coder, so not new to (imperative) programming.

After some weeks of reading up on how dependent type theory works and watching proofs on the Xena project youtube channel, I thought to try to prove 1+2+3+...+n = n*(n+1)/2 by induction using LEAN without any help, but got stuck at the steps that are obvious to humans, e.g., finding proofs of simple equalities like

N * (N - 1) + 2*N = N *(N +1) with N : nat.

Is there any advice on overcoming such trivial and mathematically uninteresting roadblocks? My question is maybe more general than "which are the one or two tactics to use in this situation?", but perhaps rather:

1) How should I approach learning what will be useful and where to find it, or how to produce something useful myself, when 'suggest' and 'library_search' or an obvious rewrite fails to produce anything?

2) How does a beginner understand what a tactic actually does when its source code is a bit opaque to the beginner? If I'm more interested in getting on with the math, are the inner workings important to understand? E.g. encountering "exact congr_fun rfl" is easy to understand if you have a basic understanding of the type theory poke around in the source a bit, but something like what EXACTLY "linarith" does is harder to understand, but perhaps not as important.

3) How should one approach reading LEAN and writing LEAN for readability? I struggle sometimes to 'see the math' in LEAN code. E.g., Say a human wants to understand the mathematics in a formal proof written in LEAN with all comments deleted? I assume in practice that it will be far easier to step through a proof with the LEAN infoview than to try to only use ONLY the source code itself.

[Riccardo Brasca]

I would say the best thing is what you are already doing: trying to formalize simple results, getting stuck (we've all been there!) and asking for help. Hare you tried the natural number game?

[Riccardo Brasca]

In your specific example, you can try ring that may be close the goal immediately (ring should automatically do simple computations like this), or using a chain of rw. For example rw mul_add it's a start.

[Mario Carneiro]

You probably shouldn't try to read the implementation of complicated tactics like linarith, at least until you are quite skilled at reading lean code. Much better to read the tactic documentation: tactic#linarith

[Anne Baanen]

Welcome! Indeed, figuring out how to easily do the obvious is still the biggest challenge for me, and I'd say I'm pretty experienced with Lean :)

[Anne Baanen]

1. Generally my process for finding relevant results is library_search/suggest → simp? → search for useful-sounding strings → ask on the #Is there code for X? stream: simp? will sometimes tell you how to rephrase your goal in a way that the library is more useful for. And code search is more powerful than I initially expected since we use a very predictable naming scheme. So for your goal n * (n - 1) I'd try searching for "mul_sub_one" and "mul_pred" (no results unfortunately).

[Mario Carneiro]

the key point to understanding what it can do is the line "linarith should prove any goal that is true in the theory of linear arithmetic over the rationals". That's a bit of jargon but it means that linarith can prove things like x + y < z -> x < 2 -> 2 + y < z

[Anne Baanen]

2. Mathlib is unfortunately written in a style that makes it harder than necessary for beginners. When I want to understand how to use an area of the library, I'll just go through the statements and ignore the proofs, then later come back and see how specific things are done. Sometimes there are nicely-structured proofs but often we just want to finish it as quickly as possible.

[Riccardo Brasca]

Also, beware that working with expressions like n*(n-1)/2, for n : nat can be very frustrating . Try to avoid statement involving division of natural/integer numbers.

[Anne Baanen]

Riccardo Brasca said:

Also, beware that working with expressions like n*(n-1)/2, for n : nat can be very frustrating . Try to avoid statement involving division of natural/integer numbers.

This kind of advice can sometimes be found in the module documentation at the top of files. And sometimes it's a bit of community wisdom that you just have to be around long enough to pick up.

[Mario Carneiro]

Another good decision procedure to have under your belt is the ring tactic, which handles equations over a commutative ring or semiring. This is the closest thing to your goal, so that's what I would try, but as Riccardo says the subtraction and division will cause problems because they are not ring operations (subtraction on nat saturates on underflow), so a reasonable approach to proving the theorem is to first get rid of these operations using lemmas about subtraction and division, and then once everything is + and * then ring will finish the goal

[Yaël Dillies]

In that case I'd
Riccardo Brasca said:

Also, beware that working with expressions like n*(n-1)/2, for n : nat can be very frustrating . Try to avoid statement involving division of natural/integer numbers.

In that case, I'd advise using docs#nat.asc_factorial

[Anne Baanen]

Since the statement includes subtraction only in N - 1, I'd handle n = 0 as a special case, giving something like:

import tactic

example (N : ℕ) : N * (N - 1) + 2*N = N *(N +1) :=
by cases N; simp; ring