Demo of "apply a reversible operation to both sides"

Stream: new members

[Isak Colboubrani]

For educational purposes, I'm trying to create the most simple and trivial demonstration of how the principle "apply a reversible operation to both sides of an equation" can be expressed in Lean.

Here’s my current draft:

import Mathlib

example (a b : ℤ) (h : a + b = 0) : -a = b := by
  -- h : a + b = 0
  apply_fun (-a + ·) at h
  -- h : -a + (a + b) = -a + 0
  simp at h
  -- h : b = -a
  symm at h
  -- h : -a = b
  exact h

This approach closely mirrors how the audience (junior undergraduates) would solve the equation on paper if they were required to show every single step—aside from the simplification step (simp), which provides a valid and acceptable shortcut in this case.

However, when I demo the same method while working directly with the goal instead of the hypothesis, the result is not as clean:

import Mathlib

example (a b : ℤ) (h : a + b = 0) : -a = b := by
  -- ⊢ -a = b
  apply_fun (a + ·)
  -- ⊢ (fun x ↦ a + x) (-a) = (fun x ↦ a + x) b
  -- ⊢ Function.Injective fun x ↦ a + x
  simp
  -- ⊢ 0 = a + b
  -- ⊢ Function.Injective fun x ↦ a + x
  symm
  -- ⊢ a + b = 0
  -- ⊢ Function.Injective fun x ↦ a + x
  exact h
  -- ⊢ Function.Injective fun x ↦ a + x
  exact add_right_injective a

My questions:

• Does the first example look correct and idiomatic? (Of course, this could be solved with linarith, but I want to demonstrate the process from first principles.)
• Regarding the latter example: I would like to avoid having to explain fun x ↦ a + x) (-a) = (fun x ↦ a + x) b, Function.Injective fun x ↦ a + x and exact add_right_injective a at this stage. Is that unavoidable, or is there any small tweak that would allow me to skip that discussion for later?

[suhr]

Well, you can use suffices:

import Mathlib

example (a b : ℤ) (h : a + b = 0) : -a = b := by
  suffices g: a + -a = a + b by
    apply_fun (-a + ·) at g
    simp at g
    exact g

  simp
  show 0 = a + b

  symm
  show a + b = 0

  exact h

[suhr]

Applying a function to the both sides of an equation is directional, you can't undo applying a function unless the function is injective. For this reason apply_fun requires Function.Injective.
Explaining functions should be done before introduction of proofs, so (fun x ↦ a + x) (-a) = (fun x ↦ a + x) b won't be a problem.

[Isak Colboubrani]

The focus here isn't really on functions -- since $\mathbb{Z}$ is an abelian group under addition, every element has an additive inverse, so solving for $-a$ is just a matter of basic group properties. There's no fundamental reason why this proof should require a discussion of injectivity as far as I can tell? My main question is whether there's a way to structure the proof that stays true to the "apply a clearly reversible operation to both sides" idea while sidestepping any detours (such as function injectivity since the operation is inherently reversible). Are you suggesting that this approach is the best possible, or might there be a simpler alternative?

[suhr]

Another way is to use cancellation lemmas like add_left_cancel:

import Mathlib

example (a b : ℤ) (h : a + b = 0) : -a = b := by
  suffices g: a + -a = a + b from
    add_left_cancel g

  simp
  show 0 = a + b

  symm
  show a + b = 0

  exact h

[Laurance Lau]

Might this be useful: congrArg

example (a b : ℤ) (h : a + b = 0) : -a = b := by
  replace h := congr_arg (b - ·) h
  simp at h
  exact h

[Ruben Van de Velde]

That's the same as apply_fun on the hypothesis, btw

[Kyle Miller]

Isak Colboubrani said:

There's no fundamental reason why this proof should require a discussion of injectivity as far as I can tell? My main question is whether there's a way to [sidestep] any detours (such as function injectivity since the operation is inherently reversible)

"Injectivity" is the word for whether a function can be reversed/canceled :-) It's not a detour.

There's a question of whether apply_fun could plug into some framework to auto-derive injectivity theorems. It already has limited ability to prove injectivity automatically if the function being applied is an docs#Equivalence, which is in the stronger case when the function is invertible.

[Kyle Miller]

If somebody wants a small metaprogramming project, I think ⊢ (fun x ↦ a + x) (-a) = (fun x ↦ a + x) b is a small bug. When you do apply_fun ... at, it beta reduces the LHS and RHS (search for headBeta in Mathlib/Tactic/ApplyFun.lean). It ought to do headBeta of the LHS and RHS when applying to the goal too.

[Kyle Miller]

Note that apply_fun ... at is sort of the original purpose of the tactic. It's the forwards direction, and something you can obviously do. Being able to apply_fun at the goal is fancy, since it needs proof that you can cancel the function.

[Ruben Van de Velde]

You might consider the following:

import Mathlib

example (a b : ℤ) (h : a + b = 0) : -a = b := by
  apply_fun (0 * ·)
  · simp
  · sorry -- oops, now what?

[Isak Colboubrani]

