Library ComhBasics
This file was written by Colm Bhandal, PhD student, Foundations and Methods group,
School of Computer Science and Statistics, Trinity College, Dublin, Ireland.
Various constants relating to the comhordu model are assumed here. Also some basic notions
are defined here such as the notion of a network of entities.
Require Import ComhCoq.Extras.LibTactics.
Require Import Coq.Reals.Reals.
Require Export List.
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Notation "e _: n" := (In e n) (at level 60).
Require Export Logic.Decidable.
Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ListSet.
Definition toNonneg (r : posreal) : nonnegreal :=
let h := (Rlt_le 0 r (cond_pos r)) in
mknonnegreal r h.
A time value is a non negative real number.
Record Time := mkTime {time :> nonnegreal}.
Definition zeroTime : Time := mkTime zeroNonneg.
Ltac timeNonneg :=
match goal with
| [ |- 0 <= (nonneg (time ?t))] => unwrap2_apply2 t
| [ |- (nonneg (time zeroTime)) <= (nonneg (time ?t))] => simpl;unwrap2_apply2 t
end.
Definition zeroTime : Time := mkTime zeroNonneg.
Ltac timeNonneg :=
match goal with
| [ |- 0 <= (nonneg (time ?t))] => unwrap2_apply2 t
| [ |- (nonneg (time zeroTime)) <= (nonneg (time ?t))] => simpl;unwrap2_apply2 t
end.
A delay is a positive real number.
Record Delay := mkDelay {delay :> posreal}.
Ltac delPos :=
match goal with
| [ |- 0 < (pos (delay ?d))] => unwrap2_apply2 d
| [ |- (nonneg (time zeroTime)) < (pos (delay ?d))] => simpl;unwrap2_apply2 d
end.
Ltac delPos :=
match goal with
| [ |- 0 < (pos (delay ?d))] => unwrap2_apply2 d
| [ |- (nonneg (time zeroTime)) < (pos (delay ?d))] => simpl;unwrap2_apply2 d
end.
We can coerce a delay to be a time.
Coercion delToTime (d : Delay) : Time :=
match d with mkDelay d0 =>
mkTime d0 end.
match d with mkDelay d0 =>
mkTime d0 end.
A distance is a non negative real number
Record Distance := mkDistance {distance :> nonnegreal}.
Ltac foldDist l l0 H := replace (dist_euc (xCoord l) (yCoord l) (xCoord l0) (yCoord l0)) with
(nonneg (dist2d l l0)) in H;[ | simpl;ring].
Definition distFun p1 p2 := mkDistance (dist2d p1 p2).
Lemma timeEqNonneg : forall (t1 t2 : Time), (time t1) = (time t2) -> t1 = t2.
Lemma timeEqR : forall (t1 t2 : Time), (nonneg (time t1)) = (nonneg (time t2)) ->
t1 = t2.
Lemma delayEqPos : forall (d1 d2 : Delay), delay d1 = delay d2 -> d1 = d2.
Lemma delayEqR : forall (d1 d2 : Delay), pos d1 = pos d2 -> d1 = d2.
Open Scope nat_scope.
Lemma lt_notEq : forall (n m : nat),
n < m -> n <> m.
Ltac foldDist l l0 H := replace (dist_euc (xCoord l) (yCoord l) (xCoord l0) (yCoord l0)) with
(nonneg (dist2d l l0)) in H;[ | simpl;ring].
Definition distFun p1 p2 := mkDistance (dist2d p1 p2).
Lemma timeEqNonneg : forall (t1 t2 : Time), (time t1) = (time t2) -> t1 = t2.
Lemma timeEqR : forall (t1 t2 : Time), (nonneg (time t1)) = (nonneg (time t2)) ->
t1 = t2.
Lemma delayEqPos : forall (d1 d2 : Delay), delay d1 = delay d2 -> d1 = d2.
Lemma delayEqR : forall (d1 d2 : Delay), pos d1 = pos d2 -> d1 = d2.
Open Scope nat_scope.
Lemma lt_notEq : forall (n m : nat),
n < m -> n <> m.
Converts a decidable proposition to a boolean.
Definition decToBool {P : Prop} (p : {P} + {~P}) : bool :=
match p with
| left _ => true
| right _ => false
end.
match p with
| left _ => true
| right _ => false
end.
Converts a decidable relation to a boolean.
Definition decToOption {P : Prop} (p : {P} + {~P}) : option P :=
match p with
| left P => Some P
| right _ => None
end.
Lemma lt_plus_r (m n : nat) :
0 < n -> m < m + n.
Lemma lt_plus_l (m n : nat) :
0 < n -> m < n + m.
Lemma le_plus_r (m n : nat) :
m <= m + n.
Lemma le_plus_l (m n : nat) :
m <= n + m.
Open Scope R_scope.
match p with
| left P => Some P
| right _ => None
end.
Lemma lt_plus_r (m n : nat) :
0 < n -> m < m + n.
Lemma lt_plus_l (m n : nat) :
0 < n -> m < n + m.
Lemma le_plus_r (m n : nat) :
m <= m + n.
Lemma le_plus_l (m n : nat) :
m <= n + m.
Open Scope R_scope.
inAtList a i l says that a is at position i in the list l.
The first position is position 0.
Inductive inAtList {A : Type} (a : A) : nat -> list A -> Prop :=
| inatlFst (l : list A) :
inAtList a 0 (a :: l)
| inatlCons (i : nat) (a' : A) (l : list A) :
inAtList a i l -> inAtList a (S i) (a' :: l).
Notation "a -@ i -: l" := (inAtList a i l) (at level 50).
| inatlFst (l : list A) :
inAtList a 0 (a :: l)
| inatlCons (i : nat) (a' : A) (l : list A) :
inAtList a i l -> inAtList a (S i) (a' :: l).
Notation "a -@ i -: l" := (inAtList a i l) (at level 50).
If an element is in a list according to the definition of inAtList,
then it is in the list according to In.
Theorem inAtList_inList (A : Type) (a : A) (l : list A) (i : nat) :
a -@ i -: l -> a _: l.
a -@ i -: l -> a _: l.
If a is at i in l and so is a', then a = a'.
Theorem inAtListUnique (A : Type) (a a' : A) (i : nat) (l : list A) :
a -@ i -: l -> a' -@ i -: l -> a = a'.
a -@ i -: l -> a' -@ i -: l -> a = a'.
There either exists an element at position i or there doesn't.
Theorem decInAtList (A : Type) (i : nat) (l : list A) :
decidable (exists a, a -@ i -: l).
Lemma eqDecTime : eqDec Time.
decidable (exists a, a -@ i -: l).
Lemma eqDecTime : eqDec Time.
Equality is decidable on Delays.
Lemma eqDecDelay : eqDec Delay.
Lemma eqDecDistance : eqDec Distance.
Definition subtractTime (t1 t2 : Time) : option Time :=
let r1 := nonneg t1 in let r2 := nonneg t2 in
match total_order_T r1 r2 with
| inleft _ => None
| inright H => Some (mkTime (mknonnegreal (r1 - r2)
(Rlt_le 0 (r1 - r2) (RltMinusBothSides r1 r2 H))))
end.
Definition addTime (t1 t2 : Time) : Time :=
let r1 := nonneg t1 in let r2 := nonneg t2 in
mkTime (mknonnegreal (r1 + r2) (Rle_zero_plus r1 r2 (cond_nonneg t1) (cond_nonneg t2))).
Lemma eqDecDistance : eqDec Distance.
Definition subtractTime (t1 t2 : Time) : option Time :=
let r1 := nonneg t1 in let r2 := nonneg t2 in
match total_order_T r1 r2 with
| inleft _ => None
| inright H => Some (mkTime (mknonnegreal (r1 - r2)
(Rlt_le 0 (r1 - r2) (RltMinusBothSides r1 r2 H))))
end.
Definition addTime (t1 t2 : Time) : Time :=
let r1 := nonneg t1 in let r2 := nonneg t2 in
mkTime (mknonnegreal (r1 + r2) (Rle_zero_plus r1 r2 (cond_nonneg t1) (cond_nonneg t2))).
Add two delays together to get a third delay.
Definition addDelay (d1 d2 : Delay) : Delay :=
let r1 := pos d1 in let r2 := pos d2 in
mkDelay (mkposreal (r1 + r2) (Rlt_zero_plus r1 r2 (cond_pos d1) (cond_pos d2))).
let r1 := pos d1 in let r2 := pos d2 in
mkDelay (mkposreal (r1 + r2) (Rlt_zero_plus r1 r2 (cond_pos d1) (cond_pos d2))).
Add a delay to a time to get a delay.
Definition addDelayTime (t : Time) (d : Delay) : Delay :=
let r1 := nonneg t in let r2 := pos d in
mkDelay (mkposreal (r1 + r2) (Rplus_le_lt_0_compat r1 r2 (cond_nonneg t) (cond_pos d))).
Notation "t +dt+ d" := (addDelayTime t d) (at level 45).
Notation "d +d+ d'" := (addDelay d d') (at level 45).
Lemma addDelayComm : forall (d d' : Delay), d +d+ d' = d' +d+ d.
Lemma timeDelAddSwitch : forall (d d' : Delay),
d +dt+ d' = d +d+ d'.
Lemma delTimeAddAssoc : forall (t : Time) (d d' : Delay),
t +dt+ d +dt+ d' = t +dt+ (d +dt+ d').
Lemma delTimeAddAssoc2 : forall (t : Time) (d d' : Delay),
(t +dt+ d) +d+ d' = t +dt+ (d +d+ d').
Lemma timeDelAddZeroL : forall (d : Delay),
zeroTime +dt+ d = d.
let r1 := nonneg t in let r2 := pos d in
mkDelay (mkposreal (r1 + r2) (Rplus_le_lt_0_compat r1 r2 (cond_nonneg t) (cond_pos d))).
Notation "t +dt+ d" := (addDelayTime t d) (at level 45).
Notation "d +d+ d'" := (addDelay d d') (at level 45).
Lemma addDelayComm : forall (d d' : Delay), d +d+ d' = d' +d+ d.
Lemma timeDelAddSwitch : forall (d d' : Delay),
d +dt+ d' = d +d+ d'.
Lemma delTimeAddAssoc : forall (t : Time) (d d' : Delay),
t +dt+ d +dt+ d' = t +dt+ (d +dt+ d').
Lemma delTimeAddAssoc2 : forall (t : Time) (d d' : Delay),
(t +dt+ d) +d+ d' = t +dt+ (d +d+ d').
Lemma timeDelAddZeroL : forall (d : Delay),
zeroTime +dt+ d = d.
If a delay d is less than or equal a time t,
then there is some time t' such that t = t' + d.
Lemma delLeTimeSum : forall (t : Time) (d : Delay),
d <= t -> exists t', t = t' +dt+ d.
d <= t -> exists t', t = t' +dt+ d.
Subtract d2 from d1. Requires a proof that d2 is indeed less than d1 so
that the result is a delay.
Definition minusDelay (r1 r2 : R) (p : r2 < r1) : Delay :=
mkDelay (mkposreal (r1 - r2) (Rgt_minus r1 r2 (Rlt_gt r2 r1 p))).
mkDelay (mkposreal (r1 - r2) (Rgt_minus r1 r2 (Rlt_gt r2 r1 p))).
Subtracting and then adding the same delay gives the same result.
Lemma minusAddDelay : forall (d1 d2 : Delay) (p : d2 < d1),
(minusDelay d1 d2 p) +d+ d2 = d1.
(minusDelay d1 d2 p) +d+ d2 = d1.
Adding a time that has been subtracted gives back the original result.
Lemma minusDelayAddTime : forall (d : Delay) (t : Time) (p : t < d),
d = t +dt+ (minusDelay d t p).
Lemma addDelayLtR : forall (d1 d2 : Delay),
d2 < d1 +d+ d2.
d = t +dt+ (minusDelay d t p).
Lemma addDelayLtR : forall (d1 d2 : Delay),
d2 < d1 +d+ d2.
Adding and then subtracting the same quantity leaves the original delay.
Lemma addMinusDelay : forall (d1 d2 : Delay),
exists p, minusDelay (d1 +d+ d2) d2 p = d1.
exists p, minusDelay (d1 +d+ d2) d2 p = d1.
Communtativity of times in a sum of three terms.
Lemma timeDelAddComm : forall (t1 t2 : Time) (d : Delay),
t1 +dt+ (t2 +dt+ d) = t2 +dt+ (t1 +dt+ d).
Definition minusTime (r1 r2 : R) (p : r2 <= r1) : Time :=
mkTime (mknonnegreal (r1 - r2) (Rge_le (r1 - r2) 0
(Rge_minus r1 r2 (Rle_ge r2 r1 p)))).
t1 +dt+ (t2 +dt+ d) = t2 +dt+ (t1 +dt+ d).
Definition minusTime (r1 r2 : R) (p : r2 <= r1) : Time :=
mkTime (mknonnegreal (r1 - r2) (Rge_le (r1 - r2) 0
(Rge_minus r1 r2 (Rle_ge r2 r1 p)))).
To show that d = d +d+ d' according to the addDel function, it suffices to show that
d = d + d' i.e. that the real parts and real number addition equates.
Lemma addRaddDel : forall (d d' d'' : Delay),
pos d = d' + d'' -> d = d' +d+ d''.
pos d = d' + d'' -> d = d' +d+ d''.
Every delay has two delays that add up to make it.
Theorem addDelayExists : forall (d : Delay),
exists d1 d2, d = d1 +d+ d2.
Lemma RMax_time (t1 t2 : Time) : 0 <= Rmax t1 t2.
Definition timeMax (t1 t2 : Time) : Time :=
mkTime (mknonnegreal (Rmax t1 t2) (RMax_time t1 t2)).
Lemma timeMax_RMax : forall (t1 t2 : Time), nonneg (timeMax t1 t2) = Rmax t1 t2.
Notation "t1 +t+ t2" := (addTime t1 t2) (at level 50).
exists d1 d2, d = d1 +d+ d2.
Lemma RMax_time (t1 t2 : Time) : 0 <= Rmax t1 t2.
Definition timeMax (t1 t2 : Time) : Time :=
mkTime (mknonnegreal (Rmax t1 t2) (RMax_time t1 t2)).
Lemma timeMax_RMax : forall (t1 t2 : Time), nonneg (timeMax t1 t2) = Rmax t1 t2.
Notation "t1 +t+ t2" := (addTime t1 t2) (at level 50).
Given time t, splits goal into two subgoals based on whether 0 = t or 0 < t
Ltac timezerolteq t U := let H := fresh in assert (0 <= t) as H;[timeNonneg| ];
apply Rle_lt_or_eq_dec in H; let U1 := fresh U in elim_intro H U1 U1.
Ltac mkdel t Q d' := remember (mkDelay (mkposreal t Q)) as d'.
apply Rle_lt_or_eq_dec in H; let U1 := fresh U in elim_intro H U1 U1.
Ltac mkdel t Q d' := remember (mkDelay (mkposreal t Q)) as d'.
The time it takes for an entity to be notified of a message delivery area.
Axiom adaptNotif : Time.
The time between initiating the sending of a message and its actual delivery.
Axiom msgLatency : Time.
Axiom speedMax : nonnegreal.
Axiom speedMax : nonnegreal.
The set of all modes.
Axiom Mode : Type.
A subset of the modes are fail safe.
Axiom failSafe : Mode -> Prop.
A mode is either fail safe or it isn't.
Axiom fsDecMode : forall (m : Mode), decidable (failSafe m).
Equality on modes is decidable.
Axiom eqDecMode : eqDec Mode.
The mode transition relation, which says whether one mode can transition
to another or not.
Axiom modeTransRel : Mode -> Mode -> Prop.
Notation "m1 -mtr-> m2" := (modeTransRel m1 m2) (at level 39).
Notation "m1 -mtr-> m2" := (modeTransRel m1 m2) (at level 39).
The mode transition relation is assumed to be decidable.
Axiom modeTransRelDec : forall (m1 m2 : Mode),
{m1 -mtr-> m2} + {~m1 -mtr-> m2}.
{m1 -mtr-> m2} + {~m1 -mtr-> m2}.
Mode transition relation as a boolean function.
Definition modeTransRelBool (m1 m2 : Mode) : bool :=
decToBool (modeTransRelDec m1 m2).
decToBool (modeTransRelDec m1 m2).
Mode transition relation as an option type
Definition modeTransRelOpt (m1 m2 : Mode) : option (m1 -mtr-> m2) :=
decToOption (modeTransRelDec m1 m2).
decToOption (modeTransRelDec m1 m2).
modeTransTime m1 m2 gives the time it takes to transition from
m1 to m2. Note that this function takes two modes and a proof that one
transitions to the other and then returns the transition time.
Axiom modeTransTime : forall (m1 m2 : Mode),
m1 -mtr-> m2 -> Time.
m1 -mtr-> m2 -> Time.
We assume that every mode transitions to some fail safe mode,
and this function simply arbitrarily picks one such fail safe mode.
Axiom failSafeSucc : Mode -> Mode.
This is the assumption that failSafeSucc m is indeed fail safe for all m.
Axiom failSafeSuccFS : forall (m : Mode), failSafe (failSafeSucc m).
Axiom failSafeSucc_successor : forall m, m -mtr-> failSafeSucc m.
Axiom failSafeSucc_successor : forall m, m -mtr-> failSafeSucc m.
trans m is the worst case time it takes for an entity in a mode m
to reach a failsafe mode.
Axiom trans : Mode -> Time.
An upper bound on trans m over all m: transMax is an upper bound on
the time it takes any entity to reach a failsafe mode.
Axiom transMax : Time.
Axiom waitSurplus : Delay.
Axiom waitSurplus : Delay.
The wait time between two modes m1 and m2 is the maximum between two different
values. The first is the mode transition time, denoting the physical time it takes
to transition from one mode to another. The second value ensures that the wait time
is to sufficient to ensure surrounding entities are warned. As such, it incorporates
the term msgLatency to allow the initial message to be delivered, transMax for the
receiving entities to react, adaptNotif for the sender to be notified of the coverage,
and finally some positive waitSurplus to ensure that the message delivery, reaction and
notification have definitely happened in the past- without the surplus it might be possible
for these events to be about to happen this instant but they might not have happened yet.
Definition waitTime (m1 m2 : Mode) (p : m1 -mtr-> m2) : Time :=
timeMax (modeTransTime m1 m2 p)
(msgLatency +t+ (timeMax adaptNotif transMax) +t+ waitSurplus).
Open Scope R_scope.
timeMax (modeTransTime m1 m2 p)
(msgLatency +t+ (timeMax adaptNotif transMax) +t+ waitSurplus).
Open Scope R_scope.
transMax is an upper bound on trans m for all m.
Axiom transMaxBound : forall m : Mode,
trans m <= transMax.
trans m <= transMax.
The minimum distance of compatibiltiy function is assumed to exist.
It tells us the minimum distance by which two modes must be separated in
order for them to be compatible. If two entities in these modes are
separated by a distance greater than or equal to this distance,
then they are compatible.
Axiom minDistComp : Mode -> Mode -> Distance.
The minimum distance of compatibility function is symmetric.
Axiom minDistCompSymmetric : forall (m1 m2 : Mode),
minDistComp m1 m2 = minDistComp m2 m1.
minDistComp m1 m2 = minDistComp m2 m1.
For a given mode m, maxMinDistComp m is an upper bound on the set
minDistComp m m' taken over all other modes m'. We do not enforce that this
is the least such upper bound, though this would be the sensible interpretation.
Axiom maxMinDistComp : Mode -> Distance.
The maxMinDistComp is an upper bound on the minDistComp for all other modes
Axiom maxMinDistCompBound : forall m m' : Mode,
minDistComp m m' <= maxMinDistComp m.
minDistComp m m' <= maxMinDistComp m.
The minimum distance of compatibility function returns 0 if either
of its arguments are fail safe. Note we only choose the left argument here,
but the choice is irrelevant since the function is symmetric.
Axiom minDistCompFS : forall (m1 m2 : Mode),
failSafe m1 -> minDistComp m1 m2 = (mkDistance zeroNonneg).
failSafe m1 -> minDistComp m1 m2 = (mkDistance zeroNonneg).
period m is the time between successive broadcasts from an entity in mode m.
Axiom period : Mode -> Time.
Axiom msgLatency_positive : 0 < msgLatency.
Axiom period_positive : forall m : Mode, 0 < period m.
Axiom msgLatency_positive : 0 < msgLatency.
Axiom period_positive : forall m : Mode, 0 < period m.
To rule out a trivial system, we assume the maximum speed is above 0.
Axiom speedMax_pos: 0 < speedMax.
Lemma speedMax_nonneg : 0 <= speedMax.
Axiom adaptNotif_positive : 0 < adaptNotif.
Axiom modeTransTime_bound : forall (m m' : Mode) (p : m -mtr-> m'),
modeTransTime m m' p <= trans m.
Ltac timering := apply timeEqR; simpl; ring.
Lemma speedMax_nonneg : 0 <= speedMax.
Axiom adaptNotif_positive : 0 < adaptNotif.
Axiom modeTransTime_bound : forall (m m' : Mode) (p : m -mtr-> m'),
modeTransTime m m' p <= trans m.
Ltac timering := apply timeEqR; simpl; ring.
The coverage r is sufficient for an entity broadcasting in mode m.
Definition sufficient (m : Mode) (r : Distance) : Prop :=
maxMinDistComp m +
2 * speedMax * (Rmax adaptNotif transMax + period m + trans m) <= r.
maxMinDistComp m +
2 * speedMax * (Rmax adaptNotif transMax + period m + trans m) <= r.
The sufficient predicate is decidable.
Lemma suffDec : forall (m : Mode) (r : Distance),
{sufficient m r} + {~sufficient m r}.
{sufficient m r} + {~sufficient m r}.
A version of the sufficient Prop that gives a bool as a result.
Definition suffBool (m : Mode) (r : Distance) : bool :=
if suffDec m r then true else false.
if suffDec m r then true else false.
The possibly incompatible distance for modes m and m' is the distance
beneath which an entity in mode m must consider mode m' messages from other entities
as potential threats.
Definition possIncDist (m m' : Mode) : R :=
minDistComp m m' + 2 * speedMax * (Rmax adaptNotif transMax + period m' + trans m').
minDistComp m m' + 2 * speedMax * (Rmax adaptNotif transMax + period m' + trans m').
possiblyIncompatible m m' r means that if e and e' in m and m'
respectively are separated by r, then e' should begin to transition to a
fail safe mode if it has not already done so.
Definition possiblyIncompatible (m m' : Mode) (r : R) :=
r < possIncDist m m'.
Lemma possIncDec : forall (m m' : Mode) (r : Distance),
{possiblyIncompatible m m' r} + {~possiblyIncompatible m m' r}.
r < possIncDist m m'.
Lemma possIncDec : forall (m m' : Mode) (r : Distance),
{possiblyIncompatible m m' r} + {~possiblyIncompatible m m' r}.
A version of the possiblyIncompatible Prop that gives a bool as a result.
Definition possIncBool (m m' : Mode) (r : Distance) : bool :=
if possIncDec m m' r then true else false.
if possIncDec m m' r then true else false.
If m m' r are possibly incompatible, r' is a sufficient coverage for m, then
r <= r'.
Theorem possIncSuff : forall (m m' : Mode) (r r' : Distance),
possiblyIncompatible m m' r -> sufficient m' r' -> r < r'.
Open Scope nat_scope.
Open Scope nat_scope.
Theorem rightmost : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
p j -> j <= k ->
exists j', j <= j' <= k /\ p j' /\
forall x : nat, j' < x <= k -> ~ p x.
Open Scope R_scope.
possiblyIncompatible m m' r -> sufficient m' r' -> r < r'.
Open Scope nat_scope.
Open Scope nat_scope.
Theorem rightmost : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
p j -> j <= k ->
exists j', j <= j' <= k /\ p j' /\
forall x : nat, j' < x <= k -> ~ p x.
Open Scope R_scope.
This is the interval in the past during which we show that any entity
in a non fail safe mode m must have sent a message containing mode m.
Definition preSentInterval (m : Mode) : Interval :=
let lower := msgLatency + Rmax adaptNotif transMax in
let upper := lower + period m + trans m in
(\lower, upper\].
let lower := msgLatency + Rmax adaptNotif transMax in
let upper := lower + period m + trans m in
(\lower, upper\].
The interval of time in the past during which we can show a
sufficient pre-broadcast takes place, parametrised on the mode m.
Definition preDeliveredInterval (m : Mode) : Interval :=
let lower := Rmax adaptNotif transMax in
let upper := lower + period m + trans m in
(\lower, upper\].
let lower := Rmax adaptNotif transMax in
let upper := lower + period m + trans m in
(\lower, upper\].
The upper bound of the pre bc suff interval is positive
Lemma preBcSuffUpperPos : forall m : Mode,
0 <= upper (preDeliveredInterval m).
Lemma plusIntervalZero : forall (i : Interval),
i [+] zeroTime = i.
Open Scope nat_scope.
Theorem rightmostNeg : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
~p j -> j <= k ->
exists j', j <= j' <= k /\ ~p j' /\
forall x : nat, j' < x <= k -> p x.
Inductive leAlt : nat -> nat-> Prop :=
| leaRefl : forall (n : nat), leAlt n n
| leaSucc : forall (m n : nat), leAlt (S m) n -> leAlt m n.
Lemma leAlt_S : forall (m n : nat), leAlt m n -> leAlt m (S n).
Lemma leAltLe : forall (m n : nat), m <= n <-> leAlt m n.
Theorem leftmost : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
p k -> j <= k ->
exists j', j <= j' <= k /\ p j' /\
forall x : nat, j <= x < j' -> ~ p x.
Theorem leftmostNeg : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
~p k -> j <= k ->
exists j', j <= j' <= k /\ ~p j' /\
forall x : nat, j <= x < j' -> p x.
Theorem rightmostCont : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
p j -> j <= k ->
exists j' , j <= j' <= k /\
forall m : nat, j <= m <= j' -> p m /\
(~p (S j') \/ j' = k).
Open Scope R_scope.
Lemma timeZero : forall (u : Time),
(nonneg (time u)) = 0 -> u = zeroTime.
Lemma speedMax_double_nonneg : 0 <= 2*speedMax.
Lemma inPreBcSuffPos : forall (m : Mode) (u : Time),
u [:] (preDeliveredInterval m) -> 0 < u.
Lemma inclNotEx {A : Type} (l1 l2 : list A) : (forall x y : A, {x = y} + {x <> y}) ->
~ incl l1 l2 -> exists a, a _: l1 /\ ~a _: l2.
Lemma incl_emp {A : Type} (l : list A) : incl [] l.
Lemma incl_emp_eq {A : Type} (l : list A) : incl l [] -> l = [].
Lemma diff_emp {A : Type} (l : list A)
(p : forall x y : A, {x = y} + {x <> y}) : set_diff p l [] = [] -> l = [].
Lemma incl_diff_equiv {A : Type} (l1 l2 : list A)
(p : forall x y : A, {x = y} + {x <> y}) : incl l1 l2 <-> set_diff p l1 l2 = [].
Lemma decIncl {A : Type} (l1 l2 : list A) :
(forall x y : A, {x = y} + {x <> y}) -> decidable (incl l1 l2).
Lemma inter_incl {A : Type} (x y z : set A)
(p : forall a b : A, {a = b} + {a <> b}) :
incl x y -> incl (set_inter p x z) (set_inter p y z).
Lemma set_inter_nil_cons {X : Type}
{p : forall x y : X, {x = y} + {x <> y}} (l1 l2 : list X) (x : X) :
set_inter p (x :: l1) l2 = [] -> set_inter p l1 l2 = [].
Lemma set_inter_nil_in1 {X : Type}
{p : forall x y : X, {x = y} + {x <> y}} (l1 l2 : list X) (x : X) :
set_inter p l1 l2 = [] -> x _: l1 -> ~x _: l2.
Lemma set_inter_nil_in2 {X : Type}
{p : forall x y : X, {x = y} + {x <> y}} (l1 l2 : list X) (x : X) :
set_inter p l1 l2 = [] -> x _: l2 -> ~x _: l1.
Lemma sufficient_suffBool m r : sufficient m r ->
suffBool m r = true.
Lemma possInc_possIncBool m m' r :
possiblyIncompatible m m' (distance r) ->
possIncBool m m' r = true.
Lemma possIncBool_possInc m m' r :
possIncBool m m' r = true ->
possiblyIncompatible m m' (distance r).
Lemma possIncDist_positive m1 m2 : 0 < possIncDist m1 m2.
0 <= upper (preDeliveredInterval m).
Lemma plusIntervalZero : forall (i : Interval),
i [+] zeroTime = i.
Open Scope nat_scope.
Theorem rightmostNeg : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
~p j -> j <= k ->
exists j', j <= j' <= k /\ ~p j' /\
forall x : nat, j' < x <= k -> p x.
Inductive leAlt : nat -> nat-> Prop :=
| leaRefl : forall (n : nat), leAlt n n
| leaSucc : forall (m n : nat), leAlt (S m) n -> leAlt m n.
Lemma leAlt_S : forall (m n : nat), leAlt m n -> leAlt m (S n).
Lemma leAltLe : forall (m n : nat), m <= n <-> leAlt m n.
Theorem leftmost : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
p k -> j <= k ->
exists j', j <= j' <= k /\ p j' /\
forall x : nat, j <= x < j' -> ~ p x.
Theorem leftmostNeg : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
~p k -> j <= k ->
exists j', j <= j' <= k /\ ~p j' /\
forall x : nat, j <= x < j' -> p x.
Theorem rightmostCont : forall (j k : nat) (p : nat -> Prop)
(K : forall i : nat, decidable (p i)),
p j -> j <= k ->
exists j' , j <= j' <= k /\
forall m : nat, j <= m <= j' -> p m /\
(~p (S j') \/ j' = k).
Open Scope R_scope.
Lemma timeZero : forall (u : Time),
(nonneg (time u)) = 0 -> u = zeroTime.
Lemma speedMax_double_nonneg : 0 <= 2*speedMax.
Lemma inPreBcSuffPos : forall (m : Mode) (u : Time),
u [:] (preDeliveredInterval m) -> 0 < u.
Lemma inclNotEx {A : Type} (l1 l2 : list A) : (forall x y : A, {x = y} + {x <> y}) ->
~ incl l1 l2 -> exists a, a _: l1 /\ ~a _: l2.
Lemma incl_emp {A : Type} (l : list A) : incl [] l.
Lemma incl_emp_eq {A : Type} (l : list A) : incl l [] -> l = [].
Lemma diff_emp {A : Type} (l : list A)
(p : forall x y : A, {x = y} + {x <> y}) : set_diff p l [] = [] -> l = [].
Lemma incl_diff_equiv {A : Type} (l1 l2 : list A)
(p : forall x y : A, {x = y} + {x <> y}) : incl l1 l2 <-> set_diff p l1 l2 = [].
Lemma decIncl {A : Type} (l1 l2 : list A) :
(forall x y : A, {x = y} + {x <> y}) -> decidable (incl l1 l2).
Lemma inter_incl {A : Type} (x y z : set A)
(p : forall a b : A, {a = b} + {a <> b}) :
incl x y -> incl (set_inter p x z) (set_inter p y z).
Lemma set_inter_nil_cons {X : Type}
{p : forall x y : X, {x = y} + {x <> y}} (l1 l2 : list X) (x : X) :
set_inter p (x :: l1) l2 = [] -> set_inter p l1 l2 = [].
Lemma set_inter_nil_in1 {X : Type}
{p : forall x y : X, {x = y} + {x <> y}} (l1 l2 : list X) (x : X) :
set_inter p l1 l2 = [] -> x _: l1 -> ~x _: l2.
Lemma set_inter_nil_in2 {X : Type}
{p : forall x y : X, {x = y} + {x <> y}} (l1 l2 : list X) (x : X) :
set_inter p l1 l2 = [] -> x _: l2 -> ~x _: l1.
Lemma sufficient_suffBool m r : sufficient m r ->
suffBool m r = true.
Lemma possInc_possIncBool m m' r :
possiblyIncompatible m m' (distance r) ->
possIncBool m m' r = true.
Lemma possIncBool_possInc m m' r :
possIncBool m m' r = true ->
possiblyIncompatible m m' (distance r).
Lemma possIncDist_positive m1 m2 : 0 < possIncDist m1 m2.
This page has been generated by coqdoc