correct use of `by`

Stream: new members

[rzeta0]

I'm sorry to ask this question again but I remain confused.

I do understand the use of by when using tactics, such as := by ring or := by norm_num.

But I don't understand why some examples online do and don't have by at the end of the first line of the proof (the theorem statement - name, variable types, hypothesis, overall proof goal).

The following proof generates no warnings or errors:

import Mathlib.Tactic

example {a: ℕ} (h1: a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

Removing the by also generates no warnings or errors:

import Mathlib.Tactic

example {a: ℕ} (h1: a = 4) : a > 1 :=
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

Perhaps the following questions will help resolve my confusion:

• When is it ok not to have by after a := ?

• Is it considered good or ok practice to always use by after a := ?

[Julian Berman]

The thing which never changes is by means "enter tactic mode". So the things that work after it are tactics, until/unless you exit tactic mode and enter some other one. Let's take term mode as another mode -- that's the mode you start in without writing by. The confusing thing is that some words exist both as tactics as well as terms. So by calc ... is a tactic called calc. Without by, there is a term calc which has very similar syntax. The same is true of have and some other tactics -- there is both a tactic and a term with quite similar syntax.

[Julian Berman]

The style guide (https://leanprover-community.github.io/contribute/style.html#tactic-mode) doesn't seem to really opine on how much one should prefer tactic mode, though here on Zulip I know there are a few previous threads I think on the subject, and different people have different preferences on how much they like one or the other. I think starting out it's probably fine to always start with by, you certainly can always remove it if your proof ends up being so short/simple that it makes sense to turn into a term mode proof.

[Julian Berman]

Perhaps to contrast, some tactics do not have term-mode equivalents, at least not with the same syntax. rw is an example of this ... := rw foo does not work. (However, there actually is term-mode functionality for something like rw, it just has different syntax; it's calledEq.subst and/or what you get from typing \t)

[Kyle Miller]

The calc term is also a tactic so that you don't have to write refine calc ... or exact calc ... to use it.

[rzeta0]

Thanks Julian and Kyle. I think I need to know more about "term mode" and "tactic mode" before I can finally crack this one. Hopefully it will resolve itself as I work through the tutorial "Mechanics of Proof".

[Jon Eugster]

I think rfl is also a very well-known example where there is a term and a tactic with identical name, so := by rfl uses the tactic while := rfl and := by exact rfl use the term. All three ways do apriori slightly different things but in practise you can mostly use any of the three proofs interchangeably.

[rzeta0]

Thanks Jon. I'm a fan of the principle of "least surprise" and "preferably one way to do it" in programming language design. I wonder to what extent this is a priority for the lean/mathlib designers?

[Damiano Testa]

Since quite a few of the operations that proof-checking involves are undecidable, there are various heuristics that Lean uses to try to get what it is that you might mean when you say something like rfl. Depending on whether you say rfl, by exact rfl or by rfl you are skewing slightly these heuristics.

From this perspective, I would say that the principle of least surprise is that you see rfl in all cases. The detail of which version of rfl works in your situation is often irrelevant, but sometimes gives you an extra edge.

[Jon Eugster]

Indeed, this is completely by design: you are expected to create a proof term which has the correct type, and := rfl is exactly that. However, in any serious proving it will be way to hard to construct such a term by hand. Therefore we have tactics, which are basically programs that create such a proof term.

For tactics, the "one - and preferably only one - obvious way to do it" mentality doesn't fully apply. Rather you have tons of different tools that might help you in specific cases. For simple problems, you can often choose which tool you use. You could compare that to trying to compute some inverses of matrices or something (e.g. in Python): There might be a general-purpose algorithm, but depending on what you know about your matrix there might be much more efficient and cleaner algorithms to use, so you do want to have a selection of these algorithms available.

[Mark Fischer]

rzeta0 said:

Thanks Julian and Kyle. I think I need to know more about "term mode" and "tactic mode" before I can finally crack this one. Hopefully it will resolve itself as I work through the tutorial "Mechanics of Proof".

My feeling is that you have the right of it. The more you use them, the more they will start to distinguish themselves and make sense. Many tactics ask for one or more terms and terms may have proofs within them which are best solved with a tactic. I've learn to switch between them as I go.

rzeta0 said:

I'm a fan of the principle of "least surprise" and "preferably one way to do it" in programming language design.

Part of Lean's design is to have a small, hopefully bug-free core and then language extensions and such built ontop of this. This is a good way to maintain confidence that if a proof type-checks it isn't due to a bug, but it means "more than one way to do things," is going to be common.

A common idiom in Lean is that collaborators let you get away with omitting parts of your code. For example, if Lean can infer the type of a variable, then it's up to you whether you want to include the type ascription. Sometimes including extra detail makes it easier to read/maintain code and sometimes it's clutter that does the opposite (where that line is seems to be a matter of taste).

As I understand it, for Lean all builtin syntax is parsed and processed using the same mechanisms and APIs open to users. This means some pretty powerful extensibility capabilities are available. Domain Specific Languages like Do-notation and string interpolation are embedded into Lean using Macros this way. Which, in effect, means you can use these DSLs or write out the code these DSLs would expand to yourself - meaning there are suddenly multiple ways to do the same thing.

The principles of language design you mentioned are (to some extent) sort of lifted to the preferences of the various communities using Lean. I do feel like cohesiveness with the extensions that are adopted is valued by the core/mathlib devs.

[Jason Rute]

This is also being discussed on this PA.SX question (and another question that was marked as a duplicate). Given that this is also asked here, maybe it is a complicated and difficult to understand topic. If there is a clearer explanation discover here, feel free to add another answer on PA.SX.