Probability / Numbers.agda

open import Algebra
module Numbers  where
open import Level
open import Relation.Binary 
record Nums  : Setwhere
  field
    commRing : CommutativeRing zero zero
  module CR = CommutativeRing commRing hiding ( isEquivalence   ; trans ; zero ; reflexive) renaming (Carrier to Num)
  open CR 
  field
    _≤_ : Rel Num _
    isTotalOrder : IsTotalOrder _≈_ _≤_
  0≤_ : Num  Set 
  0≤_ n = 0# ≤ n
  field
    +-monotonicity : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
    0≤1 : 01#
  totalOrder : TotalOrder zero zero zero
  totalOrder = record { Carrier = Num; _≈_ = _≈_; _≤_ = _≤_; isTotalOrder = isTotalOrder }

  module TO = TotalOrder totalOrder hiding (_≤_ ; _≈_ ; isTotalOrder ; refl)
  open TO public
  
  open CR public 
  import Relation.Binary.PartialOrderReasoning as POR
  open POR {{...}}
  open import Data.Product using (proj₁ ; proj₂)

  0≤b→a+b≈c→a≤c :  {a b c}    0# ≤ b  a + b ≈ c   a ≤ c
  0≤b→a+b≈c→a≤c  {a} {b} {c} 0≤b a+b≈c  = 
    begin
      a
    ≈⟨ sym (proj₂ +-identity _)      a + 0#
    ≤⟨ +-monotonicity (reflexive refl) 0≤b ⟩
      a + b
    ≈⟨ a+b≈c ⟩
      c
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.