Add pseudo periodic clocks

link/clock.v

@@ -191,8 +191,42 @@ Qed.
 
 (** ** A few specific clocks *)
 
-(** Periodic clocks are a simple example of clock *)
-Program Definition periodic_uclock (period : {posnum R}) : uclock :=
-  Build_uclock (fun n => (n%:R * period%:num)%:nng) _ period _.
+(** Pseudo periodic clocks: clocks whose time between ticks is not
+    necessarily exactly the same but might be n an interval
+    [uclock_min_intertick, ppclock_max_intertick]. *)
+Record ppuclock := {
+  (** A pseudo periodic clock is a uclock. *)
+  ppuclock_uclock :> uclock;
+  (** with a maximal time between ticks *)
+  ppuclock_max_intertick : {posnum R};
+  _ : uclock_min_intertick ppuclock_uclock <= ppuclock_max_intertick;
+  _ : forall n, (uclock_tick_time ppuclock_uclock n.+1)%:nngnum
+           <= (uclock_tick_time ppuclock_uclock n)%:nngnum
+             + ppuclock_max_intertick%:num
+}.
+Arguments Build_ppuclock : clear implicits.
+
+Lemma ppuclock_ub (c : ppuclock) n :
+  (uclock_tick_time c n.+1)%:nngnum
+  <= (uclock_tick_time c n)%:nngnum + (ppuclock_max_intertick c)%:num.
+Proof. by case: c. Qed.
+
+(** Periodic clocks are a particular case of pseudo periodic clocks *)
+Program Definition periodic_uclock (period : {posnum R}) : ppuclock :=
+  Build_ppuclock
+    (Build_uclock (fun n => (n%:R * period%:num)%:nng) _ period _)
+    period _ _.
 Next Obligation. by apply/val_inj; rewrite /= mul0r. Qed.
 Next Obligation. by rewrite -addn1 natrD mulrDl mul1r. Qed.
+Next Obligation. by rewrite -addn1 natrD mulrDl mul1r. Qed.
+
+Lemma ppuclock_incr_ub (c : ppuclock) t d :
+  (c (t + d)%nat)%:nngnum - (c t)%:nngnum
+  <= d%:R * (ppuclock_max_intertick c)%:num.
+Proof.
+elim: d => [|d IHd]; first by rewrite addn0 subrr mul0r.
+rewrite addnS -[X in X <= _]addr0 -(subrr (c (t + d)%nat)%:nngnum).
+rewrite (addrC (c (t + d)%nat)%:nngnum) addrACA.
+rewrite -(addn1 d) natrD mulrDl mul1r addrC.
+by apply: ler_add; rewrite ?(addrC (- _)) ?IHd// ler_subl_addl ppuclock_ub.
+Qed.