Help design this exercise

Stream: Lean for teaching

[Boris Kjær]

Let's say I want to show students how to use linear maps. I give the following exercise, here completed with the proof I want.

import Mathlib.Algebra.Module.LinearMap.Defs
import Mathlib.Data.Real.Basic

variable {V W : Type}
    [AddCommGroup V] [Module ℝ V]
    [AddCommGroup W] [Module ℝ W]
    (f : V →ₗ[ℝ] W)

-- attribute [-simp] map_zero

example : f 0 = 0 := by
  have f_map_add := f.map_add
  have f_map_smul := f.map_smul
  -- sorry -- finish the proof
  have : f (0 + 0) = f 0 + f 0 := f_map_add 0 0 -- this does nothing!
  simp

The trouble is, removing the last have doesn't break the proof. I would like to allow using ring but that doesn't work so instead I use simp.
But now it is not a good exercise because students aren't forced to learn f.map_add or f.map_smul.

So I could put attribute [-simp] map_zero. Then the last have would be necessary and I'm happy except for hacking simp.

Is there another way (using ring) that I haven't thought of?

[Johan Commelin]

I would do the simp hacking. And maybe hide it in an import Course.Prerequisites.

[Dan Velleman]

Would it help to use 0 + 0 = 0 to rewrite your have as f 0 = f 0 + f 0?

[Boris Kjær]

It is of course an option not to allow simp at all, and then it can be still be proved using rw [add_zero] at this etc etc.

[Boris Kjær]

But in my ideal world some combination of f.map_add and ring could do it.

[Kevin Buzzard]

Why not ask them to prove that f(3v+4w)=3f(v)+4f(w) instead? Or just abstract things out and don't have f of type linearmap, just have f : V -> W and hypotheses that f(a+b)=f(a)+f(b) and whatever else you want?

[Riccardo Brasca]

Have you thought about defining a predicate isLinear f and work with it? If you only want to work with basic stuff it could be better to not having the mathlib API.

[Kevin Buzzard]

Alternatively you could define your own linear maps (ie what Riccardo just said!)

[Riccardo Brasca]

Something like

import Mathlib
variable {V W : Type}
    [AddCommGroup V] [Module ℝ V]
    [AddCommGroup W] [Module ℝ W]

structure isLinear (f : V → W) where
  isAdd : ∀ v w, f (v + w) = f v + f w
  smul : ∀ (r : ℝ) v, f (r • v) = r • (f v)

example {f : V → W} (hf : isLinear f) : f 0 = 0 := by
  simpa using hf.smul 0 0

[Boris Kjær]

Nice, those are good ideas!
Thank you Kevin and Riccardo

[Kevin Buzzard]

I've defined my own groups before and called themGroup' but soon realised that you need to prove many many lemmas to make the procedure viable if you want to go beyond simple exercises (you need uniqueness of identity/inverses, inverse of products etc).