Zulip Chat Archive

Stream: new members

Topic: Apply rw to hypothesis


view this post on Zulip Chu-Wee Lim (Oct 04 2019 at 18:19):

Sorry quick question. Is there a way to apply the rewrite tactic to a hypothesis instead of goal?

E.g. if h : a + c = b + c, I would like to apply add_right_cancel to it and obtain a = b.

view this post on Zulip Johan Commelin (Oct 04 2019 at 18:21):

Yes, rw lemma at hyp

view this post on Zulip Johan Commelin (Oct 04 2019 at 18:22):

Similarly simp at hyp, change foo at hyp, push_neg at hyp, etc...

view this post on Zulip Chu-Wee Lim (Oct 04 2019 at 18:39):

Sorry I tried the following, but it's giving me an error.

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := assume a b c d h,
begin
rw add_right_cancel at h,
end

Error message: rewrite tactic failed, lemma lhs is a metavariable

view this post on Zulip Johan Commelin (Oct 04 2019 at 19:33):

@Chu-Wee Lim The problem is that add_right_cancel is not formulated as an iff statement. So you cannot use it like this.

view this post on Zulip Johan Commelin (Oct 04 2019 at 19:35):

You can do something like

example :  a b c d : , a + c + d = b + c + d  a = b :=
assume a b c d h,
begin
  have step1 := add_right_cancel h,
  have step2 := add_right_cancel step1,
  exact step2,
end

view this post on Zulip Floris van Doorn (Oct 04 2019 at 19:59):

If it were an iff statement, you could rewrite with it:

example :  a b c d : , a + c + d = b + c + d  a = b :=
begin
  intros a b c d h,
  rw [add_right_cancel_iff, add_right_cancel_iff] at h,
  exact h
end

view this post on Zulip Patrick Massot (Oct 04 2019 at 20:55):

Johan's solution is fake tactic mode, it could be written as

example :  a b c d : , a + c + d = b + c + d  a = b :=
assume a b c d h, add_right_cancel (add_right_cancel h)

(which is perfectly fine). More in the tactic mode spirit would be:

example :  a b c d : , a + c + d = b + c + d  a = b :=
assume a b c d h,
begin
  apply add_right_cancel,
  apply add_right_cancel h,
end

Although my taste in this case is to declare this as something Lean should just crush without asking any question:

example :  a b c d : , a + c + d = b + c + d  a = b :=
by { intros,  linarith }

Last updated: May 12 2021 at 04:19 UTC