{-# OPTIONS --cubical --safe #-}

module ProbabilityModule.Semirings.Nat where

open import ProbabilityModule.Semirings
open import Cubical.Relation.Everything
open import Cubical.Core.Everything
open import Cubical.Relation.Everything
open import Cubical.Foundations.Prelude hiding (_≡⟨_⟩_)
open import Cubical.HITs.SetTruncation
open import ProbabilityModule.Utils
open import Cubical.Data.Empty
open import Cubical.Data.Nat hiding (+-assoc)
open import Cubical.Data.Nat using (ℕ; suc; zero) public

ℕ-+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
ℕ-+-assoc zero y z = refl
ℕ-+-assoc (suc x) y z = cong suc (ℕ-+-assoc x y z)

*-identityʳ : ∀ x → x *  ≡ x
*-identityʳ zero = refl
*-identityʳ (suc x) = cong suc (*-identityʳ x)

zeroʳ : ∀ x → x *  ≡ 
zeroʳ zero = refl
zeroʳ (suc x) = zeroʳ x

*-distribˡ : ∀ x y z → x * (y + z) ≡ x * y + x * z
*-distribˡ zero y z = refl
*-distribˡ (suc x) y z =
  y + z + x * (y + z) ≡⟨ cong (y + z +_) (*-distribˡ x y z) ⟩
  y + z + (x * y + x * z) ≡˘⟨ ℕ-+-assoc (y + z) _ _ ⟩
  (y + z + x * y) + x * z ≡⟨ cong (_+ x * z) (ℕ-+-assoc y z _) ⟩
  (y + (z + x * y)) + x * z ≡⟨ cong (λ zxy → y + zxy + x * z) (+-comm z _) ⟩
  (y + (x * y + z)) + x * z ≡⟨ ℕ-+-assoc y _ _ ⟩
  y + ((x * y + z) + x * z) ≡⟨ cong (y +_) (ℕ-+-assoc (x * y) _ _) ⟩
  y + (x * y + (z + x * z)) ≡˘⟨ ℕ-+-assoc y (x * y) _ ⟩
  y + x * y + (z + x * z) ∎

*-distribʳ : ∀ x y z → (x + y) * z ≡ x * z + y * z
*-distribʳ zero y z = refl
*-distribʳ (suc x) y z =
  z + (x + y) * z ≡⟨ cong (z +_) (*-distribʳ x y z) ⟩
  z + (x * z + y * z) ≡˘⟨ ℕ-+-assoc z (x * z) (y * z) ⟩
  z + x * z + y * z ∎

*-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z)
*-assoc zero y z = refl
*-assoc (suc x) y z =
  (y + x * y) * z ≡⟨ *-distribʳ y (x * y) z ⟩
  y * z + (x * y) * z ≡⟨ cong (y * z +_) (*-assoc x y z) ⟩
  y * z + x * (y * z) ∎

+-*-𝕊 : Semiring _
+-*-𝕊 = record
  { R = ℕ
  ; _+_ = _+_
  ; _*_ = _*_
  ; 0# = 
  ; 1# = 
  ; +-assoc = ℕ-+-assoc
  ; *-assoc = *-assoc
  ; *0 =  zeroʳ
  ; 0* = λ _ → refl
  ; 0+ = λ _ → refl
  ; *1 = *-identityʳ
  ; 1* = +-zero
  ; +-comm = +-comm
  ; *⟨+⟩ = *-distribˡ
  ; ⟨+⟩* = *-distribʳ
  ; sIsSet = Discrete→isSet discreteℕ
  }