Library AbstractWalk
AbstractWalk.v: An example of probabilistic termination
Related to Vacid0 example of Maze constructionAbstraction of maze scheme
let rec iter u = if finished u then output u else let d = dData in if cond u d then iter u else iter (step d u)
Termination is taken using a measure on integer but could be generalized
to an arbitrary well-founded ordering
Variable size : Input -> nat.
Variable finished : Input -> bool.
Axiom finished_size : forall u, size u = O -> finished u = true.
Variable output : Input -> Result.
Variable cond : Input -> Data -> bool.
Variable step : Input -> Data -> Input.
When the process is not terminated, the probability to stay in the same state
is bounded by k<1
Variable k : U.
Hypothesis knot1 : k < 1.
Hypothesis d_true_bounded
: forall x, finished x = false -> mu dData (fun d => B2U (cond x d)) <= k.
Hypothesis knot1 : k < 1.
Hypothesis d_true_bounded
: forall x, finished x = false -> mu dData (fun d => B2U (cond x d)) <= k.
The random choice of data terminates
Hypothesis that the size decreases, when a step is taken
Hypothesis size_step : forall (u:Input) (x:Data),
finished u = false -> cond u x = false -> (size (step u x) < size u)%nat.
Lemma d_if_bound :
forall x, finished x = false -> forall a b, a <= b ->
k * a + [1-]k * b
<= mu dData (fun d => B2U (cond x d)) * a
+ mu dData (fun d => NB2U (cond x d)) * b.
Instance iter_mon :
monotonic
(fun (f:Input -> distr Result) (u:Input) =>
if (finished u) then Munit (output u)
else (Mlet dData
(fun d => if (cond u d) then (f u) else (f (step u d))))).
Save.
Lemma mu_if : forall A (b:bool) (dt de : distr A) (f:MF A),
mu (if b then dt else de) f = if b then (mu dt f) else (mu de f).
Definition Fiter : (Input -> distr Result) -m> (Input -> distr Result)
:= mon (fun (f:Input -> distr Result) (u:Input) =>
fif (finished u) (Munit (output u))
(Mlet dData
(fun d => fif (cond u d) (f u) (f (step u d))))).
Lemma Fiter_simpl : forall f u,
Fiter f u = fif (finished u) (Munit (output u))
(Mlet dData
(fun d => fif (cond u d) (f u) (f (step u d)))).
Lemma Fiter_cont : continuous Fiter.
Definition iter : Input -> distr Result := Mfix Fiter.
Lemma iter_eq : forall u:Input,
iter u == fif (finished u) (Munit (output u))
(Mlet dData (fun d => fif (cond u d) (iter u) (iter (step u d)))).
Hint Resolve iter_eq.
Building the invariant sequence
Fixpoint pw_ (x n : nat) : U :=
match n with O => 0
| (S n) => match x with
O => 1
| S y => k * pw_ x n + ([1-] k) * pw_ y n
end
end.
Lemma pw_decrS_x : forall n x, pw_ (S x) n <= pw_ x n.
Hint Resolve pw_decrS_x.
Lemma pw_decr_x : forall n x y, (x <= y)%nat -> pw_ y n <= pw_ x n.
Hint Resolve pw_decr_x.
Lemma pw_incr : forall x n, pw_ x n <= pw_ x (S n).
Hint Resolve pw_incr.
Definition pw : nat -> nat -m> U
:= fun x => fnatO_intro (pw_ x) (pw_incr x).
Lemma pw_pw_ : forall x n, pw x n = pw_ x n.
Lemma pw_simpl : forall x n, pw x n =
match n with O => 0
| (S n) => match x with
O => 1
| S y => k * pw x n + ([1-] k) * pw y n
end
end.
Lemma pwS_simpl : forall x n, pw (S x) (S n) = k * pw (S x) n + [1-]k * (pw x n).
Lemma lim_pw_one : forall x, lub (pw x) == 1.
Lemma iter_term : forall u, 1 <= mu (iter u) (fun r => 1).
End Walk.