, Algebra.Ring.Semiring

  proofAssociativity Nothing  _ _ = Refl
  proofAssociativity (Some _) _ _ = Refl

  proofAssociative Nothing  _ _ = Refl
  proofAssociative (Some _) _ _ = Refl

import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid

import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid

import Algebra.Ring.Semiring

[NaturalSumCommutativeMagma] CommutativeMagma Natural using NaturalSumMagma where
  proofCommutative = proofPlusCommutative
public export

  proofAssociativity = proofPlusAssociative

  proofAssociative = proofPlusAssociative
public export
[NaturalSumCommutativeSemigroup] CommutativeSemigroup Natural using NaturalSumCommutativeMagma NaturalSumSemigroup where

[NaturalSumCommutativeMonoid] CommutativeMonoid Natural using NaturalSumCommutativeSemigroup NaturalSumMonoid where
public export

proofMultRightDistributesPlus : (x, y, z : Natural)
                              -> mult (plus x y) z = plus (mult x z) (mult y z)
proofMultRightDistributesPlus x y z =
  rewrite proofMultCommutative (plus x y) z in
  rewrite proofMultLeftDistributesPlus z x y in
  rewrite proofMultCommutative z x in
  rewrite proofMultCommutative z y in
  Refl

  proofAssociativity x y Zero = Refl
  proofAssociativity x y (Succesor z) =

  proofAssociative x y Zero = Refl
  proofAssociative x y (Succesor z) =

    rewrite proofAssociativity x y z in

    rewrite proofAssociative x y z in

public export
Semiring Natural where
  (+) = plus
  (*) = mult
  zero = 0
  one  = 1
  proofSumZero = proofRightIdentity @{NaturalSumMonoid}
  proofSumCommutative = proofCommutative @{NaturalSumCommutativeMagma}
  proofSumAssociative = proofAssociative @{NaturalSumSemigroup}
  proofMultOneLeft  = proofLeftIdentity  @{NaturalMultMonoid}
  proofMultOneRight = proofRightIdentity @{NaturalMultMonoid}
  proofMultAssociative = proofAssociative @{NaturalMultSemigroup}
  proofMultDistributesSumLeft  = proofMultLeftDistributesPlus
  proofMultDistributesSumRight = proofMultRightDistributesPlus
  zeroAnnihilatorLeft  = proofMultLeftAnnihilation
  zeroAnnihilatorRight = proofMultRightAnnihilation

  proofAssociativity Nil     _ _ = Refl
  proofAssociativity (x::xs) y z = rewrite proofAssociativity xs y z in Refl

  proofAssociative Nil     _ _ = Refl
  proofAssociative (x::xs) y z = rewrite proofAssociative xs y z in Refl

  proofAssociativity Nil f g = Refl
  proofAssociativity (x::xs) f g with (f x)
    proofAssociativity (x::xs) f g | Nil = rewrite proofAssociativity xs f g in Refl
    proofAssociativity (x::xs) f g | (r::rs) = ?holeAssociativity

  proofAssociative Nil f g = Refl
  proofAssociative (x::xs) f g with (f x)
    proofAssociative (x::xs) f g | Nil = rewrite proofAssociative xs f g in Refl
    proofAssociative (x::xs) f g | (r::rs) = ?holeAssociative

  proofAssociativity (Left  _) f g = Refl
  proofAssociativity (Right _) f g = Refl

  proofAssociative (Left  _) f g = Refl
  proofAssociative (Right _) f g = Refl

import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order

import Algebra.Group.Monoid

import Algebra.Group.Monoid

import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order

  proofCommutativity = proofDisjCommutative

  proofCommutative = proofDisjCommutative

  proofAssociativity False b c =

  proofAssociative False b c =

  proofAssociativity True b c = Refl

  proofAssociative True b c = Refl

  proofCommutativity = proofConjCommutative

  proofCommutative = proofConjCommutative

  proofAssociativity False b c = Refl
  proofAssociativity True  b c =

  proofAssociative False b c = Refl
  proofAssociative True  b c =

  proofAssociative = proofAssociativity @{BooleanConjSemigroup}

  proofAssociative = proofAssociative @{BooleanConjSemigroup}

  proofAssociative = proofAssociativity @{BooleanDisjSemigroup}

  proofAssociative = proofAssociative @{BooleanDisjSemigroup}

  proofAssociativity = believe_me ()

  proofAssociative = believe_me ()

module Algebra.Ring.Semiring
import Builtin
import Algebra.Group.Magma
import Algebra.Group.Monoid
infixl 5 +
infixl 6 *
public export
interface Semiring t where
  (+) : t -> t -> t
  (*) : t -> t -> t
  zero : t
  one  : t
  proofSumZero : (x : t) -> x + zero = x
  proofSumCommutative : (x, y : t) -> x + y = y + x
  proofSumAssociative : (x, y, z : t) -> x + (y + z) = (x + y) + z
  proofMultOneLeft  : (x : t) -> one * x = x
  proofMultOneRight : (x : t) -> x * one = x
  proofMultAssociative : (x, y, z : t) -> x * (y * z) = (x * y) * z
  proofMultDistributesSumLeft : (x, y, z : t) -> x * (y + z) = x * y + x * z
  proofMultDistributesSumRight : (x, y, z : t) -> (x + y) * z = x * z + y * z
  zeroAnnihilatorLeft : (x : t) -> zero * x = zero
  zeroAnnihilatorRight : (x : t) -> x * zero = zero

  proofAssociativity : (x, y, z : t) -> x <> (y <> z) = (x <> y) <> z

  proofAssociative : (x, y, z : t) -> x <> (y <> z) = (x <> y) <> z

  proofCommutativity : (x, y : t) -> x <> y = y <> x

  proofCommutative : (x, y : t) -> x <> y = y <> x

  proofAssociativity : (x : t a) -> (f : a -> t b) -> (g : b -> t c)

  proofAssociative : (x : t a) -> (f : a -> t b) -> (g : b -> t c)