Browse Source

Finish probability work with a bunch of postulates.

gas-move-test
Thomas Kerber 11 months ago
parent
commit
caf15b9d2f
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
2 changed files with 97 additions and 70 deletions
  1. 51
    48
      Yggdrasil/Probability.agda
  2. 46
    22
      Yggdrasil/Rational.agda

+ 51
- 48
Yggdrasil/Probability.agda View File

@@ -1,38 +1,38 @@
module Yggdrasil.Probability where

open import Data.List using (List; _∷_; []; map; filter; length)
open import Agda.Builtin.FromNat using (Number)
import Data.Nat.Literals as ℕLit
import Data.Rational.Literals as ℚLit
import Data.Integer.Literals as ℤLit
open import Data.List using (List; _∷_; []; map; filter; length; foldr)
open import Data.Fin using (Fin; zero; suc)
open import Data.Integer using (+_; _-_) renaming (_*_ to _ℤ*_)
open import Data.Nat using (ℕ; zero; suc; _≤_; s≤s) renaming (_*_ to _ℕ*_; _≤?_ to _ℕ≤?_)
open import Data.Integer using (ℤ; +_; _-_) renaming (_*_ to _ℤ*_)
open import Data.Nat using (ℕ; zero; suc; s≤s) renaming (_*_ to _ℕ*_; _≤?_ to _ℕ≤?_; _≤_ to _ℕ≤_)
open import Data.Nat.Literals
open import Data.Nat.Properties using (≤-trans; ≤-refl)
open import Data.List.Properties using (length-filter; length-map)
open import Data.Product using (_×_; ∃; ∃-syntax; proj₁) renaming (_,_ to ⟨_,_⟩)
open import Data.Rational using (ℚ; _÷_) renaming (_≤?_ to _ℚ≤?_)
open import Data.Rational using (ℚ) renaming (_≤?_ to _ℚ≤?_; _≤_ to _ℚ≤_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable using (True; fromWitness)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)
open import Level using (Level; Lift; lift) renaming (suc to lsuc)
open import Yggdrasil.List using (_∈_; with-proof)
import Yggdrasil.Rational as ℚ

record [0,1] : Set where
field
q : ℚ
≤1 : True (q ℚ≤? (+ 1 ÷ 1))
0≤ : True ((+ 0 ÷ 1) ℚ≤? q)
instance
ℕnumber : Number ℕ
ℕnumber = ℕLit.number
ℤnumber : Number ℤ
ℤnumber = ℤLit.number
ℚnumber : Number ℚ
ℚnumber = ℚLit.number

interval : (q : ℚ) → {≤1 : True (q ℚ≤? (+ 1 ÷ 1))} →
{0≤ : True ((+ 0 ÷ 1) ℚ≤? q)} → [0,1]
interval q {≤1} {0≤} = record { q = q; ≤1 = ≤1; 0≤ = 0≤ }
case : ℚ → ℚ → ℚ → ℚ
case Pr[A] Pr[B∣A] Pr[B∣¬A] = Pr[A] ℚ.* Pr[B∣A] ℚ.+ (1 ℚ.- Pr[A]) ℚ.* Pr[B∣¬A]

postulate
_ℚ+_ : ℚ → ℚ → ℚ
1-_ : [0,1] → [0,1]
_*_ : [0,1] → [0,1] → [0,1]
case : [0,1] → [0,1] → [0,1] → [0,1]
_/_ : (n : ℕ) → (m : ℕ) → {n≤m : True (n ℕ≤? m)} → [0,1]
sum-[0,1] : List [0,1] → ℚ
-- Absolute difference
_δ_ : [0,1] → [0,1] → [0,1]
sum : List ℚ → ℚ
sum = foldr (ℚ._+_) 0

PrFin : ∀ {ℓ} → ℕ → Set ℓ
PrFin {ℓ} n = Lift ℓ (Fin (suc (suc n)))
@@ -53,43 +53,46 @@ data Dist {ℓ : Level} : Set ℓ → Set (lsuc ℓ) where
sample : ∀ {n : ℕ} → Dist (PrFin n)
bind : ∀ {A B : Set ℓ} → Dist A → (A → Dist B) → Dist B

≡⇒≤ : {a b : ℕ} → a ≡ b → a ≤ b
≡⇒≤ : {a b : ℕ} → a ≡ b → a ≤ b
≡⇒≤ refl = ≤-refl

