applying a theorem to a hypothesis

Stream: new members

[KEW]

Section 2.2 in Mathematics in Lean, it says to apply a theorem add_left_cancel to a hypothesis h is to do rw [add_left_cancel h], previously , in Section 2.1, it shows we can use the at syntax like rw [mul_comm d a] at hyp , so any reason that rw [add_left_cancel] at h gives an error?

[Matt Diamond]

you can't rewrite with docs#add_left_cancel by itself, as it's not an equality or iff... it's a function / implication

[Matt Diamond]

could you post a #mwe? it's hard to help without knowing what h is in this context

[Philippe Duchon]

The two forms are very different in what they do, or try to do. rw [thm h] or apply thm h is something you use when theorem thm requires some hypothesis, and h can serve as this hypothesis. For instance, add_left_cancel has type n + m = n + k → m = k: it requires a hypothesis of the form n + m = n + k, and it then yields a proof of m = k; since this is an equality, add_left_cancel h (where h has the required form) can be used with rw.

The other form, rw [thm] at h or apply thm at h, tries to use thm to change hypothesis h (instead of the current goal, which is the default when no at h is present).

[KEW]

Philippe Duchon said:

The two forms are very different in what they do, or try to do. rw [thm h] or apply thm h is something you use when theorem thm requires some hypothesis, and h can serve as this hypothesis. For instance, add_left_cancel has type n + m = n + k → m = k: it requires a hypothesis of the form n + m = n + k, and it then yields a proof of m = k; since this is an equality, add_left_cancel h (where h has the required form) can be used with rw.

The other form, rw [thm] at h or apply thm at h, tries to use thm to change hypothesis h (instead of the current goal, which is the default when no at h is present).

thanks for the answer, still my question is why can't I use add_left_cancel to change h, using the example in the book,

theorem mul_zero (a : R) : a * 0 = 0 := by
  have h : a * 0 + a * 0 = a * 0 + 0 := by
    rw [← mul_add, add_zero, add_zero]
  rw [add_left_cancel h]

that would be using add_left_cancel to re-write h : a * 0 + a * 0 = a * 0 + 0 into h : a * 0 = 0 which then allows me to do exact h. But I guess the reason is the type of the theorem add_left_cancel which expects a hypothesis as you explained

[Kevin Buzzard]

that would be using add_left_cancel to re-write h : a * 0 + a * 0 = a * 0 + 0 into h : a * 0 = 0

No, that's not what is happening there. rw [add_left_cancel h] doesn't mean "change h to something else", it means "prove the equality a * 0 = 0 using add_left_cancel applied to h, and then change all a * 0 in the goal to 0".

[Ruben Van de Velde]

It's hard to help without a #mwe, but you can try putting #check add_left_cancel h before the rw and see if that helps explain what happens

[Kevin Buzzard]

add_left_cancel is a function, or an implication. It eats a proof and spits out another proof. rw eats an equality like a * 0 = 0. The concepts P -> Q (an implication) and x = y (an equality) are very different things, and are used in different ways and by different things in Lean.

[KEW]

Got it. Thanks!