"Injectivity" is the word for whether a function can be reversed/canceled :-) It's not a detour.

You're absolutely right (of course). My point was that I had naïvely assumed (or rather, hoped) that injectivity would be automatically inferred, so I wouldn't need to explicitly state it at this stage.

To clarify, here’s what I hoped for versus what I actually got:

-- What I had hoped for:
example (a b : ℤ) (h : a + b = 0) : -a = b := by
  -- ⊢ -a = b
  apply_fun (a + ·)
  -- (Automatic inferring of injectivity: ⊢ Function.Injective fun x ↦ a + x)
  -- ⊢ a + -a = a + b
  simp
  -- ⊢ 0 = a + b
  symm
  -- ⊢ a + b = 0
  exact h

-- What I got:
example (a b : ℤ) (h : a + b = 0) : -a = b := by
  -- ⊢ -a = b
  apply_fun (a + ·)
  -- ⊢ (fun x ↦ a + x) (-a) = (fun x ↦ a + x) b
  -- ⊢ Function.Injective fun x ↦ a + x
  simp
  -- ⊢ 0 = a + b
  -- ⊢ Function.Injective fun x ↦ a + x
  symm
  -- ⊢ a + b = 0
  -- ⊢ Function.Injective fun x ↦ a + x
  exact h
  -- ⊢ Function.Injective fun x ↦ a + x
  exact add_right_injective a

[Isak Colboubrani]

From a UX/demonstration perspective, I think it would already be a significant improvement if we got ⊢ a + (-a) = a + b instead of ⊢ (fun x ↦ a + x) (-a) = (fun x ↦ a + x) b, even if automatically handling injectivity is more challenging.

That said, it sounds like both are feasible? That’s really promising!

I believe that "performing clearly reversible operations on both sides of an equation" is one of the first things beginners experiment with. Thus, ensuring that extremely simple cases like this don’t introduce unnecessary cognitive load—such as having to explain how to parse (fun … ↦ …) (…), Function.Injective fun … ↦ …, etc.—would be a significant win for onboarding.

[Robin Arnez]

You can use fun_prop and a macro:

import Mathlib

theorem Odd.pow_left_injective {R : Type*} [LinearOrderedSemiring R] {n : ℕ} [ExistsAddOfLE R] (hn : Odd n) :
    Function.Injective fun a : R => a ^ n :=
  hn.strictMono_pow.injective

theorem Odd.zpow_left_injective {R : Type*} [LinearOrderedField R] {n : ℤ} [ExistsAddOfLE R] (hn : Odd n) :
    Function.Injective fun a : R => a ^ n := by
  by_cases h : 0 ≤ n
  · conv => rhs; intro a; rw [← Int.toNat_of_nonneg h, zpow_natCast]
    apply Odd.pow_left_injective
    obtain ⟨k, hk⟩ := hn
    use k.toNat
    omega
  · conv => rhs; intro a; rw [← neg_neg n, _root_.zpow_neg, ← Int.toNat_of_nonneg (neg_nonneg.mpr (le_of_not_le h)), zpow_natCast]
    refine Function.Injective.comp inv_injective ?_
    apply Odd.pow_left_injective
    obtain ⟨k, hk⟩ := hn
    use (-k - 1).toNat
    omega

theorem div_left_injective₀ {G : Type*} [GroupWithZero G] {b : G} (hb : b ≠ 0) : Function.Injective fun a => a / b := by
  intro x y (h : x / b = y / b)
  exact (div_left_inj' hb).mp h

attribute [fun_prop] Function.Injective
attribute [fun_prop] add_left_injective
attribute [fun_prop] add_right_injective
attribute [fun_prop] sub_left_injective
attribute [fun_prop] sub_right_injective
attribute [fun_prop] Function.Injective.comp
attribute [fun_prop] mul_left_injective
attribute [fun_prop] mul_left_injective₀
attribute [fun_prop] mul_right_injective
attribute [fun_prop] mul_right_injective₀
attribute [fun_prop] div_left_injective
attribute [fun_prop] div_left_injective₀
attribute [fun_prop] div_right_injective
attribute [fun_prop] pow_right_injective₀
attribute [fun_prop] zpow_right_injective₀
attribute [fun_prop] Odd.pow_left_injective
attribute [fun_prop] Odd.zpow_left_injective
attribute [fun_prop] inv_injective

macro "apply_fun'" f:term : tactic => `(tactic| (apply_fun $f; beta_reduce; rotate_left 1; fun_prop (disch := norm_num <;> trivial)))

-- What you had hoped for and what you'll get:
example (a b : ℤ) (h : a + b = 0) : -a = b := by
  -- ⊢ -a = b
  apply_fun' (a + ·)
  -- (Automatic inferring of injectivity: ⊢ Function.Injective fun x ↦ a + x)
  -- ⊢ a + -a = a + b
  simp
  -- ⊢ 0 = a + b
  symm
  -- ⊢ a + b = 0
  exact h

[Floris van Doorn]

We should definitely add fun_prop attributes for injectivity to Mathlib!