Library ALEA.Markov
Definition dec (P:nat -> Prop) := forall n, {P n} + {~ P n}.
Record Dec : Type := mk_Dec {prop :> nat -> Prop; is_dec : dec prop}.
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.
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).
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.
(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.