Library Transitions
Require Export Prog.
Set Implicit Arguments.
Module PTS(Univ:Universe).
Module RP := (Rules Univ).
Section TRANSITIONS.
Variable A : Type.
Variable step : A -> distr A.
Require Export Nelist.
Definition add_step (start : distr (nelist A)) : M (nelist A) :=
fun f => mu start (fun l => (mu (step (hd l)) (fun x => (f (add x l))))).
Lemma add_step_stable_inv : forall (start : distr (nelist A)), stable_inv (add_step start).
red; unfold add_step; intros.
apply Ule_trans with
(mu start (finv (fun l : nelist A => mu (step (hd l)) (fun x : A => f (add x l))))).
apply (mu_monotonic start).
repeat red; intros.
apply (mu_stable_inv (step (hd x))) with (f:= fun x0 : A => f (add x0 x)).
apply (mu_stable_inv start).
Save.
Lemma add_step_stable_plus : forall (start : distr (nelist A)), stable_plus (add_step start).
red; unfold add_step; intros.
apply Ueq_trans with
(mu start (fplus (fun l => (mu (step (hd l)) (fun x : A => f (add x l))))
(fun l => (mu (step (hd l)) (fun x : A => g (add x l)))))).
apply (mu_stable_eq start).
repeat red; intros.
apply (mu_stable_plus (step (hd x)))
with (f:= fun x0 : A => f (add x0 x)) (g:= fun x0 : A => g (add x0 x)).
repeat red in H; repeat red; intros; unfold finv.
apply (H (add x0 x)).
apply (mu_stable_plus start).
repeat red in H; repeat red; intros; unfold finv.
apply Ule_trans with
(mu (step (hd x)) (finv (fun x0 : A => g (add x0 x)))).
apply (mu_monotonic (step (hd x))).
repeat red; intros; apply (H (add x0 x)).
apply (mu_stable_inv (step (hd x))).
Save.
Lemma add_step_stable_mult : forall (start : distr (nelist A)), stable_mult (add_step start).
red; unfold add_step; intros.
apply Ueq_trans with
(mu start (fmult k (fun l => (mu (step (hd l)) (fun x : A => f (add x l)))))).
apply (mu_stable_eq start).
repeat red; intros.
apply (mu_stable_mult (step (hd x)) k)
with (f:= fun x0 : A => f (add x0 x)).
apply (mu_stable_mult start).
Save.
Lemma add_step_monotonic : forall (start : distr (nelist A)), monotonic (add_step start).
red; unfold add_step; intros.
apply (mu_monotonic start).
repeat red; intros.
apply (mu_monotonic (step (hd x)))
with (f:= fun x0 : A => f (add x0 x)).
repeat red; intros.
apply (H (add x0 x)).
Save.
Definition Add_step : (distr (nelist A)) -> (distr (nelist A)).
intros start; exists (add_step start).
apply add_step_stable_inv.
apply add_step_stable_plus.
apply add_step_stable_mult.
apply add_step_monotonic.
Defined.
Definition of the measure
Fixpoint path (k:nat) (s : A) {struct k} : distr (nelist A) :=
match k with
O => Munit (singl s)
|(S p) => Add_step (path p s)
end.
The opposite view of composition starting from one step
Lemma path_unfold : forall k s f,
mu (path (S k) s) f == mu (step s) (fun x => mu (path k x) (fun l => f (app l (singl s)))).
induction k; intros.
simpl; unfold unit; auto.
apply Ueq_trans with (add_step (path (S k) s) f); trivial.
unfold add_step.
setoid_rewrite
(IHk s (fun l => mu (step (hd l)) (fun x : A => f (add x l)))).
apply (mu_stable_eq (step s)).
red; intros.
pose (g:=fun l => f (app l (singl s))).
apply Ueq_trans with
(mu (path k x)
(fun l : nelist A => mu (step (hd l)) (fun x0 : A => g (add x0 l)))); trivial.
apply (mu_stable_eq (path k x)); red; intros.
rewrite hd_app; auto.
Save.
End TRANSITIONS.
End PTS.
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (11 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (4 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |
This page has been generated by coqdoc