data Pr[_[_]]≡_ {ℓ : Level} : {A : Set ℓ} → (P : A → Set ℓ) → Dist A →
[0,1] → Set (lsuc ℓ) where
→ Set (lsuc ℓ) where
pure-zero : {A : Set ℓ} {P : A → Set ℓ} → (x : A) → ¬ (P x) →
Pr[ P [ pure x ]]≡ (interval (+ 0 ÷ 1))
Pr[ P [ pure x ]]≡ 0
pure-one : {A : Set ℓ} {P : A → Set ℓ} → (x : A) → P x →
Pr[ P [ pure x ]]≡ (interval (+ 1 ÷ 1))
Pr[ P [ pure x ]]≡ 1
sample-count : {n : ℕ} {P : PrFin n → Set ℓ} →
(dec : (f : PrFin n) → Dec (P f)) →
Pr[ P [ sample {n = n} ]]≡ (_/_ (count dec) (suc (suc n)) {fromWitness (
≤-trans (length-filter dec (map lift (all-fin (suc (suc n)))))
(s≤s (s≤s (≡⇒≤
(trans (length-map lift (map suc (map suc (all-fin n))))
(trans (length-map suc (map suc (all-fin n)))
(trans (length-map suc (all-fin n)) (length-all-fin n)))))))
)})
Pr[ P [ sample {n = n} ]]≡ (+ (count dec) ℚ.÷ (suc (suc n)))
conditional : {A B : Set ℓ} {D : Dist A} {f : A → Dist B} {P₁ : A → Set ℓ}
{P₂ : B → Set ℓ} {p₁ p₂ p₃ : [0,1]} →
{P₂ : B → Set ℓ} {p₁ p₂ p₃ : ℚ} →
Pr[ P₁ [ D ]]≡ p₁ →
((x : A) → P₁ x → Pr[ P₂ [ f x ]]≡ p₂) →
((x : A) → ¬ (P₁ x) → Pr[ P₂ [ f x ]]≡ p₃) →
Pr[ P₂ [ bind D f ]]≡ (case p₁ p₂ p₃)

data _≈[_]≈_ {ℓ : Level} {A : Set ℓ} : Dist A → ℚ → Dist A → Set (lsuc ℓ) where
finite : (d₁ d₂ : Dist A) → (xs : List A) →
(pr₁ : (x : A) → x ∈ xs → ∃[ p ] Pr[ _≡ x [ d₁ ]]≡ p) →
(pr₂ : (x : A) → x ∈ xs → ∃[ p ] Pr[ _≡ x [ d₂ ]]≡ p) →
(ε : ℚ) →
sum-[0,1] (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₁ x x∈xs)
}) (with-proof xs)) ≡ + 1 ÷ 1 →
sum-[0,1] (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₂ x x∈xs)
}) (with-proof xs)) ≡ + 1 ÷ 1 →
sum-[0,1] (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₁ x x∈xs) δ proj₁ (pr₂ x x∈xs)
}) (with-proof xs)) ≡ ε →
d₁ ≈[ ε ]≈ d₂
record _≈[_]≈_ {ℓ : Level} {A : Set ℓ} (d₁ : Dist A) (ε : ℚ) (d₂ : Dist A) : Set (lsuc ℓ) where
field
elements : List A
pr₁ : (x : A) → x ∈ elements → ∃[ p ] Pr[ _≡ x [ d₁ ]]≡ p
pr₂ : (x : A) → x ∈ elements → ∃[ p ] Pr[ _≡ x [ d₂ ]]≡ p
elements-complete-d₁ : sum (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₁ x x∈xs)
}) (with-proof elements)) ≡ 1
elements-complete-d₂ : sum (map (λ{
⟨ x , x∈xs ⟩ → proj₁ (pr₂ x x∈xs)
}) (with-proof elements)) ≡ 1
ε-error : sum (map (λ{
⟨ x , x∈xs ⟩ → ℚ.∣ proj₁ (pr₁ x x∈xs) ℚ.- proj₁ (pr₂ x x∈xs) ∣
}) (with-proof elements)) ℚ≤ ε

_≃_ : {ℓ : Level} {A : Set ℓ} (d₁ d₂ : Dist A) → Set (lsuc ℓ)
d₁ ≃ d₂ = d₁ ≈[ 0 ]≈ d₂

postulate
≈-trans : {ℓ : Level} {A : Set ℓ} {d₁ d₂ d₃ : Dist A} {ε₁ ε₂ : ℚ} →
d₁ ≈[ ε₁ ]≈ d₂ → d₂ ≈[ ε₂ ]≈ d₃ → d₁ ≈[ ε₁ ℚ.+ ε₂ ]≈ d₃
≈-sym : {ℓ : Level} {A : Set ℓ} {d₁ d₂ : Dist A} {ε : ℚ} → d₁ ≈[ ε ]≈ d₂ →
d₂ ≈[ ε ]≈ d₁
≈-refl : {ℓ : Level} {A : Set ℓ} {d : Dist A} → d ≃ d

