terminology for parts of a lean proof

Stream: new members

[rzeta0]

I'm a beginner so forgive the basic question about terminology:

-- 01 - First Proof by Calculation
import Mathlib.Tactic

example {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 := by
    calc
        y = x + 4 := by rw [h1]
        _ = 3 + 4 := by rw [h2]
       _ = 7 := by norm_num

Questions:

1. Is example the name of the theorem we're proving (noting example is a special case)?
2. Is the next section {x y : ℝ} called a type declaration?
3. Is calc a strategy?
4. I guess by rw and by num_norm are called tactics.
5. UPDATE: is the section after := by called a justification?

I'm creating tutorials as I learn myself, and would like to know what the official naming of these things are.

[Filippo A. E. Nuccio]

Well, example is somewhat unique: if your code were

-- 01 - First Proof by Calculation
import Mathlib.Tactic

lemma foo{x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 := by
    calc
        y = x + 4 := by rw [h1]
        _ = 3 + 4 := by rw [h2]
       _ = 7 := by norm_num

then we would say that foo is the name of the lemma, because actually it is the name of the term in the type y=7 that you are producing (in the context {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3).

[Filippo A. E. Nuccio]

For example we are producing an "unnamed" term.

[Filippo A. E. Nuccio]

A type declaration is x: ℝ: it declares thatx is a term of type $\mathbb{R}$.

[Filippo A. E. Nuccio]

In that example x and y are called "implicit variables": the fact that they are implicit comes from them living between curly braces, and it affects the way the lemma foo will be used. So all in all {x y : ℝ} are implicit variables declared to be of type ℝ.

[Filippo A. E. Nuccio]

3. : calcis a "mode" (sometimes an "environment"): the two main other modes are "tactic mode" and "term mode". These are ways to make lean produce terms of the required type. See here.
4. Yes, both rw and num_norm are tactics
5. That section is called a proof, normally.

[rzeta0]

thanks Filippo- I will need to read further about "modes"

also - what is the name given to the symbol/syntaxc := ... is it called a justification marker?

[Markus Schmaus]

4. rw and num_norm are called tactics,by is a keyword which starts tactic mode, just like calc is a keyword which starts calc mode.
5. everything after := is called the proof. By default you start out in term mode, by then start the tactic mode, and calc then starts the calc mode.

[rzeta0]

hi @Markus Schmaus - so in the given example :

lemma foo{x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 := by
    calc

... it seems like by starts tactic mode, but is immediately overridden by calc which starts calc mode. Does this mean by was not necessary?

if everything after := is a proof, then are the per-line := sub-proofs proving or justifying whatever equality/relation is immediately to their left?

[Ruben Van de Velde]

calc is both a mode and a tactic, just to confuse you :)

[Ruben Van de Velde]

And yes, in calc, you have a ~ b := proof that a ~ b

[Markus Schmaus]

I don't think there is a standard way to directly go from term mode to calc mode, so the by is necessary, but it would be quite easy to make a macro that directly goes to calc mode.

rzeta0 said:

if everything after := is a proof, then are the per-line := sub-proofs proving or justifying whatever equality/relation is immediately to their left?

Yes, these are proofs for the equality to the left. They are currently all done in tactic mode, but at least the first line could also be directly proven in term mode:

import Mathlib.Tactic

lemma foo{x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 := by
    calc
        y = x + 4 := h1
        _ = 3 + 4 := by rw [h2]
        _ = 7 := by norm_num

That's because h1 is the proof for y = x + 4, and therefore can directly be used to proof y = x + 4 again.

[Ruben Van de Velde]

Try

import Mathlib.Tactic

lemma foo{x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 :=
    calc
        y = x + 4 := h1
        _ = 3 + 4 := by rw [h2]
        _ = 7 := by norm_num

[Ruben Van de Velde]

No by necessary

[Markus Schmaus]

I stand corrected. I thought I tried that, but I must have had a typo somewhere.

[rzeta0]

Ruben, Marcus - so for a beginner like me, one of the challenges is to avoid getting sucked into what is "possible" due to the idiosyncrasies of the syntax (think C++) - and maintaining focus on good idiomatic structures.

So for this example, like so many I have seen in beginner tutorials, should we say that by should always be there at the end of the line that initiates a proof?

As I say, every example I have seen has a by at the end of the first line.

[Markus Schmaus]

I have been a beginner myself not so long ago and in many ways I still am. I would argue that understanding how tactic mode and term mode relate to each other is essential for understanding Lean works, so you have an easier time writing your own proofs.

Have a look at the following simple proof, which I copied from here.

namespace Nat
protected theorem sub_lt_left_of_lt_add' {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m := by
  have := Nat.sub_le_sub_right (succ_le_of_lt h) n
  rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this

have introduces an auxiliary hypothesis, which is proven by Nat.sub_le_sub_right (succ_le_of_lt h) n in term mode without by.

The tradeoff between tactic and term mode is roughly this: In term mode you specify the proof precisely, so Lean can often infer the type of the proof, i.e. the statement it proves. If you have specified the statement, you can use tactic mode to have Lean find the proof semi-automatically. Since theorems have to include the statement, proofs for theorems typically use tactic mode, the same is true for lines in a calc proof.

[Bbbbbbbbba]

rzeta0 said:

Ruben, Marcus - so for a beginner like me, one of the challenges is to avoid getting sucked into what is "possible" due to the idiosyncrasies of the syntax (think C++) - and maintaining focus on good idiomatic structures.

So for this example, like so many I have seen in beginner tutorials, should we say that by should always be there at the end of the line that initiates a proof?

As I say, every example I have seen has a by at the end of the first line.

As far as the compiler is concerned, you have quite some freedom where to put by:

example {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 := by norm_num [h1, h2]

example {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 :=
  by norm_num [h1, h2]

However most proofs I encounter with any sort of complexity are tactic proofs, so putting by at the end of the first line is a very reasonable style rule.

[Patrick Massot]

rzeta0 said:

I'm creating tutorials as I learn myself, and would like to know what the official naming of these things are.

I think that writing tutorials so early in your learning process is a very dangerous thing to do, unless you keep them on your hard drive to make sure nobody else read them.

[rzeta0]

(deleted)

[Kyle Miller]

On the other hand, sometimes tutorials are best written by a newcomer since newcomers are seeing everything with fresh eyes. Paired with someone who knows the system and can edit it to avoid incorrect things, it could be useful to others.

This never stopped people from writing monad tutorials for Haskell though :-) https://wiki.haskell.org/Monad_tutorials_timeline (I think I too wrote a monad tutorial at some point, but it didn't make the list.)

[Martin Dvořák]

Kyle Miller said:

https://wiki.haskell.org/Monad_tutorials_timeline

Maybe, if I read all of them, I will finally understand what a monad is (I have already "learnt" about monads circa 6 times and yet I still don't know what a monad is).

[llllvvuu]

Given that millions of JavaScript programmers use async/await (do notation) and Promise.then (de-sugared monadic bind) daily without issue, it makes me wonder whether monad tutorials are cursed and should be avoided.

[Patrick Massot]

I’m sorry my comment was too strong. rzeta0, you should of course feel free to write whatever you want, although warning readers would probably be nicer.

[Mauricio Collares]

llllvvuu said:

Given that millions of JavaScript programmers use async/await (do notation) and Promise.then (de-sugared monadic bind) daily without issue, it makes me wonder whether monad tutorials are cursed and should be avoided.

Writing them is still very educational for the author! But I agree with https://byorgey.wordpress.com/2009/01/12/abstraction-intuition-and-the-monad-tutorial-fallacy/

[Michael Rothgang]

Bbbbbbbbba said:

rzeta0 said:

Ruben, Marcus - so for a beginner like me, one of the challenges is to avoid getting sucked into what is "possible" due to the idiosyncrasies of the syntax (think C++) - and maintaining focus on good idiomatic structures.

So for this example, like so many I have seen in beginner tutorials, should we say that by should always be there at the end of the line that initiates a proof?

As I say, every example I have seen has a by at the end of the first line.

As far as the compiler is concerned, you have quite some freedom where to put by:

example {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 := by norm_num [h1, h2]

example {x y : ℝ} (h1 : y = x + 4) (h2 : x = 3) : y = 7 :=
  by norm_num [h1, h2]

However most proofs I encounter with any sort of complexity are tactic proofs, so putting by at the end of the first line is a very reasonable style rule.

Also, the style guide to mathlib (in Lean 4) mandates putting by at the end of first line; this might be why many projects also follow this.

[rzeta0]

is this the style guide you're referring to?

https://leanprover-community.github.io/contribute/style.html