is this normal?

Stream: lean4

[Joseph O]

I have this theorem

theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b := by
  induction b
  { simp }
  {
    rw [add_succ]
    repeat {rw [mul_succ]}
  }

and when i put my cursor on line repeat {rw [mul_succ]}, i get the error
image.png
but when I place it on the next line, I get the message goals accomplished
image.png
is this normal?

[Joseph O]

what does it mean?

[Horatiu Cheval]

I think that in contrast to Lean 3, in Lean 4 one writes tactic combinators with parentheses:repeat (rw [mul_succ])

[Arthur Paulino]

The brackets can be used if you want to be explicit that a goal can be closed with the tactics within them

[Horatiu Cheval]

Though in this case

open Nat

theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b := by
  induction b
  { simp }
  {
    rw [add_succ]
    repeat (rw [mul_succ])
    /-
    case succ
    t a n✝ : Nat
    n_ih✝ : t * (a + n✝) = t * a + t * n✝
    ⊢ t * (a + n✝) + t = t * a + t * succ n✝
    case succ
    t a n✝ : Nat
    n_ih✝ : t * (a + n✝) = t * a + t * n✝
    ⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)
    case succ
    t a n✝ : Nat
    n_ih✝ : t * (a + n✝) = t * a + t * n✝
    ⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)
    -/
  }

we get 3 goals after the repeat which still doesn't seem right.

[Joseph O]

Hmm, that doesnt seem right either. Im trying to translate

lemma left_distrib (t a b : nat) : t * (a + b) = t * a + t * b :=
begin
  induction b with d hd,
  {
    simp,
  },
  {
    rw add_succ,
    repeat {rw mul_succ},
    rwa [hd, ←add_assoc],
  }
end

[Horatiu Cheval]

open Nat

theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b :=
by
  induction b
  case zero =>
    simp
  case succ d hd =>
    rw [add_succ]
    repeat (rw [mul_succ])
    rw [hd, ←Nat.add_assoc]

[Joseph O]

Oh i I wasnt aware of the new syntax.

[Joseph O]

You opened Nat, so why do you have to do Nat.add_assoc?

[Horatiu Cheval]

I got uknown identifier without the Nat.. I don't really understand why

[Arthur Paulino]

This is also valid syntax:

open Nat

theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b :=
by
  induction b with
  | zero => simp
  | succ d hd =>
    rw [add_succ]
    repeat (rw [mul_succ])
    rw [hd, ← Nat.add_assoc]

[Joseph O]

wow thank you

[Joseph O]

Which is more used?

[Arthur Paulino]

Maybe it's too early to talk about "more used". I, personally, use the one I posted more often. But it's a personal preference

[Kyle Miller]

By the way, simp [mul_succ] is sort of like repeat (rw [mul_succ]). You can collapse the second case of the induction into a single simp too.

theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b :=
by
  induction b with
  | zero => rfl
  | succ d hd => simp only [add_succ, mul_succ, hd, Nat.add_assoc]

I did simp only to emphasize that simp is using only these lemmas.

[Arthur Paulino]

And the fact that add_assoc couldn't be found after open Nat is likely a bug. Should we ping a core dev?

[Kyle Miller]

Horatiu Cheval said:

I got uknown identifier without the Nat.. I don't really understand why

It's because Nat.add_assoc is a protected theorem.

[Kyle Miller]

I think it's because mathlib4 defines a general add_assoc in the top-level namespace. (docs4#add_assoc)

[Arthur Paulino]

I didn't know protected prevented declarations from being accessed directly after open. Thanks Kyle!

[Joseph O]

Kyle Miller said:

By the way, simp [mul_succ] is sort of like repeat (rw [mul_succ]). You can collapse the second case of the induction into a single simp too.

theorem left_distrib (t a b : Nat) : t * (a + b) = t * a + t * b :=
by
  induction b with
  | zero => rfl
  | succ d hd => simp only [add_succ, mul_succ, hd, Nat.add_assoc]

I did simp only to emphasize that simp is using only these lemmas.

did you get rid of the arrow before add_assoc because simp does that for you?
could you do something similar to this in lean 3?

[Kyle Miller]

Oh, no, it's just that you're able to prove it by doing reassociation in either direction (this works too simp only [add_succ, mul_succ, hd, ← Nat.add_assoc]). I think I just forgot to copy the arrow.

[Joseph O]

does lean 3 have simp only?

[Leonardo de Moura]

Joseph O said:

You opened Nat, so why do you have to do Nat.add_assoc?

Nat.add_assoc is protected
https://leanprover.github.io/theorem_proving_in_lean4/interacting_with_lean.html?highlight=protected#more-on-namespaces

[Joseph O]

why is it protected though?

[Jireh Loreaux]

Because there are lots of other lemmas we would like to call add_assoc (even one in the root namespace I think). If it weren't protected, then whenever you opened Nat, then all of a sudden add_assoc would be ambiguous, and you would have to use qualified names anyway Nat.add_assoc and (worse) for the root namespace one, _root_.add_assoc.