Zulip Chat Archive

Stream: new members

Topic: subtract equation lemma


view this post on Zulip Calle Sönne (Feb 25 2019 at 14:42):

I have a goal a = b and a hypothesis `c = d is there a lemma that gives a - c = b - d ? Only way I see how to do it without the lemma is to subtract c from a = b, then use conv to rw c on rhs, but this is quite tedious.

view this post on Zulip Calle Sönne (Feb 25 2019 at 14:42):

I am in some ring if that is relevant

view this post on Zulip Kenny Lau (Feb 25 2019 at 14:43):

congr (congr_arg (-) (hab : a = b)) (hcd : c = d)

view this post on Zulip Kenny Lau (Feb 25 2019 at 14:43):

I once tried to get it to mathlib but people didn't like it

view this post on Zulip Kenny Lau (Feb 25 2019 at 14:44):

or you can just have a - c = b - d, by rw [hab, hcd]

view this post on Zulip Patrick Massot (Feb 25 2019 at 14:44):

I think that actually we should have more tactics like that, at least for teaching purposes

view this post on Zulip Gabriel Ebner (Feb 25 2019 at 15:01):

If you already have a - c = b - d as a goal, then you can apply the congr tactic which produces a=b and c=d as subgoals (there's also congr'):

example (a b c d : ) (h1 : a = b) (h2 : c = d) :=
show a - c = b - d, by congr; assumption

view this post on Zulip Calle Sönne (Feb 25 2019 at 16:06):

I have this goal: 0 = finset.sum (finset.range n) (λ (x : ℕ), digit b r x * ↑b ^ (n - x) - digit b r x * ↑b ^ (n - 1 - x + 1)) Im having trouble proving this, as the subtraction lemma I need require x ≤ n which is only true in the finset.range n, can I "enter" the sum somehow and prove it there, given hypothesis x ≤ n or similar .

view this post on Zulip Calle Sönne (Feb 25 2019 at 16:07):

the lemma is, nat.add_sub_assoc

view this post on Zulip Calle Sönne (Feb 25 2019 at 16:09):

The closest I have gotten is here:

0 = finset.sum (finset.range (1 + n))
      (λ (x : ), digit b r x * b ^ (1 + n - x) + -(digit b r x * b ^ (1 + (n - x))))

which is what requires nat.add_sub_assoc

view this post on Zulip Kenny Lau (Feb 25 2019 at 16:10):

finset.sum_eq_zero :
   {α : Type u_1} {β : Type u_2} [_inst_1 : add_comm_monoid β] [_inst_2 : add_comm_monoid β] {f : α  β}
  {s : finset α}, ( (x : α), x  s  f x = 0)  finset.sum s f = 0

view this post on Zulip Patrick Massot (Feb 25 2019 at 16:11):

You could use https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L124 if you were using my bigop proto-library. I don't know about finset

view this post on Zulip Calle Sönne (Feb 25 2019 at 16:11):

Thanks :)

view this post on Zulip Scott Morrison (Feb 25 2019 at 21:12):

We really need a mode in conv to enter a sum (whether finset or bigop), automatically gaining the hypothesis saying that you are in the domain.

view this post on Zulip Patrick Massot (Feb 25 2019 at 21:13):

That would be really cool


Last updated: May 08 2021 at 05:14 UTC