Commit 14468fc0 authored by Sophie Quinton's avatar Sophie Quinton

added a first version of the library for event streams

parent e61a702b
Pipeline #2139 skipped
##thesis_lina_coq
This repository contains the main Coq proof spec
& proof development of the conversions event model functions.
## hierarchy
1. conversion_function.v:
contains the conversions of the event model definitions
and its conversion properties.
2. dmin.v
contains the definition of the construction of d_min
and its properties.
(Written by Pascal Fradet)
3. event_model.v
contains the definition of the event model.
4. eval_event_model.v
contains the evaluation of the event model.
5. next.v
contains the properties and proof of existence
of next occurrences in a trace.
(Written by Pascal Fradet)
6. trace_properties.v
contains trace properties.
7. types.v
contains the the types definition used
to define the event model.
8. tactics.v
contains useful tactics.
9. util.v
contains some useful added lemmas to make our proofs.
This diff is collapsed.
This diff is collapsed.
Require Import Arith NPeano List Omega dmin tactics types next event_model.
(* ########################################################### *)
(** * Evaluations *)
(* ########################################################### *)
Definition sigma1 (t : instant) : nb_occurrences :=
match t with
| 0 => 0
| 1 => 0
| 2 => 1
| 3 => 2
| 4 => 1
| 5 => 1
| 9 => 3
| n => 4
end.
Check delta.
(*
Example test_delta : @delta sigma1 AE 1 3 = 1.
unfold delta.
simpl.
unfold instant_of.
assert (H : instant_after sigma1 AE 3 0 = 3).
-
unfold instant_after.
elim sigma1.
induction sigma1.
unfold instant_after_func.
simpl.
induction.
Eval compute in (@next sigma1 AE 1).
*)
\ No newline at end of file
Require Import Arith NPeano List Omega dmin tactics next types.
Require Import Coq.Program.Wf.
(* ####################################################### *)
(** * The event load function and its properties *)
(* ####################################################### *)
(** The event load function *)
Fixpoint eta (t : instant) (dt : duration) : nb_occurrences :=
match dt with
| 0 => 0
| S dt' => sigma t + eta (S t) dt'
end.
Definition subadditive (f : nat -> nat) : Prop :=
forall (x y : nat), f (x + y) <= f x + f y.
Definition max_eta_trace (f : duration -> nb_occurrences) : Prop :=
forall t dt, eta t dt <= f dt.
(** The event load maximum function *)
Definition eta_max (f : duration -> nb_occurrences) : Prop :=
max_eta_trace f /\ subadditive f.
(* ########################################################### *)
(** * The event distance function and its properties *)
(* ########################################################### *)
(* compute the instant after an number of occurrence *)
Program Fixpoint instant_after (remaining : nb_occurrences) (curr : instant)
{measure remaining} : instant :=
match remaining with
| 0 => curr
| _ => instant_after (remaining - sigma (next curr)) (next (S curr))
end.
Obligation 1.
set (N := next_prop curr).
destruct N as [? [? ?]].
omega.
Defined.
(* return the instant of an id of occurrence *)
Definition instant_of (n : id_occurrence) : instant := instant_after n 0.
(** The event distance function *)
Definition delta (n : id_occurrence) (k : nb_occurrences) : duration :=
instant_of (n + k - 1) - instant_of n.
Definition superadditive (f : nat -> nat) : Prop :=
forall (x y : nat), f (x + y) >= f x + f y.
Definition pseudo_superadditive (f : nat -> nat) : Prop :=
forall (x y : nat), f (x + (y + 1)) >= f (x + 1) + f (y + 1).
Definition min_delta_trace (f : nb_occurrences -> duration) : Prop :=
forall n k, delta n k >= f k.
(** The event distance minimum function *)
Definition delta_min (f : nb_occurrences -> duration) : Prop :=
min_delta_trace f /\ pseudo_superadditive f.
Require Import List Coq.Logic.ConstructiveEpsilon Coq.Logic.Decidable Omega.
Require Import dmin.
Require Import tactics types.
Require Import Arith NPeano List Omega.
(* There is no event at instants t,t+1,...,t+k-1 *)
Definition Zero_between t k := forall t', t+k > t' -> t' >= t -> sigma t' = 0.
(* Zero_between is a decidable property (check for k,...,0) *)
Lemma zero_between_dec : forall t k, {Zero_between t k} + {~Zero_between t k}.
Proof.
introv. induction k.
- left. unfold Zero_between. introv G1 G2. omega.
- destruct IHk as [G|G].
+ assert (G1:{sigma (t+k) > 0}+{~ sigma (t+k) > 0}) by apply gt_dec.
destruct G1 as [G1|G1].
* right. intro G2.
assert (Y1: t + S k > t + k) by omega.
assert (Y2: t + k >= t) by omega.
apply (G2 (t+k) Y1) in Y2. omega.
* left.
introv G2 G3.
set (X:=G t').
assert (Y:{t'=t+k}+{t'<>t+k}) by apply Nat.eq_dec.
destruct Y as [Y|Y].
subst.
assert (Z:sigma (t + k) > 0 \/ 0 = sigma (t + k)) by apply gt_0_eq.
destruct Z. omega. symmetry; easy.
assert (Z:t + k > t') by omega.
apply X; easy.
+ right. introv F. apply G.
unfold Zero_between in *.
introv X1 X2.
assert (Y:{t'=t+k}+{t'<>t+k}) by apply Nat.eq_dec.
destruct Y as [Y|Y].
* apply F in X2; try omega.
* apply F in X2; try omega. easy.
Qed.
(* Next-event t1 t2: t2 is the next instant after (or at) t1 with an event *)
Definition Next_event t1 t2 := Later_event t1 t2 /\ Zero_between t1 (t2-t1).
(* Next_event is decidable *)
Lemma next_event_dec : forall t1 t2, {Next_event t1 t2} + {~Next_event t1 t2}.
Proof.
introv.
assert (G1:{sigma t2 > 0}+{~ sigma t2 > 0}) by apply gt_dec.
assert (G2:{t2 >= t1}+{~ t2 >= t1}) by apply le_dec.
assert (G3:{Zero_between t1 (t2-t1)} + {~Zero_between t1 (t2-t1)}) by apply zero_between_dec.
destruct G1 as [G1|G1]; destruct G2 as [G2|G2]; destruct G3 as[G3|G3];
try (right; intro X; destruct X as [[X1 X2] X3]; easy).
left. repeat split; easy.
Qed.
(* later implies next i.e. there exists a closest instant such that ... *)
Definition later_imp_next : forall t1 t2, Later_event t1 t2
-> exists t, Next_event t1 t.
Proof.
introv X.
apply (exists_min t2 (fun t => t >= t1 /\ sigma t > 0)) in X; try easy.
- destruct X as [t [X1 X2]].
exists t. split. easy.
unfold Zero_between.
introv G1 G2.
assert (Y1: {t1 <= t} + {~ t1 <= t}) by apply le_dec.
assert (Y2: {sigma t' > 0} + {~ sigma t' > 0}) by apply gt_dec.
destruct Y1 as [Y1|Y1]; destruct Y2 as [Y2|Y2].
+ rewrite le_plus_minus_r in G1; try easy.
apply X2 in G1. tauto.
+ rewrite le_plus_minus_r in G1; try easy.
apply X2 in G1.
assert (Z:sigma t' > 0 \/ 0 = sigma t') by apply gt_0_eq.
destruct Z. omega. easy.
+ destruct X1. apply Y1 in H. false.
+ assert (Z:sigma t' > 0 \/ 0 = sigma t') by apply gt_0_eq.
destruct Z. omega. easy.
- intro t.
assert (G1:{sigma t > 0}+{~ sigma t > 0}) by apply gt_dec.
assert (G2:{t >= t1}+{~ t >= t1}) by apply le_dec.
destruct G1; destruct G2; try (right; intro Y; destruct Y; easy).
left. easy.
Qed.
(* There exists a next (closest) instant with an event *)
Lemma next_event_exists : forall t1, {t2:nat | Next_event t1 t2}.
Proof.
intros t1.
eapply constructive_indefinite_ground_description_nat.
- apply next_event_dec.
- assert (X:= AE_Events_occur t1).
destruct X as [t2 X]. eapply later_imp_next. exact X.
Qed.
(* The function next can be defined *)
Definition next : instant -> instant.
intro t1. destruct (next_event_exists t1) as [t2 _]. exact t2.
Defined.
(* Expected properties of next *)
Lemma next_prop : forall t, next t >= t /\ sigma (next t ) > 0
/\ forall t', next t > t' -> t' >= t -> sigma t' = 0.
Proof.
intros t. unfold next.
destruct (next_event_exists t) as [t1 [G1 G2]].
destruct G1. repeat split; try easy.
introv G0 G1.
apply G2 in G1.
- easy.
- omega.
Qed.
This diff is collapsed.
Require Import Arith NPeano List Omega dmin tactics types next event_model.
(* ############################################################ *)
(** * Properties between the instants and the ids of occurrence *)
(* ############################################################ *)
(* Compute the number of occurence happening before an instant *)
Program Fixpoint sum_occ_before (t : instant) (k : nb_occurrences) (curr : instant)
{measure t} : id_occurrence :=
match t with
| 0 => k + (sigma curr)
| _ => sum_occ_before (t-1) (k + (sigma curr)) (curr + 1)
end.
Obligation 1. omega.
Defined.
(* return the id of the first occurrence taking place after an instant *)
Fixpoint first_occ_after (t : instant) : id_occurrence :=
(sum_occ_before t 0 0) + 1.
(* No instant should happened after an instant t and the first occurrence after t *)
Property first_occurence_after_prop (t : instant) (n : id_occurrence) :
instant_of(n) >= t /\ Zero_between t (instant_of n).
Proof.
Admitted.
Variable k_max : nb_occurrences.
(* By hypothesis the number of occurrences in an instant in the trace is bounded *)
Hypothesis E_bounded_event_at : forall t, le (sigma t) k_max.
Definition bounded_event_is (max_nb: nb_occurrences) :=
forall t, le (sigma t) max_nb.
(* If f k > dt /\ deltamin f, max_nb_occur_in_dt = max {k | f k <= dt} *)
Fixpoint max_k_in_dt (k: nb_occurrences)
(f: nb_occurrences -> duration) (dt: duration)
: nb_occurrences :=
match k with
| 0 => k
| S x => if ltb (f x) dt then x else max_k_in_dt (x-1) f dt
end.
Definition max_nb_occ_in_dt :=
max_k_in_dt k_max.
Program Fixpoint min_dt_with_k' (dt: duration)
(g: duration -> nb_occurrences) (k: nb_occurrences)
{measure k }: duration :=
match k with
| 0 => dt
| S x => if leb x (g (dt+1)) then dt else min_dt_with_k' (dt+1) g (k-1)
end.
Obligation 1. omega.
Defined.
Definition min_dt_with_k :=
min_dt_with_k' 0.
Lemma min_dt :
forall (g: duration -> nb_occurrences) k, eta_max g
-> lt (g (min_dt_with_k g k)) k /\ le k (g ((min_dt_with_k g k) + 1 )).
intros.
Admitted.
Lemma max_nb_occ :
forall (f : nb_occurrences -> duration) dt, delta_min f
-> lt (f (max_nb_occ_in_dt f dt)) dt /\ le dt (f ((max_nb_occ_in_dt f dt) + 1 )).
intros.
Admitted.
\ No newline at end of file
Require Import NPeano.
Require Import Coq.Arith.Le.
Require Import Coq.ZArith.BinIntDef.
Definition instant := nat.
Definition duration := nat.
Definition duration' (t: instant) (t1: instant) : duration :=
if (leb t t1) then t1 - t else t - t1.
Definition nb_occurrences := nat.
Definition id_occurrence := nat.
Definition id_occ_pls_nb (id: id_occurrence) (nb: nb_occurrences) : id_occurrence :=
id + nb.
Definition trace := instant -> nb_occurrences.
Variable sigma: trace.
(* At any instant there is an event occuring later *)
Definition Later_event t1 t2 := t2 >= t1 /\ sigma t2 > 0.
(* By hypotheis the trace sigma has that property *)
Hypothesis AE_Events_occur : forall t1, exists t2, Later_event t1 t2.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment