addList_assoc

Stream: new members

[Iocta]

Am I on the right track here? How can I finish?

import Mathlib

def addOptionAll [Semiring α] : Option α → Option α → α
  | none, none => 0
  | none, some y => y
  | some x, none => x
  | some x, some y => x + y

lemma addOptionAll_assoc [Semiring α] (ma mb mc : Option α) :
  addOptionAll (some (addOptionAll ma mb)) mc = addOptionAll ma (some (addOptionAll mb mc)) := by
  unfold addOptionAll
  match ma, mb, mc with
  | none, none, none => simp only
  | some a, none, none => simp only [add_zero]
  | none, some b, none => simp only
  | some a, some b, none => simp only
  | none, none, some c => simp only [zero_add]
  | some a, none, some c => simp only
  | none, some b, some c => simp only
  | some a, some b, some c => simp only [add_assoc]


def addList [Semiring α] (xs ys : List α) : List α :=
  List.zipWithAll addOptionAll xs ys



lemma addList_assoc [Semiring α] (as bs cs : List α) :
  addList (addList as bs) cs = addList as (addList bs cs) := by
  unfold addList
  induction as with
  | nil => {
    rw [List.zipWithAll,List.zipWithAll,]
    simp only [addOptionAll, List.map_id']
  }
  | cons a aa ih => {
    cases bs with
    | nil => {
      rw [List.zipWithAll, List.zipWithAll,]
      simp only [addOptionAll, List.map_cons, List.map_id']
    }
    | cons b bb => {
      rw [List.zipWithAll,]
      cases cs with
      | nil => {
        rw [List.zipWithAll]
        simp only [addOptionAll, List.map_cons, List.map_id', List.zipWithAll_nil_right,
          List.zipWithAll_cons_cons]
      }
      | cons c cc => {
        simp only [List.zipWithAll, addOptionAll, add_assoc, List.cons_inj] at *
        cases aa with
        | nil => {
          simp only [List.zipWithAll_nil_left, addOptionAll, List.map_cons, List.map_id',
            List.zipWithAll_cons_cons] at *
        }
        | cons head tail => {
          rw [List.zipWithAll, addOptionAll] at ih
          simp [List.zipWithAll_cons_cons, List.cons.injEq, addOptionAll] at *
          /-
          case cons.cons.cons.cons
          α : Type u_1
          inst✝ : Semiring α
          a b : α
          bb : List α
          c : α
          cc : List α
          head : α
          tail : List α
          ih : head + b + c = head + (b + c) ∧
            List.zipWithAll addOptionAll (List.zipWithAll addOptionAll tail bb) cc =
              List.zipWithAll addOptionAll tail (List.zipWithAll addOptionAll bb cc)
          ⊢ List.zipWithAll addOptionAll (List.zipWithAll addOptionAll (head :: tail) bb) cc =
            List.zipWithAll addOptionAll (head :: tail) (List.zipWithAll addOptionAll bb cc)
          -/
          sorry
        }
      }
    }
  }

[Eric Wieser]

You would have an easier time if your definition was x.getD 0 + y.getD 0

[Iocta]

Stuck in basically the same place.

def addD0 [Semiring α] (x y : Option α) : α :=
  (x.getD 0) + (y.getD 0)

lemma addD0_assoc [Semiring α] (ma mb mc : Option α) :
  addD0 (some (addD0 ma mb)) mc = addD0 ma (some (addD0 mb mc)) := by
  unfold addD0
  match ma, mb, mc with
  | none, none, none => simp only [Option.getD, add_zero]
  | some a, none, none => simp only [Option.getD_some, Option.getD_none, add_zero]
  | none, some b, none => simp only [Option.getD_none, Option.getD_some, zero_add, add_zero]
  | some a, some b, none => simp only [Option.getD_some, Option.getD_none, add_zero]
  | none, none, some c => simp only [Option.getD_none, add_zero, Option.getD_some, zero_add]
  | some a, none, some c => simp only [Option.getD_some, Option.getD_none, add_zero, zero_add]
  | none, some b, some c => simp only [Option.getD_none, Option.getD_some, zero_add]
  | some a, some b, some c => simp only [Option.getD_some, add_assoc]

def addList [Semiring α] : List α → List α → List α :=
  List.zipWithAll addD0

lemma addList_assoc [Semiring α] (as bs cs : List α) :
  addList (addList as bs) cs = addList as (addList bs cs) := by
  unfold addList
  induction as with
  | nil => simp only [List.zipWithAll, addD0, Option.getD_none, Option.getD_some, zero_add, List.map_id']
  | cons a aa ih => {
    cases bs with
    | nil => simp only [List.zipWithAll_nil_right, addD0, Option.getD_some, Option.getD_none, add_zero,
        List.map_id', List.zipWithAll_nil_left, zero_add, List.map_cons] at *
    | cons b bb => {
      simp only [List.zipWithAll_cons_cons, addD0, Option.getD]
      cases cs with
      | nil => simp only [List.zipWithAll, addD0, Option.getD_some, Option.getD_none, add_zero,
          List.map_cons, List.map_id']
      | cons c cc => {
        simp only [List.zipWithAll_cons_cons, List.cons.injEq] at *
        simp only [addD0, Option.getD_some] at *
        simp only [add_assoc, true_and]
        /-
        case cons.cons.cons
        α : Type u_1
        inst✝ : Semiring α
        a : α
        aa : List α
        b : α
        bb : List α
        c : α
        cc : List α
        ih : List.zipWithAll addD0 (List.zipWithAll addD0 aa (b :: bb)) (c :: cc) =
          List.zipWithAll addD0 aa ((b + c) :: List.zipWithAll addD0 bb cc)
        ⊢ List.zipWithAll addD0 (List.zipWithAll addD0 aa bb) cc = List.zipWithAll addD0 aa (List.zipWithAll addD0 bb cc)
        -/
      }
    }
  }

Going down yet another level doesn't seem likely.

import Mathlib

def addD0 [Semiring α] (x y : Option α) : α :=
  (x.getD 0) + (y.getD 0)

lemma addD0_assoc [Semiring α] (ma mb mc : Option α) :
  addD0 (some (addD0 ma mb)) mc = addD0 ma (some (addD0 mb mc)) := by
  unfold addD0
  match ma, mb, mc with
  | none, none, none => simp only [Option.getD, add_zero]
  | some a, none, none => simp only [Option.getD_some, Option.getD_none, add_zero]
  | none, some b, none => simp only [Option.getD_none, Option.getD_some, zero_add, add_zero]
  | some a, some b, none => simp only [Option.getD_some, Option.getD_none, add_zero]
  | none, none, some c => simp only [Option.getD_none, add_zero, Option.getD_some, zero_add]
  | some a, none, some c => simp only [Option.getD_some, Option.getD_none, add_zero, zero_add]
  | none, some b, some c => simp only [Option.getD_none, Option.getD_some, zero_add]
  | some a, some b, some c => simp only [Option.getD_some, add_assoc]

def addList [Semiring α] : List α → List α → List α :=
  List.zipWithAll addD0

lemma addList_assoc [Semiring α] (as bs cs : List α) :
  addList (addList as bs) cs = addList as (addList bs cs) := by
  unfold addList
  induction as with
  | nil => simp only [List.zipWithAll, addD0, Option.getD_none, Option.getD_some, zero_add, List.map_id']
  | cons a aa ih => {
    cases bs with
    | nil => simp only [List.zipWithAll_nil_right, addD0, Option.getD_some, Option.getD_none, add_zero,
        List.map_id', List.zipWithAll_nil_left, zero_add, List.map_cons] at *
    | cons b bb => {
      simp only [List.zipWithAll_cons_cons, addD0, Option.getD]
      cases cs with
      | nil => simp only [List.zipWithAll, addD0, Option.getD_some, Option.getD_none, add_zero,
          List.map_cons, List.map_id']
      | cons c cc => {
        simp only [List.zipWithAll_cons_cons, List.cons.injEq] at *
        simp only [addD0, Option.getD_some] at *
        simp only [add_assoc, true_and]
        cases aa with
        | nil => simp only [List.zipWithAll_nil_left, addD0, Option.getD_none, Option.getD_some, zero_add,
            List.map_cons, List.map_id', List.zipWithAll_cons_cons] at *
        | cons a' aa' => {
          simp [addD0, add_assoc] at *
          /-
          case cons.cons.cons.cons
          α : Type u_1
          inst✝ : Semiring α
          a b : α
          bb : List α
          c : α
          cc : List α
          a' : α
          aa' : List α
          ih : List.zipWithAll addD0 (List.zipWithAll addD0 aa' bb) cc = List.zipWithAll addD0 aa' (List.zipWithAll addD0 bb cc)
          ⊢ List.zipWithAll addD0 (List.zipWithAll addD0 (a' :: aa') bb) cc =
            List.zipWithAll addD0 (a' :: aa') (List.zipWithAll addD0 bb cc)
          -/
        }
      }
    }
  }

[Daniel Weber]

lemma addD0_assoc [Semiring α] (ma mb mc : Option α) :
  addD0 (some (addD0 ma mb)) mc = addD0 ma (some (addD0 mb mc)) := by
  unfold addD0
  rw [Option.getD_some, add_assoc]

works for addD0_assoc.

[Markus Himmel]

I would do it like this:

lemma addList_assoc [Semiring α] (as bs cs : List α) :
    addList (addList as bs) cs = addList as (addList bs cs) := by
  apply List.ext_get?
  intro n
  simp only [addList, List.zipWithAll_get?]
  cases as.get? n <;> cases bs.get? n <;> cases cs.get? n <;> simp [addD0, add_assoc]