Library probsa.util.misc

From discprob.prob Require Export prob countable.
From prosa.util Require Import tactics.
From prosa.classic.util Require Import list.
From probsa.util Require Export boolp.
Require Export Reals Psatz.
From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype fintype bigop.
Local Open Scope nat_scope.

We prove that any monotone function f : nat → bool falls into one of the following cases: (1) f n is false for any n, (2) there exists t0 such that ∀ t, t > t0 ↔ f t, (3) or f n is always true. We note that this lemma uses the classical excluded middle axiom ∀ P : Prop, P ∨ ¬ P.

Lemma swithing_point_of_monotone_function :
  ∀ (f : nat → bool),
    (∀ t1 t2, t1 ≤ t2 → f t1 → f t2)%nat →
    (∀ t, ¬ f t ) ∨ (∃ t0 , ∀ t, t > t0 ↔ f t)%nat ∨ (∀ t, f t ).

Function that changes a type of a job s by mapping s : Job to s : Job \ {j}.

Definition to_fintype {Job : finType} (s j : Job) (NEQ: s != j) :
  Finite.sort (seq_sub_finType (T:=Job) (rem (T:=Job) j (enum Job))).

Lemma nth_seq_eq :
  ∀ {X : eqType} (d : X) (xs : seq X) (i1 i2 : nat),
    i1 < size xs →
    i2 < size xs →
    uniq xs →
    nth d xs i1 = nth d xs i2 →
    i1 = i2.

Lemma nth_mem_o :
  ∀ {X : eqType} (xs : seq X) (P : pred X) (x : X) (i : nat),
    nth None [seq Some x | x <- xs & P x] i = Some x →
    x \in xs ∧ P x.
Lemma perm_eq_allpairs_flatten :
  ∀ {X Y : eqType} (P : X → pred Y) (F : Y → X) (xs : seq X) (ys : seq Y),
    uniq xs →
    uniq ys →
    (∀ y, y \in ys → F y \in xs ) →
    (∀ y, y \in ys → P (F y) y ) →
    (∀ x1 x2 y, y \in ys → P x1 y → P x2 y → x1 = x2 ) →
    perm_eq [seq (F y , y ) | y <- ys] [seq (x , y ) | x <- xs, y <- filter (P x) ys].

Lemma seq_filter_singleton :
  ∀ {X : eqType} (P : pred X) (xs : seq X) (x : X),
    uniq xs →
    P x →
    (x \in xs ) →
    (∀ y, y \in xs → P y → x = y ) →
    [seq x <- xs | P x] = [:: x].