MIL Ch2.1 exercise

Stream: new members

[Jeremy Aube]

I was going through the exercises in MIL Ch2.1 and got to this exercise:

The following exercise is a little more challenging. You can use the theorems listed underneath.

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  sorry

#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a

I was able to solve with this, but only by using sub_add_cancel, which isn't mentioned until later:

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  rw [add_mul, mul_sub, ← pow_two]
  rw [mul_sub, ← pow_two, add_sub]
  rw [mul_comm, sub_add_cancel]

Is there some way to solve this that only uses theorems mentioned up to that point in the guide?

[Daniel Horton]

I've recently picked up Lean and have been going through the MIL exercises as well. Here's what I wrote for that exercise:

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  calc
    (a + b) * (a - b) = a ^ 2 - a * b + a * b - b ^ 2 := by
      rw [add_mul, mul_sub, mul_sub, ← pow_two, ← pow_two, mul_comm b, add_sub]
    _ = a ^ 2 - b ^ 2 := by
      rw [add_comm, add_sub, add_comm, ← add_sub, sub_self, add_zero]

It looks like I avoided using sub_add_cancel by instead using the theorem sub_self which was introduced earlier in the chapter.

[Jeremy Aube]

@Daniel Horton thanks! That was it, I was missing that middle

rw [add_comm, add_sub, add_comm]

to rotate the terms. That’s a neat trick.

[Michael]

It feels worth mentioning conv here - I don't think MIL mentions it, but it's really convenient for applying rewrites to complex statements.

https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Targeted-Rewriting-with--conv/

[Jeremy Aube]

Interesting, that seems similar to nth_rw, but I don’t know enough to know what the difference is.

[Michael]

Try stepping through this:

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Set.Basic

section
variable (G : Type*) [CommGroup G] [Finite G]

example {_ : Fintype G} {x : G} (hx : x = ∏ g : G, g) : x * x = 1 := by
  let G' := {g | g : G}
  have _ := Fintype.ofFinite G' -- we need this to use ∏
  have hx' : x = ∏ g ∈ G', g := by
    rw [hx]
    apply Finset.prod_bijective id Function.bijective_id
    · intro i
      simp only [Finset.mem_univ, id_eq, Set.mem_toFinset, true_iff]
      use i
    · intro g hg; unfold id; rfl
  have hxinv' : x = ∏ g ∈ G', g⁻¹ := by
    rw [hx']
    apply Finset.prod_bijective (·⁻¹)
    · apply And.intro inv_injective inv_surjective
    · intro g
      simp only [Set.mem_toFinset]
      apply Iff.intro
      · intro hg; use g⁻¹
      · intro hg; use g
    · intro g hg; rw [inv_inv]
  -- do some rewriting to match the assumptions of Finset.prod_mul_prod_comm
  conv => lhs; lhs; rw [hx']; arg 2; ext g; rw [← mul_one g, ← id_eq g]
  conv => lhs; rhs; rw [hxinv']; arg 2; ext g; rw [← mul_one g⁻¹]
  rw [Finset.prod_mul_prod_comm id (fun a ↦ (1 : G)) (·⁻¹) (fun a ↦ (1 : G))]
  -- for manual solving, the relevant theorem is Finset.prod_eq_one
  -- rw [id_eq] -- this fails, but conv can do it:
  conv => lhs; rw [one_mul]; lhs; arg 2; ext g; rw [id_eq, mul_inv_cancel]
  simp

end

conv seems to be able to navigate into structures that rw can't.

In your case, you can do rewrites by carefully specifying exactly where you want them done, but it feels more intuitive to me doing it with conv.

(I don't know why the rw [id_eq] fails -- rw [one_mul] doesn't, but the context looks identical to me. And unfold id will succeed in the same context where rw [id_eq] doesn't.)

[Aaron Liu]

Michael said:

Try stepping through this:

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Algebra.Group.Basic
import Mathlib.Data.Set.Basic

section
variable (G : Type*) [CommGroup G] [Finite G]

example {_ : Fintype G} {x : G} (hx : x = ∏ g : G, g) : x * x = 1 := by
  let G' := {g | g : G}
  have _ := Fintype.ofFinite G' -- we need this to use ∏
  have hx' : x = ∏ g ∈ G', g := by
    rw [hx]
    apply Finset.prod_bijective id Function.bijective_id
    · intro i
      simp only [Finset.mem_univ, id_eq, Set.mem_toFinset, true_iff]
      use i
    · intro g hg; unfold id; rfl
  have hxinv' : x = ∏ g ∈ G', g⁻¹ := by
    rw [hx']
    apply Finset.prod_bijective (·⁻¹)
    · apply And.intro inv_injective inv_surjective
    · intro g
      simp only [Set.mem_toFinset]
      apply Iff.intro
      · intro hg; use g⁻¹
      · intro hg; use g
    · intro g hg; rw [inv_inv]
  -- do some rewriting to match the assumptions of Finset.prod_mul_prod_comm
  conv => lhs; lhs; rw [hx']; arg 2; ext g; rw [← mul_one g, ← id_eq g]
  conv => lhs; rhs; rw [hxinv']; arg 2; ext g; rw [← mul_one g⁻¹]
  rw [Finset.prod_mul_prod_comm id (fun a ↦ (1 : G)) (·⁻¹) (fun a ↦ (1 : G))]
  -- for manual solving, the relevant theorem is Finset.prod_eq_one
  -- rw [id_eq] -- this fails, but conv can do it:
  conv => lhs; rw [one_mul]; lhs; arg 2; ext g; rw [id_eq, mul_inv_cancel]
  simp

end

Note that ∏ g : G, g is short for ∏ g ∈ Finset.univ, g, so you can directly apply lemmas about ∏ x ∈ s, f x and G' is unnecessary.

[Aaron Liu]

Michael said:

(I don't know why the rw [id_eq] fails -- rw [one_mul] doesn't, but the context looks identical to me. And unfold id will succeed in the same context where rw [id_eq] doesn't.)

rw can't match bound variables. So since 1 * 1 doesn't contain any bound variables, rw [one_mul] will work, but id a has the bound variable a so rw [id_eq] fails.

[Jeremy Aube]

That ext is interesting. Is that something that's only available to conv? Is that what's removing the bound variable so rw [id_eq] can succeed?

[Michael]

Aaron Liu said:

Note that ∏ g : G, g is short for ∏ g ∈ Finset.univ, g, so you can directly apply lemmas about ∏ x ∈ s, f x and G' is unnecessary.

Thanks! Something that bothered me about the proof is that I needed to assume {_ : Fintype G} to make the definition of hx typecheck, even though G is declared with [Finite G]. I don't like it because that Fintype assumption is independent of the [Finite G] - if I comment out [Finite G], the example still compiles just fine. Is there a better way to pose the example?

[Michael]

Jeremy Aube said:

That ext is interesting. Is that something that's only available to conv? Is that what's removing the bound variable so rw [id_eq] can succeed?

Yes, the ext navigates into the binding, and to my understanding the rw then runs in a context where the bound variable is just one of your facts.

ext x traverses into a binder (a fun x => e or ∀ x, e expression) to target e, introducing name x in the process.