reasoning through math on structs

Stream: general

[Matthew Pocock]

I have a struct LinEq that's a simple linear equation. I've defined scalar multiplication and addition for it. In the example at the end of this MWE, the proof gets stuck, as I haven't convinced it to unpack the hMul and hAdd definitions.

inductive ColN where
    | zero      : ColN          -- zero, also leading zero
    | even_of   : ColN → ColN   -- the even number that is twice the previous
    | odd_of    : ColN → ColN   -- the odd number that is one more than twice the previous
deriving Repr

def z10 := ColN.even_of $ ColN.odd_of ColN.zero

@[simp]
def ColN.eval {α : Type} [HMul ℕ α α] [HAdd ℕ α α] (cn: ColN) (n : α) : α := match cn with
| ColN.zero => n
| ColN.even_of cm => 2 * (ColN.eval cm n)
| ColN.odd_of cm => 1 + 2 * (ColN.eval cm n)

structure LinEq (α : Type) :=
  (m : α)
  (c : α)
deriving Repr

instance {α : Type} [HMul α α α]: HMul α (LinEq α) (LinEq α) where
  hMul a b := ⟨a * b.m, a * b.c⟩

instance {α : Type} [HAdd α α α]: HAdd α (LinEq α) (LinEq α) where
  hAdd a b := ⟨b.m, a + b.c⟩

example (n : LinEq ℕ): z10.eval n = ⟨4, 2⟩ := by
  have ⟨m₀, c₀⟩ := n -- unpacking here doesn't seem to help
  simp -- this doesn't simplify through the LinEq ops
  ring

[Eric Wieser]

The standard thing to do here is write an @[ext] lemma for LinEq

[Eric Wieser]

As well as write a simp lemma that says (a * b).m = a * b.m

[Eric Wieser]

simp only knows the things you teach it, and you didn't teach it what * and + on LinEq mean

[Matthew Pocock]

Ah OK - I had assumed that simp could see through instances of things like HMul. Fair enough. I'll write out the lemmas :D

[Eric Wieser]

You can get lean to generate them for you if you add @[simps] to the instance, but it will generate them with terrible names!

[Matthew Pocock]

Thanks. It worked when I added @[simp] directly to the instances. It didn't work when I wrote out theorems for each component m, c, individually, as I don't think that was the right shape. I feel a bit strange pushing entire linear equations through functions that I thought of as taking numbers. Good strange, but strange.

[Yaël Dillies]

Not sure you noticed, but @[simp] and @[simps] do different things.

[Matthew Pocock]

Yaël Dillies said:

Not sure you noticed, but @[simp] and @[simps] do different things.

No, I hadn't! And I don't think I'd noticed they were differently written until you pointed it out. FWIW, tagging the instances with @[simp] works in this case, while @[simps] does not.

[Eric Wieser]

simps should do the right thing in combination with @[ext] on the structure

[Eric Wieser]

(and ext in the proof)