+ 46
- 22
Yggdrasil/Rational.agda View File

@@ -1,13 +1,13 @@
module Yggdrasil.Rational where

open import Data.Bool using (true; false; T)
open import Data.Integer using (ℤ; ∣_∣; _◃_; sign; +_) renaming (_+_ to _ℤ+_; _*_ to _ℤ*_)
open import Data.Nat as ℕ using (ℕ; suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Integer as ℤ using (ℤ; +_)
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Nat.GCD using (GCD; gcd)
open import Data.Nat.Divisibility using (_∣_; divides)
open import Data.Nat.Coprimality using (coprime?; gcd-coprime)
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Rational using (ℚ; _÷_)
open import Data.Rational using (ℚ) renaming (_÷_ to _÷†_)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Data.Sign using (Sign) renaming (+ to s+; - to s-)
@@ -17,32 +17,56 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open ℚ

¬0*¬0≡¬0 : {a b : ℕ} → ¬ (a ≡ 0) → ¬ (b ≡ 0) → ¬ (a ℕ* b ≡ 0)
¬0*¬0≡¬0 = ?
infixl 6 _+_ _-_
infixl 7 _*_ _÷_

¬0≡¬0*¬0 : {a b : ℕ} → ¬ (0 ≡ a ℕ* b) → ¬ (b ≡ 0)
¬0≡¬0*¬0 = ?
postulate
_÷_ : ℤ → (d : ℕ) → {d≢0 : False (d ℕ.≟ 0)} → ℚ

_+_ : ℚ → ℚ → ℚ
a + b with gcd (suc (denominator-1 a)) (suc (denominator-1 b))
... | ⟨ c , denom-gcd ⟩ with GCD.commonDivisor denom-gcd
... | ⟨ divides d₁ d₁*c≡da , divides d₂ d₂*c≡db ⟩ = let
d′ = d₁ ℕ* d₂ ℕ* c
n′ = ((numerator a) ℤ* (+ d₂)) ℤ+ ((numerator b) ℤ* (+ d₁))
d′≢0 = ?
in _÷_ n′ d′
{fromWitness (λ{ {i} ⟨ i∣n′ , i∣d′ ⟩ →
-- Coprime because: d₁ coprime d₂, d₁ coprime n₁, d₂ coprime n₂, n₁,
-- n₂ coprime c
?})}
{?}
∣_∣ : ℚ → ℚ
∣ q ∣ = _÷†_ (+ ℤ.∣ numerator q ∣) (suc (denominator-1 q)) {isCoprime q}

-_ : ℚ → ℚ
- q = _÷_ (ℤ.- numerator q) (suc (denominator-1 q))

_+_ : ℚ → ℚ → ℚ
a + b = let
n-a = numerator a
d-a = suc (denominator-1 a)
n-b = numerator b
d-b = suc (denominator-1 b)
n-c = n-a ℤ.* (+ d-b) ℤ.+ n-b ℤ.* (+ d-a)
d-c = d-a ℕ.* d-b
in n-c ÷ d-c

_*_ : ℚ → ℚ → ℚ
a * b = ?
a * b = let
n-a = numerator a
d-a = suc (denominator-1 a)
n-b = numerator b
d-b = suc (denominator-1 b)
n-c = n-a ℤ.* n-b
d-c = d-a ℕ.* d-b
in n-c ÷ d-c

_-_ : ℚ → ℚ → ℚ
a - b = ?
a - b = a + (- b)


--gcd (suc (denominator-1 a)) (suc (denominator-1 b))
--... | ⟨ c , denom-gcd ⟩ with GCD.commonDivisor denom-gcd
--... | ⟨ divides d₁ d₁*c≡da , divides d₂ d₂*c≡db ⟩ = let
-- d′ = d₁ ℕ* d₂ ℕ* c
-- n′ = ((numerator a) ℤ* (+ d₂)) ℤ+ ((numerator b) ℤ* (+ d₁))
-- d′≢0 = ?
-- in _÷_ n′ d′
-- {fromWitness (λ{ {i} ⟨ i∣n′ , i∣d′ ⟩ →
-- -- Coprime because: d₁ coprime d₂, d₁ coprime n₁, d₂ coprime n₂, n₁,
-- -- n₂ coprime c
-- ?})}
-- {?}



--data ℚ′ : Set where
-- _÷′_ : ℤ → (d : ℕ) → {d≢0 : False (d ℕ.≟ 0)} → ℚ′

Loading…
Cancel
Save