cartesianProduct_zipWith

Stream: new members

[Iocta]

I want to prove cartesianProduct distributes over zipWith, which I think is true but I'm missing the last part of it.

import Mathlib

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⟩


def cartesianProduct (f : α → α → α): List α → List α → List α
  | _, [] => []
  | as, b::bs => (List.map (fun a => f a b) as) ++ (cartesianProduct f as bs)

lemma cartesianProduct_nil (f : α → α → α) (as : List α) : cartesianProduct f as [] = [] := by
  unfold cartesianProduct
  rfl

lemma nil_cartesianProduct (f : α → α → α) (bs : List α) : cartesianProduct f [] bs  = [] := by
  unfold cartesianProduct
  induction bs with
  | nil => simp only
  | cons head tail ih => {
    unfold cartesianProduct
    simp only [List.map_append, List.nil_append, List.map_nil, ih]
  }

def srZipWith [sr : MySemiring α] : List α → List α → List α := List.zipWith sr.add

def srProd [sr : MySemiring α] : List α → List α → List α := cartesianProduct sr.mul

def xs : List ℤ := [1,2,3]
def ys : List ℤ := [10, 20, 30]
def zs : List ℤ := [100, 200, 300]
#test srProd xs (srZipWith ys zs) = srZipWith (srProd xs ys) (srProd xs zs)

lemma srProd_srZipWith [sr : MySemiring α] (as bs cs : List α) :
  srProd as (srZipWith bs cs) = srZipWith (srProd as bs) (srProd as cs) := by
  induction cs with
  | nil => {
    unfold srZipWith srProd
    simp only [List.zipWith_nil, cartesianProduct_nil sr.mul]
  }
  | cons headc tailc ihc => {
    cases bs with
    | nil => {
      rw [srZipWith,]
      simp [List.zipWith_nil]
      unfold srProd
      rw [cartesianProduct_nil, List.nil_zipWith]
    }
    | cons headb tailb => {
      rewrite [srZipWith, List.zipWith, ←srZipWith]
      /-
      case cons.cons
      α : Type
      sr : MySemiring α
      as : List α
      headc : α
      tailc : List α
      headb : α
      tailb : List α
      ihc : srProd as (srZipWith (headb :: tailb) tailc) = srZipWith (srProd as (headb :: tailb)) (srProd as tailc)
      ⊢ srProd as (MySemiring.add headb headc :: srZipWith tailb tailc) =
        srZipWith (srProd as (headb :: tailb)) (srProd as (headc :: tailc))
      -/
      sorry
    }
  }

[Bolton Bailey]

Just at a glance, but I see you have proven lemmas for cartesianProduct_nil, perhaps what you need is cartesianProduct_cons?

[Iocta]

So far whenever I've felt the need for cartesianProduct_cons I've been able to use rw [cartesianProduct], as far as I can tell.