Proving a theorem with recursion and lists

Stream: new members

[Colin Jones ⚛️]

I'm definitely missing a typeclass here; if so, please add. Is there anyway to prove this? I want to keep it polymorphic.

import Mathlib

-- Through Polymorphic Definitions
def sum [Add α] [Zero α] : List α → α
  | [] => 0
  | x :: L => x + sum L

def mul_cons [Mul α] [Add α] : α → List α → List α
  | _, [] => []
  | a, x::L => List.append [x * a] (mul_cons a L)

theorem mul_sum [MulZeroClass α] [Mul α] [Add α] [Zero α] (a : α) (L : List α) :
  a * sum L = sum (mul_cons a L) := by
  cases L
  · rw [show sum ([]:List α) = (0:α) by rfl]
    sorry
  · sorry

[Matt Diamond]

I don't think you're missing a typeclass... in fact, you have too many!

MulZeroClass extends Mul and Zero, so you should remove Mul and Zero from the mul_sum assumptions

things tend to go wrong when you add redundant instances

[Matt Diamond]

you also don't need the [Add α] assumption in mul_cons, though I don't think that's actively doing any harm

[Colin Jones ⚛️]

If I remove Mul and Zero it causes an error with the functions of sum and mul_cons because it fails to synthesize the instances. Is there a way to tell lean that MulZeroClass includes them so no problem?

[Matt Diamond]

I'm not sure what you mean... you don't need to remove them everywhere, just in mul_sum

this isn't giving me any issues (at least not with the latest version of Mathlib):

import Mathlib

-- Through Polymorphic Definitions
def sum [Add α] [Zero α] : List α → α
  | [] => 0
  | x :: L => x + sum L

def mul_cons [Mul α] : α → List α → List α
  | _, [] => []
  | a, x::L => List.append [x * a] (mul_cons a L)

theorem mul_sum [MulZeroClass α] [Add α] (a : α) (L : List α) :
  a * sum L = sum (mul_cons a L) := by
  induction L with
  | nil =>
    rw [show sum ([]:List α) = (0:α) by rfl]
    simp [sum, mul_cons]
  | cons h t IH =>
    simp only [sum, mul_cons]
    sorry

[Matt Diamond]

@Colin Jones ⚛️ I was able to finish the proof this way:

import Mathlib

-- Through Polymorphic Definitions
def sum [Add α] [Zero α] : List α → α
  | [] => 0
  | x :: L => x + sum L

def mul_cons [Mul α] : α → List α → List α
  | _, [] => []
  | a, x::L => List.append [a * x] (mul_cons a L)

theorem mul_sum [MulZeroClass α] [Add α] [LeftDistribClass α] (a : α) (L : List α) :
  a * sum L = sum (mul_cons a L) := by
  induction L with
  | nil => simp [sum, mul_cons]
  | cons h t IH => simp [sum, mul_cons, left_distrib, IH]

[Matt Diamond]

note that I reversed the order of x * a to a * x in mul_cons to avoid needing commutativity of multiplication

[Matt Diamond]

also tried to keep the typeclass requirements to a bare minimum, since it sounded like that was your goal