03-classes.agda

{-# OPTIONS --verbose tc.constr.findInScope:15 #-}

module 03-classes where

open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties
open import Data.Nat.Properties as NatProps
open import Data.Nat
open import Data.Bool.Properties using (isCommutativeSemiring-∧-∨)
open import Data.Product using (proj₁)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary

open import Level renaming (zero to lzero; suc to lsuc)

open CommutativeSemiring NatProps.commutativeSemiring using (semiring)
open IsCommutativeSemiring isCommutativeSemiring using (isSemiring)
open IsCommutativeSemiring isCommutativeSemiring-∧-∨ using () renaming (isSemiring to Bool-isSemiring)

record S (A : Set) : Set₁ where
  field
    z : A
    o : A
    _≈_ : Rel A lzero
    _⟨+⟩_ : Op₂ A
    _⟨*⟩_ : Op₂ A
    isSemiring' : IsSemiring _≈_ _⟨+⟩_ _⟨*⟩_ z o

ℕ-S : S ℕ
ℕ-S = record { z = 0; o = 1;
               _≈_ = _≡_; _⟨+⟩_ = _+_; _⟨*⟩_ = _*_;
               isSemiring' = isSemiring }

zero' : {A : Set} → {{aRing : S A}} → A
zero' {{ARing}} = S.z ARing

zero-nat : ℕ
zero-nat = zero'

zero'' : {A : Set} {_≈_ : Rel A lzero} {_⟨+⟩_ _⟨*⟩_ : Op₂ A} {z o : A} →
         {{isr : IsSemiring _≈_ _⟨+⟩_ _⟨*⟩_ z o}} → A
zero'' {z = z} = z

zero-nat' : ℕ
zero-nat' = zero''

isZero : {A : Set} {_≈_ : Rel A lzero} {_⟨+⟩_ _⟨*⟩_ : Op₂ A} {z o : A} →
         {{isr : IsSemiring _≈_ _⟨+⟩_ _⟨*⟩_ z o}} → Zero _≈_ z _⟨*⟩_
isZero {{isr}} = IsSemiring.zero isr

useIsZero : 0 * 5 ≡ 0
useIsZero = proj₁ isZero 5