Zulip Chat Archive

Stream: new members

Topic: Embarrassingly simple question about Mathlib example


Martin Gilchrist (Jan 02 2024 at 00:50):

Hi - this really a two-part question. First, what is the best forum in which to ask simple questions about the Mathlib tutorial? Secondly, I am having difficulty with one example in the Rings section: it asks, show

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by

I think this should be done by a rw clause, but the first thing I want to do is to add -a to the left of each side of the hypothesis, but I can't work out how to express this. I'm sure this is a simple question, but don't yet have the conceptual mindset to do this.

Thanks for any help! Martin

Pedro Sánchez Terraf (Jan 02 2024 at 00:57):

Hi! #new members is the right place for beginner's questions (perhaps you can move this thread to that channel). You can also use backtics to make your code more readable:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by

Pedro Sánchez Terraf (Jan 02 2024 at 01:04):

One idea for this exercise (which actually belongs to Section 2, Basics, of MIL) is to start by rewriting the goal using one of the previous two theorems.

Working at the hypothesis h is also feasible, but you'll learn about that later on.

Notification Bot (Jan 02 2024 at 01:24):

This topic was moved here from #lean4 > Embarrassingly simple question about Mathlib example by Kyle Miller.

Kyle Miller (Jan 02 2024 at 01:25):

(@Martin Gilchrist Moved!)

Martin Gilchrist (Jan 02 2024 at 03:02):

Hi - thanks, Pedro and Kyle - I am sorry, but I just don't understand what it means to "rewrite the goal"! Can you give me an example of how I would (left) add -a to h in order to start the re-writing process? Apologies for really dumb questions.

Richard Copley (Jan 02 2024 at 03:18):

import Mathlib

variable (R : Type*) [AddCommGroup R]

theorem add_left_cancel' {a b c : R} (h : a + b = a + c) : b = c := by
  rw [ (add_right_injective a).eq_iff]
  sorry

Yaël Dillies (Jan 02 2024 at 07:22):

Richard, I think this uses too much compared to what the exercise is intending.

Yaël Dillies (Jan 02 2024 at 07:23):

@Martin Gilchrist, you can start with rw [← add_neg_cancel_right b a].

Martin Gilchrist (Jan 02 2024 at 18:05):

@Yaël Dillies Thanks - I have proved add_neg_cancel_right, and so I added the following with your hint:

theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
rw [← add_neg_cancel_right b a, add_assoc, zero_add]

which I feel should give me three rewrites: -a + a + b = -a + a + c then (-a + a) + b = (-a + a) + c then 0 + b = 0 + c then b = c but instead I get an error that the tactic did not find instance of pattern (see screenshot). I think I must be missing some understanding here.

image.png

Any help would be appreciated. Thanks, Martin

Matt Diamond (Jan 02 2024 at 18:16):

I can explain why you're getting that issue, but I'm curious why you're trying to rewrite the goal from b = c back to b = c

Matt Diamond (Jan 02 2024 at 18:23):

if you click after each comma in the rw block, you can see the effect of each individual rewrite in the infoview, which might help clarify things

Ruben Van de Velde (Jan 02 2024 at 18:41):

There's no 0 + ... anywhere to be seen, so why do you think zero_addapplies?

Ruben Van de Velde (Jan 02 2024 at 18:42):

But also Matt's point

Ruben Van de Velde (Jan 02 2024 at 18:44):

You need to get to a point where you can rewrite with h, so you need to get a+b in your goal somehow

Martin Gilchrist (Jan 02 2024 at 18:45):

@Matt Diamond Hi, Matt - I would really appreciate your help here. Your comment about clicking after each comma is very useful, but as you can see from the following screenshot, I think I have got to the point b = c, but I still see a red underline under by indicating that I have not proved the theorem! I think I'm not clear about what you mean by trying to rewrite from b = c back to b = c because I think I am going from a + b = a+ c to b = c . Am I not?

image.png

Yaël Dillies (Jan 02 2024 at 18:50):

Yes, you managed to reduce b = c to proving b = c. As Ruben pointed out, this is not what you want to be doing.

Matt Diamond (Jan 02 2024 at 18:59):

I think I am going from a + b = a+ c to b = c . Am I not?

@Martin Gilchrist rw [] operates on the goal, which is b = c... to rewrite the hypothesis h : a + b = a + c, you would use rw [] at h

Matt Diamond (Jan 02 2024 at 19:03):

however, you don't necessarily need to rewrite h... you can also solve this by rewriting the goal using h

Matt Diamond (Jan 02 2024 at 19:15):

the strategy that Ruben is suggesting is to rewrite the goal so that it includes a + b, and then do rw [h]

Matt Diamond (Jan 02 2024 at 19:26):

also, I think you might have a misunderstanding of how the goal works in the info view... ⊢ b = c doesn't mean that you've proved b = c, it means that b = c is the thing you need to prove

Martin Gilchrist (Jan 02 2024 at 19:57):

@Matt Diamond and @Yael and @Ruben Van de Velde I am really sorry, and I don't mean to be a pain, but I don't understand what you mean by use rw [] at h. I tried the following (see screenshot) in which I have at h at the end of the line, and I am trying to (I think) add -a to the left of each side of h, but try as I might, I cannot get the syntax right.

image.png

I have tried variations using the left arrow and using a b but I'm afraid that I am missing something syntactical about Lean. It might save time all around, if you can show me a simple solution, and then I can puzzle through the syntax by myself rather than take up your time?

Matt Diamond (Jan 02 2024 at 21:31):

@Martin Gilchrist No need to apologize! Here's a solution:

import Mathlib

variable (R : Type*) [AddCommGroup R]

theorem add_left_cancel' {a b c : R} (h : a + b = a + c) : b = c := by
  rw [ add_neg_cancel_right b a, add_comm b a, h, add_comm a c, add_neg_cancel_right]

Martin Gilchrist (Jan 02 2024 at 21:57):

@Matt Diamond Thanks, and I assume that the h in the rw clause is an example of "using h" that you mentioned earlier?

Anyway, @Matt Diamond @Yaël Dillies @Ruben Van de Velde I do appreciate your patience with me. This has been a learning experience for me, and reconfirms my appreciation of the helpfulness and responsiveness of the Lean community!

Matt Diamond (Jan 02 2024 at 22:13):

I assume that the h in the rw clause is an example of "using h" that you mentioned earlier?

yes, exactly... hypotheses can be used just like any other lemma or theorem

Ruben Van de Velde (Jan 02 2024 at 22:31):

Essentially the proof here is b=0+b=(a+a)+b=a+(a+b)=a+(a+c)=(a+a)+c=0+c=cb = 0 + b = (-a + a) + b = -a + (a + b) = -a + (a + c) = (-a + a) + c = 0 + c = c


Last updated: May 02 2025 at 03:31 UTC