It's just add and sub?

Stream: new members

[Anders Larsson]

Hi,
I'm a software guy trying to learn Lean.

I think I have missed something obvious here. I would expect simp or some similar command do be able to
fix the example below or fail and prove that the equality is incorrect. What is a reasonable path forward?
(What tutorial to read? How to reason with big but seemingly obvious reshuffle of add/sub?).

import data.complex.basic

example (a b c : ℂ) :  a.re * b.im - c.re * b.im + (c.im * b.re - a.im * b.re) =
                       a.re * b.im + -(a.im * b.re) - (c.re * b.im + -(c.im * b.re)) :=
begin
   sorry
end

[Patrick Johnson]

docs#tactic.linarith

example (a b c : ℂ) :
  a.re * b.im - c.re * b.im + (c.im * b.re - a.im * b.re) =
  a.re * b.im + -(a.im * b.re) - (c.re * b.im + -(c.im * b.re)) :=
begin
  linarith,
end

[Anders Larsson]

Patrick Johnson said:

Awesome! I had only seen linarith in the context of inequalities so far.

[Alex J. Best]

tactic#ring and tactic#abel can also both prove this. Fun fact: linarith indeed does "only" do inequalities and proves this goal by showing both the the left hand side is \le the right hand side, and vice-versa.

[Alex J. Best]

tactic#abel is probably the right answer to the question of how to deal with a seemingly obvious reshuffle of add and sub, indeed abel can prove this when we set up a similar goal over an arbitrary ring, not just the reals/complexes:

example {C : Type*} [ring C] (a_re b_re c_re a_im b_im c_im : C) :
  a_re * b_im - c_re * b_im + (c_im * b_re - a_im * b_re) =
  a_re * b_im + -(a_im * b_re) - (c_re * b_im + -(c_im * b_re)) :=
begin
  abel,
end

The other two mentioned tactics don't manage this one, as linarith wants an ordering on the ring, and ring likes rings to be commutative.

[Kevin Buzzard]

I don't know what you're interested in but maybe this https://github.com/ImperialCollegeLondon/complex-number-game might show you some techniques?

[Anders Larsson]

Kevin Buzzard said:

I don't know what you're interested in but maybe this https://github.com/ImperialCollegeLondon/complex-number-game might show you some techniques?

Sure, i found it some days ago. I'm working on level 03 now.

[Kyle Miller]

@Anders Larsson simp can do this if you give it enough lemmas:

example (a b c : ℂ) :  a.re * b.im - c.re * b.im + (c.im * b.re - a.im * b.re) =
                       a.re * b.im + -(a.im * b.re) - (c.re * b.im + -(c.im * b.re)) :=
by simp [mul_comm, sub_eq_add_neg, add_assoc, add_comm, add_left_comm]

Even though repeat { rw mul_comm } would run forever, simp is smarter and chooses some sort of normal form.