Library ALEA.Markov

Require Export Arith.
Require Export Omega.
Set Implicit Arguments.

Markov rule

Decidable predicates on natural numbers

Definition dec (P:nat -> Prop) := forall n, {P n } + {~ P n }.

Record Dec : Type := mk_Dec {prop :> nat -> Prop; is_dec : dec prop}.

Definition of a successor function on predicates

PS P n = P (n+1)

Definition PS : Dec -> Dec.
Defined.

Order on predicates

P <= Q iff forall n, Q n -> exists m < n, P m

Definition ord (P Q:Dec) := forall n, Q n -> exists m, m < n /\ P m.

Lemma ord_eq_compat : forall (P1 P2 Q1 Q2:Dec),
(forall n, P1 n -> P2 n) -> (forall n, Q2 n -> Q1 n)
-> ord P1 Q1 -> ord P2 Q2.

Lemma ord_not_0 : forall P Q : Dec, ord P Q -> ~ Q 0.

Lemma ord_0 : forall P Q : Dec, P 0 -> ~ Q 0 -> ord P Q.

Chaining two predicates

PP P Q : first elt of P then Q : PP P Q 0 = P 0, PP P Q (n+1) = Q n

Definition PP : Dec -> Dec -> Dec.
Defined.

Lemma PP_PS : forall (P:Dec) n, PP P (PS P) n <-> P n.

Lemma PS_PP : forall (P Q:Dec) n, PS (PP P Q) n <-> Q n.

Lemma ord_PS : forall P : Dec, ~ P 0 -> ord (PS P) P.

Lemma ord_PP : forall (P Q: Dec), ~ P 0 -> ord Q (PP P Q).

Lemma ord_PS_PS : forall P Q : Dec, ord P Q -> ~ P 0 -> ord (PS P) (PS Q).

Accessibility of the order relation

Lemma Acc_ord_equiv : forall P Q : Dec,
(forall n, P n <-> Q n) -> Acc ord P -> Acc ord Q.

Lemma Acc_ord_0 : forall P : Dec, P 0 -> Acc ord P.
Hint Immediate Acc_ord_0.

Lemma Acc_ord_PP : forall (P Q:Dec), Acc ord Q -> Acc ord (PP P Q).

Lemma Acc_ord_PS : forall (P:Dec), Acc ord (PS P) -> Acc ord P.

Lemma Acc_ord : forall (P:Dec), (exists n,P n) -> Acc ord P.

Definition of the minimize function

Fixpoint min_acc (P:Dec) (a:Acc ord P) {struct a} : nat :=
   match is_dec P 0 with
      left _ => 0 | right H => S (min_acc (Acc_inv a (PS P) (ord_PS P H)))
   end.

Definition minimize (P:Dec) (e:exists n, P n) : nat := min_acc (Acc_ord P e).

Lemma minimize_P : forall (P:Dec) (e:exists n, P n), P (minimize P e).

Lemma minimize_min : forall (P:Dec) (e:exists n, P n) (m:nat), m < minimize P e -> ~ P m.

Lemma minimize_incr : forall (P Q:Dec)(e:exists n, P n)(f:exists n, Q n),
            (forall n, P n -> Q n) -> minimize Q f <= minimize P e.