Library probsa.probability.partition

(* ---------------------------------- Coq ----------------------------------- *)
From Coq Require Import Program.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Import notation.

(* ---------------------------------- Main ---------------------------------- *)

The following definition introduces the concept of an Ω_partition. Intuitively, a partition is just a set of events that (i) cover all positive-probability elements of Ω and (ii) are disjoint. In Coq, we use the set of indices to refer to different elements of a partition. Formally, a partition is a record consisting of the following components:

1. Ω - a countable sample space,

2. μ - a measure on Ω,

3. I - a countable set of indices,

4. p - a function that maps each index i to a subset of Ω,

5. a proof that the partition covers all ω : Ω with positive probability,

6. and a proof that for any two indices i and j, p i and p j are disjoint.

Record Ω_partition {Ω} {μ : measure Ω} :=
  {
    I : countType;
    p : I → pred Ω;
    COV : ∀ ω, μ ω > 0 → ∃ i , p i ω;
    DIS : ∀ ω, ∀ i j, p i ω → p j ω → i = j
  }.

Important notation: Given an Ω-partition S and an index i, we denote the i'th set of S as S◁{i} (recall that partition is a set of subsets).

Notation "S '◁{' i '}'" := (p S i)
(at level 30, format "S ◁{ i }") : probability_scope.

(* --------------------------- Extra Definitions ---------------------------- *)

One important type of partition is the partition into singletons { {ω} | ω ∈ Ω }, since, as we show later, such a partition trivially satisfies the job_cost_partition_independence defined in axiomatic_pWCET.

Section PartitionIntoSingletons.

Context {Ω} (μ : measure Ω).

A singleton-partition contains |Ω| sets, each containing only one element.

  Program Definition partition_into_singletons : @Ω_partition Ω μ :=
    {|
      I := Ω;
      p := fun ω _index ω ⇒ ω _index == ω
    |}.

End PartitionIntoSingletons.

Sometimes, it is useful to combine different partitions into one. Specifically, in the following section, we define an identity-partition (id-partition, for short) and the product of two partitions.

Section PartitionProduct.

Context {Ω} {μ : measure Ω}.

An id-partition is just one set that contains the entire Ω.

  Program Definition partition_id : @Ω_partition Ω μ :=
    {|
      I := [countType of unit ];
      p := fun _ _ ⇒ true
    |}.

Given two partitions with indices I1 and I2 and sets P1 i and P2 i respectively, a product partition is a partition with index I1 × I2 and sets defined by a predicate that checks if both P1 i1 and P2 i2 hold for a given tuple (i1, i2).

  Program Definition partition_prod (P1 P2 : @Ω_partition Ω μ) : @Ω_partition Ω μ :=
    match P1, P2 with
    | Build_Ω_partition I1 P1 CO1 DI1, Build_Ω_partition I2 P2 CO2 DI2 ⇒
        {|
          I := [countType of I1 × I2];
          p := fun '(i1 , i2 ) ω ⇒ (P1 i1 ω ) && (P2 i2 ω )
        |}
    end.

End PartitionProduct.

In this section, we define a way to extend a partition on a set Ω to a new set Ω × Ω'.

Section PartitionExtend.

Context {Ω} (μ : measure Ω).
Context {Ω'} (μ' : measure Ω').

A partition of Ω with index I and set p i can be extended to a set Ω × Ω' by using the same index set I and by redefining p i to ignore the element of Ω': fun i '(ω ,_) ⇒ p i ω). Such an extension is useful when one needs to transfer a partition of a set Ω to a set Ω × Ω'.

  Program Definition partition_ext (P : @Ω_partition Ω μ) :
    @Ω_partition [countType of (Ω × Ω')] (distrib_prod μ μ') :=
    match P with
    | Build_Ω_partition I p CO DI ⇒
        {|
          I := I;
          p := fun i '(ω, _) ⇒ p i ω
        |}
    end.

End PartitionExtend.