Understanding calc Mode Behavior with rw in Lean

Stream: new members

[ChenW]

Hi, I'm new to Lean and currently learning from the book Mathematics in Lean. I encountered some confusion while working with the calc mode in the following examples:

import Mathlib.Algebra.Group.Basic
theorem test1 {a : ℕ} : a + 0 = a := calc   a + 0 = a := by rw [Nat.add_zero]
theorem test2 {a : ℕ} : a = a + 0 := calc   a = a + 0 := by rw [Nat.add_zero]
theorem test3 {a : ℕ} : a = a + 0 := calc   a = a + 0 := by rw [← Nat.add_zero]

Both test1 and test2 are accepted by Lean, but test3 is rejected. This is confusing because I expected Nat.add_zero to be applicable in reverse when switching the left and right sides of the equation using ←.

Could someone explain why test2 works but test3 does not? Is there a specific behavior of calc or rw that causes this?

[Kevin Buzzard]

Not a specific answer to your question but in general calc expects proofs to be more than one line long, because there is no point entering calc mode to prove A = B if all you're then going to do is to prove A = B directly; calc is a tool enabling users to formalize proofs of the form "$A=B$ because $A=C$ and $C=D$ and $D=B$". So my advice is not to worry about this at all and ask about calc only if you're using it "properly" i.e. have some future "_ = B line in your proof. I've seen other users confused with calc mode for one-line proofs and the short answer is "best not to do it rather than worrying about making it work, it wasn't designed to work like that".

[Kevin Buzzard]

Actually this is not the issue, because this also fails:

import Mathlib.Algebra.Group.Basic

theorem test3 {a : ℕ} : a = a + 0 := calc
  a = a := by rfl
  _ = a + 0 := by rw [← Nat.add_zero]

so my diagnosis is incorrect. The error is

tactic 'rewrite' failed, pattern is a metavariable
  ?n
from equation
  ?n = ?n + 0
a : ℕ
⊢ a = a + 0

[Kevin Buzzard]

Oh I see. So the issue is that rw [← Nat.add_zero] means "change ? to ? + 0" and Lean's response is "oh come on, how am I expected to guess what you mean by ?? You could mean the first a, the second a, the 0, the a + 0..."

[Kevin Buzzard]

When you rw [Nat.add_zero] you're asking Lean to find ? + 0 and there's only one of those in the goal, so this is a reasonable request. Is looks like Lean point blank refuses to do a rewrite if you give absolutely no information about which term you want to transform (other than its type).

[Samuel Yin]

I'm sorry if this is not really the orginial question, but this reminds me of a question about calc

I know that

example (x:ℤ) (h: 1 < x) : (2:ℝ) ≤ x := by norm_cast

should be the right way, but I'm still curious about why the following gives me an error:

example (x:ℤ) (h: 1 < x) : (2:ℝ) ≤ x := by
  calc
  _ = (2:ℤ) := by rfl
  _ ≤ _ := by norm_cast

but this is ok:

example (x:ℤ) (h: 1 < x) : (2:ℝ) ≤ x := by
  calc
  (2:ℝ) = (2:ℤ) := by rfl
  _ ≤ _ := by norm_cast

[ChenW]

Kevin Buzzard said:

When you rw [Nat.add_zero] you're asking Lean to find ? + 0 and there's only one of those in the goal, so this is a reasonable request. Is looks like Lean point blank refuses to do a rewrite if you give absolutely no information about which term you want to transform (other than its type).

Thank you for your answer! My original question was actually a simplified version of a more complex scenario. I hoped the simplified problem would reveal the same issue, but it seems not. Here’s the original code:

import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Real.Basic


variable {R : Type*} [Ring R]


-- Works
theorem t1 {a b c : R} (h : a + b = a + c) : b = c := calc
  b = b + 0 := by rw [add_zero]
  _ = b + (a + -a) := by rw [add_neg_cancel]
  _ = (c + a) + -a := by rw [← add_assoc, add_comm b a, h, add_comm a c]
  _ = c := by rw [add_assoc, add_neg_cancel, add_zero]

