When is the lean 4 "by" required?

Question

I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally omitted.

For example, it works both with and without by here:

example : 1 + 1 = 2 := sorry
example : 1 + 1 = 2 := by sorry

But for other tactics, it only works with the by:

example : 1 + 1 = 2 := by ring

without the by, it didn't work:

example : 1 + 1 = 2 := ring

The hover hint says:

by tac constructs a term of the expected type by running the tactic(s) tac.

But it is not informational enough for me to understand why it is required some times while not in other occasions.

When is the by required?

I am more interested in this from the perspective of a math learner (who does not know much about programming), not a computer scientist's view about terms and types. In doing a proof, when should one say "by some tactic" versus just "some tactic".

Answer 1

To complement the other answer, by is used to start tactic mode proofs (from inside term mode). The most common setting for this is in a top-level theorem such as:

theorem n_plus_m_eq_m_plus_n (n m : Nat) : n + m = m + n := by
  -- now in tactic mode
  simp  -- apply tactic simp

However, there are a number of more subtle situations where := is also used to start a proof and by is needed to write tactics. Without the by, then one would be giving a term proof instead of a tactic proof.

example : True := by
  -- tactic mode
  have h0 : True ∨ False -> True := by
    -- this is a tactic proof inside a tactic proof
    intro h
    trivial
  -- back to outer tactic block
  have h1 : True ∨ False :=
    -- this is a term proof (inside a tactic proof)
    Or.inl True.intro
  -- back to outer tactic block
  apply h0
  exact h1

example : 1 + 2 = (1 * 1)  + (1 + 1) := by
  -- in tactic mode, but we didn't have to be since calc also works in term mode
  calc
    1 + 2 = 1 + (1 + 1) := by
      -- in tactic mode inside calc block inside tactic mode
      rfl  -- rfl the tactic
    _     = (1 * 1) + (1 + 1) :=
      -- in term mode inside calc block inside tactic mode
      rfl  -- rfl the term

Advanced

An advanced application is where one goes into tactic mode in the middle of a term proof. It is rare, but one case is where one starts with a match or recursion like the following:

theorem foo : (n : Nat) -> (n = 0 ∨ n > 0)
| 0 => by
  -- tactic mode inside recursion
  simp
| n+1 =>
  -- term mode inside recursion
  Or.inr (Nat.zero_lt_succ n)

But here are some more cases where I've seen this sort of thing:

example : ∀ (n : Nat),  n + 1 = 1 + n :=
  -- term proof
  fun n => by
    -- entering tactic mode in the middle of a term proof
    simp [Nat.add_comm]

This is sort of a dumb example. It would be better to do the whole thing in tactic mode with intro n at the start.

Sometimes by is nice for making an inline lemma on the spot.

example : ∀ (n : Nat), n + 0 = 0 + n := by
  -- tactic mode
  intro n
  -- normally put 
  -- here I'm applying rw with the term (Nat.add_zero n)
  rw [Nat.add_zero n]
  -- here I'm applying rw with the term `(by simp : (∀ n : Nat, 0 + n = n))`
  -- this is going into tactic mode and using `simp` to prove the goal `∀ n : Nat, 0 + n = n`
  rw [(by simp : (∀ n : Nat, 0 + n = n))]

Finally, as for the foo example above, here is one way to write it in tactic mode. Note we don't use by to give the subproofs. We are still in tactic mode.

theorem foo' (n : Nat) : (n = 0 ∨ n > 0) := by
  -- tactic mode
  induction n with
  | zero => 
    -- no `by` required here.  Still in tactic mode.
    simp
  | succ n ih =>
    -- no `by` required here.  Still in tactic mode.
    simp

How to know if you are in tactic mode or term mode?

If you see a goal in the info view, you are likely in tactic mode. If you don't but do see a goal if you write _, then you are in term mode.

You can also write tactics like done. If it says "unknown identifier done" then you are in term mode. Otherwise, if it tells you you have unsolved goals, you are in tactic mode.

Answer 2

by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. sorry is a good example: it is both a syntactically valid tactic and a valid expression. They serve the same purpose, and Lean is setup this way so that you can always use sorry no matter the context, but they should not be confused. When you use sorry as an expression, it's, well, an expression, just like true or 3 + 4. When you use it as a tactic, it's a piece of program whose purpose is to generate a piece of a proof.

From a mathematician perspective, you should always use by unless you have a good reason not to.

To expand on Jason Rute's comment,

• The rfl expression is like Eq.refl a (which is a proof of a = a), except that the a is implicitly figured out by Lean. The rfl tactic (that is, the one you have when you do by rfl), on the other hand, is a bit more general. It tries to match the current goal with things that "look like" that should be closed by "reflexivity", which includes goals like a = a, but also P ↔ P.
• The sorry expression is a macro that essentially just produces a proof (or any value, really) for anything, based on a postulated axiom sorryAx. It's a macro, and not just a plain value, because it also setup things so that error reporting is a little bit better, but you can really think of it just as a value with any type. The sorry tactic, on the other hand, is simply a shorthand for exact sorry. So when you do by sorry, it's really the same thing as just sorry.
• as for calc, I'm not exactly sure why there would be an expression version, but, as far as I understand it, it's pretty much equivalent to its tactic counterpart.