Commits

ppavel committed 5f648b1

[mq]: ∪-monoid получен переименованием

Comments (0)

Files changed (4)

EventAlgebra.agda

        ⊤ to Ω ;
        ⊥ to ∅ ;
        _∧_ to _∩_ ; 
-       _∨_ to _∪_ ; 
-       ¬_ to ∁_)
+       _∨_ to _∪_ ;
+       ¬_ to ∁_;
+       ¬-cong to ∁-cong)
   open BA public
-  import Algebra.Props.BooleanAlgebra as B
+  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
     
-  _disj_ : Rel Event zero
-  e₁ disj e₂ = e₁ ∩ e₂ ≈ ∅
+    _⊥_ : Rel Event zero
+    e₁ ⊥ e₂ = e₁ ∩ e₂ ≈ ∅
+  
+    import Relation.Binary.EqReasoning as ER
+    open ER {{...}}
+    open import Data.Product 
 
-  ∪-monoid : Monoid zero zero
-  ∪-monoid = record { -- TODO заиспользовать имеющийся моноид
-      Carrier = Event; _≈_ = _≈_; _∙_ = _∪_; ε = ∅; 
-      isMonoid = IsCommutativeSemiring.+-isMonoid (B.∨-∧-isCommutativeSemiring algebra) }
+ 
 
-  open Poset (B.poset algebra) public using () renaming (_≤_ to _⊆_)
+    ⊥-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 _)
 
  

FinAdditives.agda

 open Monoid m
 abstract
   sum : List Carrier → Carrier
-  sum = foldl _∙_  ε
+  sum = foldl _∙_  ε
+  private  import Relation.Binary.PropositionalEquality as ≡
+  import Relation.Binary.EqReasoning as ER
+  private 
+    open ER {{...}}
+    leftIdentity : (a : Carrier) → ε ∙ a ≈ a 
+    leftIdentity = proj₁ identity where open import Data.Product using (proj₁)
+
+  a≈sum[a] : ∀ a → a ≈ sum (a ∷ [])
+  a≈sum[a] a = sym (leftIdentity a)
+
+  sum[]≈ε : sum [] ≈ ε
+  sum[]≈ε = refl
+
+  -- TODO 
+  -- ∀ a l → a ∙ sum l ≈ sum (a ∷ l) или вообще через конгруэнтости из стандартных свойств списка
+  a∙b≈sum[a,b] :  ∀ a b → a ∙ b ≈ sum (a ∷ b ∷ [])
+  a∙b≈sum[a,b] a b =
+    begin
+       a ∙ b
+     ≈⟨ sym (leftIdentity _) ⟩
+       ε ∙ (a ∙ b) 
+     ≈⟨ sym (assoc _ _ _) ⟩
+       (ε ∙ a) ∙ b
+    ∎ 
+
+  
 open import Algebra
 module Numbers  where
 open import Level
-open import Relation.Binary
+open import Relation.Binary 
 record Nums  : Set₁ where
   field
     commRing : CommutativeRing zero zero
-  module CR = CommutativeRing commRing hiding (zero) renaming (Carrier to Num)
-  open CR
+  module CR = CommutativeRing commRing hiding ( isEquivalence   ; trans ; zero ; reflexive) renaming (Carrier to Num)
+  open CR 
   field
     _≤_ : Rel Num _
-    partialOrder : IsTotalOrder _≈_ _≤_
-  module TO = IsTotalOrder partialOrder hiding (isEquivalence ; refl ; reflexive ; trans) 
-  open TO
+    isTotalOrder : IsTotalOrder _≈_ _≤_
   0≤_ : Num → Set 
   0≤_ n = 0# ≤ n
   field
-    0≤b→a≤a+b : ∀ a → ∀{b} → 0≤ b → a ≤ (a + b)
+    +-monotonicity : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
     0≤1 : 0≤ 1#
+  totalOrder : TotalOrder zero zero zero
+  totalOrder = record { Carrier = Num; _≈_ = _≈_; _≤_ = _≤_; isTotalOrder = isTotalOrder }
 
+  module TO = TotalOrder totalOrder hiding (_≤_ ; _≈_ ; isTotalOrder ; refl)
   open TO public
-  open CR 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
+    ∎
+
 import EventAlgebra
 open import Numbers 
+ 
 module Probability (nums : Nums) (ba : _) where
-open module EA = EventAlgebra ba hiding (_≈_)
-open Nums nums hiding (_≈_)
-import FinAdditives as FA
-open FA +-monoid renaming (sum to Σ_)
-open FA ∪-monoid renaming (sum to ∪_)
-import Algebra.Structures
+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
 
-open import Relation.Binary
-open Setoid {{...}} public
+private open import Relation.Binary 
+private open Setoid {{...}} public hiding (sym)
+private open IsEquivalence {{...}} 
+private open import Data.List
+private open import Algebra
 
-open import Data.List
-open import Algebra
+-- Вроде хорошее, годное определение "попарно непересекающиеся".
+-- Что-то я навскидку к первым принципам не смог свести.
+data ⊥_ : List Event → Set where
+  [] : ⊥ []
+  _∷_ : ∀ {e l} → e ⊥ (∪ l) → ⊥ l → ⊥ (e ∷ l)
 
-data Disjoint : List Event → Set where
-  [] : Disjoint []
-  _∷_ : ∀ {e l} → e disj (∪ l) → Disjoint l → Disjoint (e ∷ l)
-
+-- формулировка сделана в классическом стиле "множеста попарно-непересекающихся событий". Если пойти просто от
+-- пары - все бы стало намного проще. Но что сделано - то сделано. 
 record Axioms : Set where
   field
     P : Event → Num
+    P-cong : P Preserves _≈_ ⟶ _≈_
     a₁ : ∀ e → 0≤ P e
     a₂ : P Ω ≈ 1#
-    a₃ : ∀{l} → Disjoint l → P (∪ l) ≈ Σ (map P l)
+    a₃ : ∀{l} →  l → P (∪ l) ≈ Σ (map P l)
      
-  e₁⊆e₂→Pe₁≤Pe₂ : ∀ {e₁ e₂ } → e₁ ⊆ e₂ → P e₁ ≤ P e₂
-  e₁⊆e₂→Pe₁≤Pe₂ = {!-m!}
+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⊆Ω _))