-- Works
theorem t2 {a b c : R} (h : a + b = a + c) : b = c := by
  rw [← add_zero b, ← add_neg_cancel a, ← add_assoc, add_comm b a, h, add_comm a c, add_assoc, add_neg_cancel, add_zero]

-- Failed
theorem t3 {a b c : R} (h : a + b = a + c) : b = c := calc
  b = b + 0 := by rw [← add_zero b]
  -- Error occurs 👆: unsolved goals ...|- b + 0 = b + 0 + 0
  _ = b + (a + -a) := by rw [add_neg_cancel]
  _ = (c + a) + -a := by rw [← add_assoc, add_comm b a, h, add_comm a c]
  _ = c := by rw [add_assoc, add_neg_cancel, add_zero]

In both t2 and t3, I intend to tell Lean, "Please find b + 0 = b using add_zero and apply the equation in reverse." However, Lean fails in t3. The error indicates unresolved goals even though the reverse application of add_zero works perfectly fine in t2.

This makes me wonder if there are specific rules about the use of ← with calc mode. Could you clarify this behavior? Is there something I might be missing about how calc handles rewrites compared to standard proof scripts?

[ChenW]

Kevin Buzzard said:

When you rw [Nat.add_zero] you're asking Lean to find ? + 0 and there's only one of those in the goal, so this is a reasonable request. Is looks like Lean point blank refuses to do a rewrite if you give absolutely no information about which term you want to transform (other than its type).

Interestingly, I found explicitly telling Lean to apply the rule to b works for Nat.add_zero but not for add_zero. What's the difference? Here is the code:

import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Real.Basic


variable {R : Type*} [Ring R]

-- Works
theorem t4 {b : ℕ} : b = b + 0 := calc
  b = b + 0 := by rw [← Nat.add_zero b]

-- Failed
theorem t5 {b : R} : b = b + 0 := calc
  b = b + 0 := by rw [← add_zero b]
  -- Error occurs 👆: unsolved goals ...|- b + 0 = b + 0 + 0

[Michael Stoll]

As you can see, rw rewrote both occurrences of b. In the Nat case, the resulting goal can be proved by rfl (which is tried by rw after the rewriting), but this is not the case for Real.

[Michael Stoll]

If you replace rw by rewrite (which does not try rfl), then you see that it rewrites in the same way in your first example.

[Ruben Van de Velde]

I'm surprised that rw's rfl is strong enough for that

[Kevin Buzzard]

Yes the issue is not with calc or with ←, the issue is that the way rw [h] when h : A = B works, when A contains some metavariable (e.g. ?s), is: first Lean finds a way to give values to all the ?s such that the corresponding concrete ?-free version of A appears in the goal, and then it replaces all occurrences of this particular A with the corresponding B. So nothing here seems surprising.

[ChenW]

Michael Stoll said:

As you can see, rw rewrote both occurrences of b. In the Nat case, the resulting goal can be proved by rfl (which is tried by rw after the rewriting), but this is not the case for Real.

Thanks, that’s the point :laughing: . It seems that when using rw, Lean replaces all occurrences on both the left and right sides of the equation.

This is surprising to me, as I expected rw to only replace the first occurrence. So, the next question is: Is there a way to instruct Lean to replace only the first, second, or specific occurrence of a symbol with another symbol?

[Ilmārs Cīrulis]

nth_rewrite and nth_rw, maybe?

[Ruben Van de Velde]

Either that or the "occurrences" configuration, for which I always forget the syntax, but hovering over rw might show it

[ChenW]

Thank you guys. :+1:

[Ruben Van de Velde]

Now, note that it's a bit more complex than "all occurrences" - consider (a + 0) + (b + 0) = a + 0. In this case rw will look for a place where it matches, notice it matches when filling in a as the argument, and replace both cases of a + 0 but not b + 0

[Michael Stoll]

There is also conv, which allows you to navigate inside the goal and do very targeted rewrites.

[Kyle Miller]

@Ruben Van de Velde I think it made it into the Lean release mathlib is now using — you can now write rw (occs := [2,6]) [lemmas]. I believe the occurrences are 1-indexed.