Tips for basic equality manipulations

Stream: new members

[Pi Lanningham]

Hi all! One thing I find myself struggling with is equation manipulation. Things that feel very simple in standard mathematics are completely eluding me, like "moving" a term to the other side. In principle I know it probably involves adding or subtracting the same thing from both sides, but I can't find a rewrite rule that lets me do this.

Here's a simple example, but I'd emphasize that I could probably figure this one out, and the specific example is less important; it's just that this kind of thing grows very challenging very quickly, so it feels like I'm missing some tool.

https://gist.github.com/Quantumplation/0e845840ca31555a884879915849a617

[Rado Kirov]

I am just getting started with LEAN too, but this seems to work (it was suggested to be me by Claude :):

theorem sample (a: Int) (b: Int) : a + b = c -> b = c - a := by
  intro h
  apply_fun (λ x => x + a)
  simp [add_comm]
  exact h
  exact add_left_injective a

[Rado Kirov]

To your point though - what's the general repeatable part that is not specific to this example. The function that is applied to the equality can be quite general, but you still have to prove infectivity (and in this case it happens to already be there).

[Pi Lanningham]

ok so apply_fun essentially applies some function to both sides of the equation; that's helpful!

[Markus Himmel]

Most Lean users would probably use one of the high-powered algebraic tactics for goals like this instead of manually manipulating the terms. Here are some examples for tactics you could use:

import Mathlib

example (a : Int) (b : Int) : a + b = c → b = c - a := by
  intro h
  -- `omega` is a decision procedure for `Nat` and `Int`
  omega

example (a : Int) (b : Int) : a + b = c → b = c - a := by
  intro h
  -- `linarith` solves systems of linear (in)equalities
  linarith

example (a : Int) (b : Int) : a + b = c → b = c - a := by
  intro h
  -- replace `c` with `a + b` in the goal
  subst h
  -- `abel` solves goals in abelian groups
  abel

example (a : Int) (b : Int) : a + b = c → b = c - a := by
  intro h
  -- replace `c` with `a + b` in the goal
  subst h
  -- `ring` solves goals in commutative rings
  ring

example (a : Int) (b : Int) : a + b = c → b = c - a := by
  intro h
  -- replace `c` with `a + b` in the goal
  subst h
  -- The simplifier also know many basic algebraic facts
  simp

[Pi Lanningham]

knowing about those high level algebraic tactics is useful, but I'm finding myself struggling when the proof is more complex, so I wanted to build up my understanding from the "primitives" i have available to me, so I can convince it / massage it by hand when needed

[Pi Lanningham]

If you're curious, here's the full example I'm currently playing with; The sorry here is where I'm currently stuck:

https://gist.github.com/Quantumplation/cbfbe910a75f5f03c21be9820a55ab3a

I'm not sure if the apply_fun ended up being the right thing to do here, so I might backtrack, but it at least gives a sense for where omega, abel, etc. aren't going to solve it right away

[Markus Himmel]

I see. I think having a good command of #naming is useful for guessing the names of helpful lemmas in cases like this. For example, I think rw [add_comm, ← sub_eq_add_neg, sub_eq_iff_eq_add, ← balanced] makes progress in your example.

[Ruben Van de Velde]

In this case, you can also use that it exists in the library:

import Mathlib
theorem sample (a: Int) (b: Int) : a + b = c -> b = c - a := by
  intro h
  apply eq_sub_of_add_eq'
  exact h