Polynomial proofs

Stream: new members

[Iocta]

I'm stuck on proving zero_add for MyPolynomial Int. I'm guessing it's because I defined MyPolynomial.add with reference to a.sr, but I don't know how to fix it.

import Mathlib

variable {α : Type}

structure MySemiring where
  zero : α
  add : α → α → α
  add_zero a : add a zero = a
  zero_add a : add zero a = a
  one : α
  mul : α → α → α
  mul_one a : mul a one = a
  one_mul a : mul one a = a
  mul_add a b c : mul a (add b c) = add (mul a b) (mul a c)
  add_mul a b c : mul (add a b) c = add (mul a c) (mul b c)

def MyIntSemiring : @MySemiring ℤ :=
  ⟨(0:ℤ), HAdd.hAdd, add_zero, zero_add, (1:ℤ), HMul.hMul, mul_one, one_mul, mul_add, add_mul⟩


structure MyPolynomial where
  sr : @MySemiring α
  coeffs : List α

def zipWithFill (f : α → α → α) (z : α) (as bs : List α) : List α :=
  match as, bs with
  | a::as, b::bs => (f a b) :: zipWithFill f z as bs
  | a::as, _ => (f a z) :: zipWithFill f z as []
  | [], b::bs => (f z b) :: zipWithFill f z [] bs
  | _, _ => []


def MyPolynomial.add (a b : @MyPolynomial α) : (@MyPolynomial α) :=
  ⟨ a.sr, zipWithFill a.sr.add a.sr.zero a.coeffs b.coeffs ⟩

lemma my_int_polynomial_add_zero (pa : @MyPolynomial ℤ) :
  MyPolynomial.add pa { sr := MyIntSemiring, coeffs := [] } = pa := by
    unfold MyPolynomial.add
    simp only
    have : zipWithFill pa.sr.add pa.sr.zero pa.coeffs [] = pa.coeffs
    {
      induction pa.coeffs with
      | nil => rfl
      | cons head tail ih => { unfold zipWithFill; rw [pa.sr.add_zero, ih] }
    }
    rw [this]


lemma my_int_polynomial_zero_add (pb : @MyPolynomial ℤ) :
  MyPolynomial.add { sr := MyIntSemiring, coeffs := [] } pb = pb := by
    unfold MyPolynomial.add
    simp only
/-
α : Type
pb : MyPolynomial
⊢ { sr := MyIntSemiring, coeffs := zipWithFill MyIntSemiring.add MyIntSemiring.zero [] pb.coeffs } = pb
-/
  sorry

[Iocta]

(bump)

[Bolton Bailey]

It seems like what you need is a proof that zipWithFill _ _ [] x = x, perhaps extract that as an intermediate lemma?

[Bolton Bailey]

Also side note: docs#Polynomial is defined with the semiring instance as one of the arguments to the structure definition, so it is a bit odd looking here to see it as a field of the structure itself

[Iocta]

This doesn't seem like it's gonna work: I won't be able to unify MyIntSemiring with MySemiring.

lemma zipWithFill_empty (f : α → α → α) (z : α) (zero_f : ∀(b:α), f z b = b) (bs : List α) :
  zipWithFill f z [] bs = bs := by
  induction bs with
  | nil => rfl
  | cons head tail ih => {
      unfold zipWithFill
      rw [zero_f head, ih]
  }


lemma my_int_polynomial_zero_add (pb : @MyPolynomial ℤ) :
  MyPolynomial.add { sr := MyIntSemiring, coeffs := [] } pb = pb := by
    unfold MyPolynomial.add
    simp only
    rw [zipWithFill_empty MyIntSemiring.add MyIntSemiring.zero MyIntSemiring.zero_add pb.coeffs]
    let ⟨pbsr, pbcoeffs⟩ := pb
    /-
    α : Type
    pb : MyPolynomial
    pbsr : MySemiring
    pbcoeffs : List ℤ
    ⊢ { sr := MyIntSemiring, coeffs := { sr := pbsr, coeffs := pbcoeffs }.coeffs } = { sr := pbsr, coeffs := pbcoeffs }
    -/

[Bolton Bailey]

I think the issue may be the semiring instance argument thing. What guarantee is there that the semiring instance of pb is MyIntSemiring?

[Bolton Bailey]

Spoilers:

import Mathlib

variable {α : Type}

class MySemiring (α : Type) where
  zero : α
  add : α → α → α
  add_zero a : add a zero = a
  zero_add a : add zero a = a
  one : α
  mul : α → α → α
  mul_one a : mul a one = a
  one_mul a : mul one a = a
  mul_add a b c : mul a (add b c) = add (mul a b) (mul a c)
  add_mul a b c : mul (add a b) c = add (mul a c) (mul b c)

instance MyIntSemiring : MySemiring ℤ :=
  ⟨(0:ℤ), HAdd.hAdd, add_zero, zero_add, (1:ℤ), HMul.hMul, mul_one, one_mul, mul_add, add_mul⟩

structure MyPolynomial (α : Type) [MySemiring α] where
  coeffs : List α

def zipWithFill (f : α → α → α) (z : α) (as bs : List α) : List α :=
  match as, bs with
  | a::as, b::bs => (f a b) :: zipWithFill f z as bs
  | a::as, _ => (f a z) :: zipWithFill f z as []
  | [], b::bs => (f z b) :: zipWithFill f z [] bs
  | _, _ => []


def MyPolynomial.add [sr : MySemiring α] (a b : MyPolynomial α) : (MyPolynomial α) :=
  ⟨ zipWithFill sr.add sr.zero a.coeffs b.coeffs ⟩

lemma my_int_polynomial_add_zero (pa : MyPolynomial ℤ) :
  MyPolynomial.add pa { coeffs := [] } = pa := by
    unfold MyPolynomial.add
    simp only
    have : zipWithFill MySemiring.add MySemiring.zero pa.coeffs [] = pa.coeffs
    {
      induction pa.coeffs with
      | nil => rfl
      | cons head tail ih => { unfold zipWithFill; rw [MySemiring.add_zero, ih] }
    }
    rw [this]


lemma zipWithFill_empty (f : α → α → α) (z : α) (zero_f : ∀(b:α), f z b = b) (bs : List α) :
  zipWithFill f z [] bs = bs := by
  induction bs with
  | nil => rfl
  | cons head tail ih => {
      unfold zipWithFill
      rw [zero_f head, ih]
  }


lemma my_int_polynomial_zero_add (pb : MyPolynomial ℤ) :
  MyPolynomial.add { coeffs := [] } pb = pb := by
    unfold MyPolynomial.add
    simp only
    rw [zipWithFill_empty MyIntSemiring.add MyIntSemiring.zero MyIntSemiring.zero_add pb.coeffs]

[Eric Wieser]

Yes, this "bundled Semiring" construction is mathematically nonsense; it forces you to ask the question "when I add p and q, do I use ps addition or qs addition?" which shouldn't be possible to ask in the first place

[Bolton Bailey]

Incidentally @Iocta , I see that you are defining a type for Polynomial based off of lists. I need something similar for one of my projects. Perhaps there is a potential for some synergy here - is there a particular goal you have for creating this List-based polynomial type?

[Iocta]

I'm doing exercises inspired by a course, I don't have any plans to build anything with them.