natural_arithmetic.idr

plus_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> plus a (plus b c) = plus (plus a b) c
plus_assoc Z     b c = Refl
plus_assoc (S a) b c = rewrite plus_assoc a b c in Refl

plus_unit : (a : Nat) -> a = plus a Z
plus_unit Z     = Refl
plus_unit (S a) = rewrite plus_unit a in Refl

plus_commutes_S : (a : Nat) -> (b : Nat) -> S (plus a b) = plus a (S b)
plus_commutes_S Z     b = Refl
plus_commutes_S (S a) b = rewrite plus_commutes_S a b in Refl

plus_commutes : (a : Nat) -> (b : Nat) -> plus a b = plus b a
plus_commutes Z     b = plus_unit b
plus_commutes (S a) b = rewrite plus_commutes a b in plus_commutes_S b a

distributive1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> mult a (plus b c) = plus (mult a b) (mult a c)
distributive1 Z     b c = Refl
distributive1 (S a) b c =
  rewrite distributive1 a b c in
  rewrite plus_assoc (plus b (mult a b)) c (mult a c) in
  rewrite sym (plus_assoc  b (mult a b) c) in
  rewrite plus_commutes (mult a b) c in
  rewrite plus_assoc b c (mult a b) in
  rewrite sym (plus_assoc (plus b c) (mult a b) (mult a c)) in Refl

mult_unit : (a : Nat) -> a = mult a 1
mult_unit Z     = Refl
mult_unit (S a) = rewrite mult_unit a in Refl

mult_zero : (a : Nat) -> Z = mult a Z
mult_zero Z     = Refl
mult_zero (S a) = mult_zero a

mult_commutes_S : (a : Nat) -> (b : Nat) -> mult (S a) b = mult b (S a)
mult_commutes_S a Z     = sym (mult_zero (S a))
mult_commutes_S a (S b) =
  rewrite distributive1 a 1 b in
  rewrite sym (mult_commutes_S a b) in
  rewrite plus_assoc a b (mult a b) in
  rewrite plus_commutes a b in
  rewrite sym (plus_assoc b a (mult a b)) in
  rewrite mult_unit a in Refl

mult_commutes : (a : Nat) -> (b : Nat) -> mult a b = mult b a
mult_commutes Z     b = mult_zero b
mult_commutes (S a) b = mult_commutes_S a b

distributive2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> mult (plus a b) c = plus (mult a c) (mult b c)
distributive2 a b c =
  rewrite mult_commutes a c in
  rewrite mult_commutes b c in
  rewrite sym (distributive1 c a b) in
  rewrite mult_commutes c (plus a b) in Refl

mult_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> mult a (mult b c) = mult (mult a b) c
mult_assoc Z     b c = Refl
mult_assoc (S a) b c =
  rewrite mult_assoc a b c in
  rewrite distributive2 b (mult a b) c in Refl