Probability / Probability.agda

import EventAlgebra
open import Numbers 
 
module Probability (nums : Nums) (ba : _) where
private open module EA = EventAlgebra ba hiding (_≈_ ; sym)
private open Nums nums hiding (_≈_; sym)
private import FinAdditives as FA
private open FA +-monoid renaming (sum to Σ_ ;  a∙b≈sum[a,b] to a+b≈Σ[a,b])
private open FA ∪-monoid renaming (sum to ∪_ ; a∙b≈sum[a,b] to a∪b≈∪[a,b] ; sum[]≈ε to ∪[]≈∅ ; a≈sum[a] to a≈∪[a])
private import Algebra.Structures

private open import Relation.Binary 
private open Setoid {{...}} public hiding (sym)
private open IsEquivalence {{...}} 
private open import Data.List
private open import Algebra

-- Вроде хорошее, годное определение "попарно непересекающиеся".
-- Что-то я навскидку к первым принципам не смог свести.
data ⊥_ : List Event  Set where
  [] : ⊥ []
  _∷_ :  {e l}  e ⊥ (∪ l)  ⊥ l (e ∷ l)

-- формулировка сделана в классическом стиле "множеста попарно-непересекающихся событий". Если пойти просто от
-- пары - все бы стало намного проще. Но что сделано - то сделано. 
record Axioms : Set where
  field
    P : Event  Num
    P-cong : P Preserves _≈_ ⟶ _≈_
    a₁ :  e  0≤ P e
    a₂ : P Ω ≈ 1#
    a₃ : {l}  ⊥ l  P (∪ l) ≈ Σ (map P l)
     
module Consequencses (ax : Axioms) where
  open Axioms ax 
  open import Data.Product using (proj₁ ; proj₂)

  abstract


          import Relation.Binary.EqReasoning as EqR 
          open EqR {{...}} 

          -- Вот все эти игры ниже - от классической, "кривой" аксиоматики
          ⊥[a,b]̄→a⊥b :  {a b} (a ∷ b ∷ [])  a ⊥ b
          ⊥[a,b]̄→a⊥b ( a⊥∅∪b ∷ _) = ⊥-subst₂ (sym (a≈∪[a] _)) a⊥∅∪b

          a⊥b→⊥[a,b] :  {a b}  a ⊥ b (a ∷ b ∷ [])
          a⊥b→⊥[a,b] a⊥b =  ⊥-subst₂ (a≈∪[a] _) a⊥b ∷ ⊥-subst₂ (sym ∪[]≈∅) (e⊥∅ _) ∷ []

          -- Вот это стоило взять аксиомой
          e₁⊥e₂→Pe₁+Pe₂≈Pe₁∪e₂ : {e₁ e₂}  e₁ ⊥ e₂  P e₁ + P e₂ ≈ P (e₁ ∪ e₂)  
          e₁⊥e₂→Pe₁+Pe₂≈Pe₁∪e₂ {e₁} {e₂} e₁⊥e₂ = 
            begin
              P e₁ + P e₂
            ≈⟨ a+b≈Σ[a,b] _ _ ⟩ 
              Σ _
            ≈⟨ sym (a₃ (a⊥b→⊥[a,b] e₁⊥e₂))              P (∪ _)
            ≈⟨ P-cong (EA.sym (a∪b≈∪[a,b] _ _))              P (e₁ ∪ e₂)

          private
            Pe+P∅≈Pe :  e  (P e + P ∅) ≈ P e
            Pe+P∅≈Pe e = 
              begin
                P e + P ∅
              ≈⟨ e₁⊥e₂→Pe₁+Pe₂≈Pe₁∪e₂ (e⊥∅ _)                P (e ∪ ∅)
              ≈⟨ P-cong (e∪∅≈e _)                P e
            
          P∅≈0 : P ∅ ≈ 0#
          P∅≈0 = right-identity-unique _ _  (Pe+P∅≈Pe Ω) where
              import Algebra.Props.Group as G
              open G {{...}}
             
          -- монотонность вероятности
          e₁⊆e₂→Pe₁≤Pe₂ :  {e₁ e₂ }  e₁ ⊆ e₂  P e₁ ≤ P e₂
          e₁⊆e₂→Pe₁≤Pe₂ {e₁} {e₂} e₁⊆e₂ =
            let
              e₂′ = e₂ ∖ e₁

              e₁⊥e₂′ : e₁ ⊥ e₂′ 
              e₁⊥e₂′ = e₁⊥e₂∖e₁ _ _

              e₁∪e₂′≈e₂ : (e₁ ∪ e₂′) ≈ e₂
              e₁∪e₂′≈e₂ = e₁∪e₂∖e₁≈e₂ e₁⊆e₂

              Pe₁+Pe₂′≈Pe₂ : P e₁ + P e₂′ ≈ P e₂
              Pe₁+Pe₂′≈Pe₂ = 
                begin
                  P e₁ + P e₂′
                ≈⟨ e₁⊥e₂→Pe₁+Pe₂≈Pe₁∪e₂ e₁⊥e₂′ ⟩
                  P (e₁ ∪ e₂′)
                ≈⟨ P-cong e₁∪e₂′≈e₂ ⟩
                  P e₂

 
            in  
                  0≤b→a+b≈c→a≤c (a₁ _) Pe₁+Pe₂′≈Pe₂
         
          -- лень разбираться с областями видимости и в таскивать PartialOrderReasoning (будет конфликтовать по begin/∎)
          Pe≤1 :  e  P e ≤ 1#
          Pe≤1 e = proj₁ ≤-resp-≈  a₂ (e₁⊆e₂→Pe₁≤Pe₂ (e⊆Ω _))
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.