Source

Probability / EventAlgebra.agda

open import Level
open import Algebra
module EventAlgebra (algebra : BooleanAlgebra zero zero) where
  open import Relation.Binary
  module BA = BooleanAlgebra algebra  renaming (
       Carrier to Event ;
       ⊤ to Ω ;
       ⊥ to ∅ ;
       _∧_ to _∩_ ; 
       _∨_ to _∪_ ;
       ¬_ to ∁_;
       ¬-cong to ∁-cong)
  open BA public
  import Algebra.Props.BooleanAlgebra as B'
  private module B = B' algebra
  import Algebra.FunctionProperties as FP
  open import Algebra.Structures
  open FP _≈_
  abstract
    csr : CommutativeSemiring zero zero
    csr = B.∨-∧-commutativeSemiring 
    private module CC = CommutativeSemiring csr

    _∖_ : Op₂ Event
    a ∖ b = a ∩ ∁ b
    
    _⊥_ : Rel Event zero
    e₁ ⊥ e₂ = e₁ ∩ e₂ ≈ ∅
  
    import Relation.Binary.EqReasoning as ER
    open ER {{...}}
    open import Data.Product 

 

    ⊥-sym : Symmetric _⊥_
    ⊥-sym a∩b≈∅ = trans (∧-comm _ _) a∩b≈∅ 

    ⊥-subst₂ :  {c a b}  a ≈ b  c ⊥ a   c ⊥ b
    ⊥-subst₂  a≈b c⊥a =  trans (∧-cong refl (sym a≈b)) c⊥a
    
    ⊥-subst₁ :  {c a b}  c ≈ b  c ⊥ a   b ⊥ a
    ⊥-subst₁ c≈b c⊥a = ⊥-sym (⊥-subst₂ c≈b (⊥-sym c⊥a))

    ⊥-subst : _⊥_ Respects₂ _≈_ 
    ⊥-subst = ( ⊥-subst₂ , ⊥-subst₁) 

    e⊥∅ :  e  e ⊥ ∅
    e⊥∅  = proj₂ CC.zero 

    ∅⊥e :  e   ∅ ⊥ e
    ∅⊥e = proj₁ CC.zero

   
    open Poset B.poset  public using () renaming (_≤_ to _⊆_)

    e₁⊆e₂→e₁∪e₂≈e₂ :  e₁ e₂  e₁ ⊆ e₂  (e₁ ∪ e₂) ≈ e₂
    e₁⊆e₂→e₁∪e₂≈e₂ e₁ e₂ e₁⊆e₂ = 
      begin
        e₁ ∪ e₂
      ≈⟨ ∨-cong e₁⊆e₂ refl ⟩
        (e₁ ∩ e₂) ∪ e₂
      ≈⟨ ∨-comm _ _ ⟩
        e₂ ∪ e₁ ∩ e₂
      ≈⟨ ∨-cong refl (∧-comm _ _)        e₂ ∪ (e₂ ∩ e₁)
      ≈⟨ proj₁ absorptive _ _ ⟩
        e₂

    -- Ниже - куча игр с ассоциативностью и коммутативностью. Вот тут бы тактика была бы очень к месту
    -- Мне достаточно коммутативного моноида, но у меня есть Почти Коммутативное Кольцо
    private import Algebra.RingSolver.AlmostCommutativeRing
    -- на которором существующий ring-solver уже работает. Но он, гад, не использует рефлекшн (или я не нашел?)
    -- по этому настоящей годной тактикой не является. Все есть в агде для этого. Кто бы из практиков написал?
    -- Мне вот влом :(

    ∩-monotonic : _∩_ Preserves₂ _⊆_ ⟶ _⊆_ ⟶ _⊆_
    ∩-monotonic {e₁}  {e₃} {e₂} {e₄} e₁⊆e₃ e₂⊆e₄ = 
      begin
        e₁ ∩ e₂
      ≈⟨ ∧-cong e₁⊆e₃ e₂⊆e₄ ⟩
        (e₁ ∩ e₃)(e₂ ∩ e₄)
      ≈⟨ ∧-assoc _ _ _ ⟩
        e₁ ∩ (e₃ ∩ (e₂ ∩ e₄))
      ≈⟨ ∧-cong refl (sym (∧-assoc _ _ _))        e₁ ∩ ((e₃ ∩ e₂) ∩ e₄)
      ≈⟨ ∧-cong refl (∧-cong (∧-comm _ _) refl)        e₁ ∩ ((e₂ ∩ e₃) ∩ e₄)
      ≈⟨ ∧-cong refl ( ∧-assoc _ _ _)        e₁ ∩ (e₂ ∩ (e₃ ∩ e₄))
      ≈⟨ sym (∧-assoc _ _ _)        (e₁ ∩ e₂) ∩ e₃ ∩ e₄
    open CommutativeSemiring B.∨-∧-commutativeSemiring  public using () renaming (+-monoid to ∪-monoid)

    e∪∅≈e :  e  e ∪ ∅ ≈ e
    e∪∅≈e = proj₂ CC.+-identity
 
    e₁∪e₂∖e₁≈e₂ :  {e₁ e₂}  e₁ ⊆ e₂    e₁ ∪ (e₂ ∖ e₁) ≈ e₂
    e₁∪e₂∖e₁≈e₂ {e₁} {e₂}  e₁⊆e₂ =  
      begin
        e₁ ∪ (e₂ ∖ e₁)
      ≈⟨ refl ⟩
        e₁ ∪ (e₂ ∩ ∁ e₁ )
      ≈⟨ ∨-comm _ _ ⟩
       (e₂ ∩ ∁ e₁ ) ∪ e₁
  
      ≈⟨ ∨-∧-distribʳ _ _ _ ⟩
        (e₂ ∪ e₁)(∁ e₁ ∪ e₁)
    
      ≈⟨ ∧-cong  (∨-comm _ _) refl ⟩ 
        (e₁ ∪ e₂)(∁ e₁ ∪ e₁)
      ≈⟨ ∧-cong (e₁⊆e₂→e₁∪e₂≈e₂ _ _ e₁⊆e₂) (proj₁ B.∨-complement _)        e₂ ∩ Ω
      ≈⟨ proj₂ CC.*-identity _ ⟩
        e₂


    e₁⊥e₂∖e₁ :  e₁ e₂  e₁ ⊥ (e₂ ∖ e₁)
    e₁⊥e₂∖e₁ e₁ e₂ = 
      begin
        e₁ ∩ e₂ ∖ e₁
      ≈⟨ refl ⟩
        e₁ ∩ (e₂ ∩ ∁ e₁)
      ≈⟨ ∧-cong refl (∧-comm _ _)        e₁ ∩ (∁ e₁ ∩ e₂)
      ≈⟨ sym (∧-assoc _ _ _)        (e₁ ∩ ∁ e₁) ∩ e₂
      ≈⟨ ∧-cong ( proj₂ B.∧-complement  e₁ ) refl ⟩
        ∅ ∩ e₂
      ≈⟨ ∅⊥e _ ⟩


    e⊆Ω :  e  e ⊆ Ω
    e⊆Ω e = sym (proj₂ CC.*-identity _)