# Probability / EventAlgebra.agda

 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141``` ```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 _) ```