Multiplication distributes over addition

multDistOverPlus.idr

-- Informal proof:
--==============================================================
--  S a * (b + c)
--= b + c + a * (b + c)         -- definition of *
--= b + c + (a * b) + (a * c)   -- induction hypothesis
--= b + (a * b) + c + (a * c)   -- associativity / commutativity
--= S a * b + S a * c           -- definition of *

-- With all associativity and commutativity manipulations:
--==============================================================
--  S a * (b + c)
--= (b + c) + a * (b + c)     -- definition of *
--= (b + c) + (a * b + a * c) -- induction hypothesis
--= b + (c + (a * b + a * c)) -- associativity
--= b + ((c + a * b) + a * c) -- associativity
--= b + ((a * b + c) + a * c) -- commutativity
--= b + (a * b + (c + a * c)) -- associativity
--= (b + a * b) + (c + a * c) -- associativity
--= S a * b + S a * c         -- definition of *

multDistOverPlus : (a, b, c : Nat) -> a * (b + c) = a * b + a * c
multDistOverPlus Z b c = refl
multDistOverPlus (S a) b c = multDistOverPlusS (multDistOverPlus a b c)
  where
    assoc_right : (b + c) + (a * b + a * c) = b + (c + (a * b + a * c))
    assoc_right = sym (plusAssociative b c (a*b + a*c))

    assoc_left_right_fragment : c + (a * b + a * c) = c + a * b + a * c
    assoc_left_right_fragment = plusAssociative c (a * b) (a * c)

    flip_left_right_fragment : c + a * b + a * c = a * b + c + a * c
    flip_left_right_fragment = cong {f = \x => x + a * c} (plusCommutative c (a * b))

    assoc_right_right_fragment : a * b + c + a * c = a * b + (c + a * c)
    assoc_right_right_fragment = sym $ plusAssociative (a*b) c (a*c)

    assoc_left : b + (a * b + (c + a * c)) = (b + a * b) + (c + a * c)
    assoc_left = plusAssociative b (a*b) (S a * c)

    move_c_over : (b + c) + (a * b + a * c) = (b + a * b) + (c + a * c)
    move_c_over = trans (trans assoc_right (cong {f = \x => b + x} (trans assoc_left_right_fragment (trans flip_left_right_fragment assoc_right_right_fragment)))) assoc_left

    multDistOverPlusS : a * (b + c) = a * b + a * c -> S a * (b + c) = S a * b + S a * c
    multDistOverPlusS p = replace {P = \x => (b + c) + x = (b + a * b) + (c + a * c)} (sym p) move_c_over