Commit 968de8c7 authored by Sophie Quinton's avatar Sophie Quinton

major restructuring

parent 1c6ab6d0
......@@ -4,28 +4,43 @@ 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.
## dependencies
1. conversion_functions.v:
- contains the conversions of the event model definitions and its conversion properties.
- depends on trace_properties, event_model and types (so also next, dmin and tactics)
2. event_models.v
- contains the definition of event models.
- depends on event_functions, trace_properties, types and util (so also tactics)?
3. event_functions.v
- contains the definitions of delta, eta and their properties.
- depends on trace_properties, types and util (so also tactics)
3. trace.v
- contains trace properties.
- depends on event_model, types and tactics (so also util)
4. types.v
- contains the type definitions used to define the event model.
- no dependencies
5. util.v
- contains some useful added lemmas to make our proofs.
- depends on tactics
6. tactics.v
- contains useful tactics.
- no dependencies
Also:
a. eval_event_model.v
- contains the evaluation of the event model.
- depends on event_model and types (so also next, util and tactics)
b. dmin.v
- contains the definition of the construction of d_min and its properties.
- depends on util and tactics
Require Import Arith NPeano List Omega tactics types next event_model.
Require Import trace_properties util dmin.
Require Import Coq.Logic.ClassicalFacts.
Require Import NPeano Arith Omega.
Require Import List Coq.Logic.ConstructiveEpsilon Coq.Logic.Decidable Omega.
Require Import event_models event_functions trace types util.
Require Import Arith_base Compare_dec Sumbool Div2 Min Max.
Require Import BinPos BinNat Pnat.
(* ########################################################### *)
(** * Conversion Functions *)
(* ########################################################### *)
(* ########################## *)
(* ** Conversion functions ** *)
(* ########################## *)
Definition conversion_delta_eta (f: nb_occurrences -> duration)
: duration -> nb_occurrences :=
fun (dt : duration) => max_nb_occ_in_dt f dt.
fun (dt : duration) => max_nb_occ_in_dt f dt.
Definition conversion_eta_delta (g: duration -> nb_occurrences)
: nb_occurrences -> duration :=
fun (k: nb_occurrences) => min_dt_with_k g k.
Definition conversion_round_trip (f: nb_occurrences -> duration)
: nb_occurrences -> duration :=
fun (k: nb_occurrences) => conversion_eta_delta (conversion_delta_eta f) k.
(* ########################################################### *)
(** * Conversion Properties *)
(* ########################################################### *)
(* ############################################ *)
(* ** Properties of the conversion functions ** *)
(* ############################################ *)
Property relation_eta_plus_delta_min_min :
forall (g: duration -> nb_occurrences) k,
g (conversion_eta_delta g k) + 1 <= k .
Proof.
intros eta_plus k.
Admitted.
Property relation_eta_plus_delta_min_maj :
forall (g: duration -> nb_occurrences) k,
k <= g (conversion_eta_delta g k + 1).
Proof.
intros eta_plus k.
Admitted.
(* eta_delta_min respect the min_delta_trace property *)
Property conversion_eta_delta_min_delta_trace :
forall (eta_plus: duration -> nb_occurrences),
max_eta_trace eta_plus
-> non_decreasing eta_plus
-> min_delta_trace (conversion_eta_delta eta_plus).
Proof.
intros eta_plus H_max_eta_trace H_non_decreasing_eta_plus.
unfold min_delta_trace.
intros n k.
assert (eta_plus (conversion_eta_delta eta_plus k) + 1 <= eta_plus (delta n k + 1)).
transitivity k.
apply (relation_eta_plus_delta_min_min eta_plus k).
apply eta_max_by_delta. easy.
apply plus_le_reg_r with (p := 1).
apply non_decreasing_lemma with (f := eta_plus). easy. easy.
Qed.
(* eta_delta_min respect is pseudo_superadditivity *)
Property conversion_eta_delta_min_superadditive:
forall (eta_plus: duration -> nb_occurrences),
subadditive eta_plus
-> pseudo_superadditive (conversion_eta_delta eta_plus).
Proof.
intros eta_plus H_eta_subadditive.
unfold pseudo_superadditive.
intros a b.
assert (eta_plus (conversion_eta_delta eta_plus (a + 1) + conversion_eta_delta eta_plus (b + 1)) + 1 <=
eta_plus (conversion_eta_delta eta_plus (a + (b + 1)) + 1)).
transitivity (eta_plus (conversion_eta_delta eta_plus (a + 1)) + (eta_plus (conversion_eta_delta eta_plus (b + 1))) + 1).
apply plus_le_compat_r.
apply H_eta_subadditive.
transitivity (a + b + 1).
apply plus_le_compat_r.
apply plus_le_compat with (n := eta_plus (conversion_eta_delta eta_plus (a + 1))) (m := a) (p := (eta_plus (conversion_eta_delta eta_plus (b + 1)))) (q := b).
apply plus_le_reg_r with (p := 1).
apply (relation_eta_plus_delta_min_min eta_plus (a + 1)).
apply plus_le_reg_r with (p := 1).
apply (relation_eta_plus_delta_min_min eta_plus (b + 1)).
replace (a + (b + 1)) with (a + b + 1).
apply (relation_eta_plus_delta_min_maj eta_plus (a + b + 1)).
ring_simplify; reflexivity.
assert (conversion_eta_delta eta_plus (a + 1) + conversion_eta_delta eta_plus (b + 1) + 1 <= conversion_eta_delta eta_plus (a + (b + 1)) + 1).
apply non_decreasing_lemma with (f:= eta_plus).
apply subadditive_implies_non_decreasing.
easy.
easy.
apply plus_le_reg_r with (p:=1).
omega.
Qed.
(* eta_delta_min is an delta_min *)
Property conversion_eta_plus_delta_min:
forall (eta_plus: duration -> nb_occurrences),
eta_max eta_plus
-> delta_min (conversion_eta_delta eta_plus).
Proof.
intros.
unfold delta_min.
split.
+ unfold eta_max in H. apply conversion_eta_delta_min_delta_trace. easy. apply subadditive_implies_non_decreasing. easy.
+ apply conversion_eta_delta_min_superadditive. unfold eta_max in H. easy.
Qed.
(* usefull lemma *)
(*
Definition subNat a b :=
if (ltb a b) then 0 else (a-b).
......@@ -48,7 +122,7 @@ forall t, sigma t = 0 -> instant_of(first_occ_after t) > t.
Proof.
Admitted.
Lemma occ_simlutanously :
Lemma occ_simultaneously :
forall t, sigma t > 0 -> instant_of(first_occ_after t) =
instant_of ((first_occ_after t) + (sigma t) - 1).
Proof.
......@@ -65,12 +139,17 @@ Proof.
intros.
unfold instant_of.
Admitted.
*)
(* Property' test *)
Property eta_to_delta :
(* Property eta_to_delta :
forall t dt k,
dt > 0 /\ (eta t dt) = k -> lt (delta (first_occ_after t) k) dt.
Proof.
Admitted.
intros.
destruct H as [H H0].
inversion H.
......@@ -95,7 +174,7 @@ inversion H.
apply first_occ_in_t. omega.
assert (H6: instant_of (first_occ_after t) =
instant_of ((first_occ_after t) + (sigma t) - 1)).
apply occ_simlutanously. omega.
apply occ_simultaneously. omega.
assert (H7: instant_of (first_occ_after t + sigma t - 1)-
instant_of (first_occ_after t) = 0) by omega.
assert (H8: delta (first_occ_after t) (eta t 1) = 0).
......@@ -180,11 +259,19 @@ inversion H.
u nfold eta.
(* apply IHk. *)
*)
(* Relation between eta and delta *)
(*
Property eta_to_delta :
forall t dt k,
(eta t dt) = k -> lt (delta (first_occ_after t) k) dt.
Proof.
Admitted.
*)
(*
intros.
induction dt.
(*cas initial dt = 0 *)
......@@ -231,38 +318,17 @@ induction dt.
assert (H4: a > S a).
assert (H4: instant_after (a - 1) 0 > instant_after (S (a - 1)) 0).
apply H3.
Admitted.
*)
(* Relation between delta and eta *)
Property delta_to_eta :
forall n k dt,
delta n k = dt -> eta (instant_of n) (dt+1) >= k.
intros.
induction dt.
+ simpl.
unfold delta in H.
assert (H0: instant_of(n + 1) >= instant_of(n)).
unfold instant_of.
induction n. simpl.
assert (H0: instant_of(n + k - 1) = instant_of(n)).
assert (H1: instant_of (n + k - 1) >= instant_of n).
- assert (H2: decidable (instant_of (n + k - 1) >= instant_of n))
by apply dec_ge.
destruct H2. omega.
assert (H3: instant_of (n + k - 1) < instant_of n). omega.
assert (H4: instant_of n - instant_of (n+k-1) > 0 ). omega.
contradiction.
Admitted.
(* Relation between eta and delta_min *)
(*
Property delta_min_by_eta :
forall t dt (f : nb_occurrences -> duration),
delta_min f
-> lt (f (eta t dt)) dt.
Proof.
intros.
destruct H as [H H1].
......@@ -281,31 +347,9 @@ assert (H4: (f (eta t dt)) < dt).
assert(H9: f (eta t dt) < dt) by omega.
omega. easy.
Qed.
*)
(* Relation between delta and eta_max *)
Property eta_max_by_delta :
forall n k (g : duration -> nb_occurrences),
eta_max g
-> g ((delta n k) + 1) >= k.
Proof.
intros.
destruct H as [H H1].
assert (H2:
delta n k = (delta n k) -> eta (instant_of n) ((delta n k) + 1) >= k)
by apply delta_to_eta.
assert (H3:
eta (instant_of n) ((delta n k) + 1) <= g ((delta n k) + 1)).
assert (H4: eta_max g). split. easy. easy.
apply H.
assert (H4: eta (instant_of n) ((delta n k) + 1) >= k).
apply H2. easy.
assert (H5: g ((delta n k) + 1) >= k) by omega.
omega.
Qed.
(* ########################################################### *)
(** * Conversion Proofs *)
(* ########################################################### *)
(* delta_eta_max respect the max_eta_trace property *)
......@@ -314,6 +358,9 @@ forall (f : nb_occurrences -> duration),
delta_min f
-> max_eta_trace (conversion_delta_eta f).
Proof.
Admitted.
(*
intros.
unfold max_eta_trace.
intros.
......@@ -340,12 +387,17 @@ apply H8.
split. easy. easy.
omega.
Qed.
*)
Property conversion_delta_eta_sub_additive :
forall (f : nb_occurrences -> duration),
delta_min f
-> subadditive (conversion_delta_eta f).
intros.
Proof.
Admitted.
(*intros.
unfold subadditive.
intros.
(* eta_max (dt) = max {k | delta_min (k) < dt }*)
......@@ -394,6 +446,7 @@ apply H13.
split. easy. easy.
omega.
Qed.
*)
(* delta_eta_max is an eta_max *)
Property conversion_delta_min_eta_max:
......@@ -407,103 +460,8 @@ split.
+ apply conversion_delta_eta_sub_additive. easy.
Qed.
(* eta_delta_min respect the min_delta_trace property *)
Property conversion_eta_delta_min_delta_trace :
forall (g: duration -> nb_occurrences),
eta_max g
-> min_delta_trace (conversion_eta_delta g).
Proof.
intros.
unfold min_delta_trace.
intros.
unfold conversion_eta_delta.
(* eta_max is increasing *)
assert (H1: forall a, g a + 1 >= g a).
intros. omega.
assert (H2:
lt (g (min_dt_with_k g k)) k /\ le k (g ((min_dt_with_k g k) + 1 ))).
intros. apply min_dt. easy.
destruct H2 as [H2 H3].
destruct H as [H H'].
assert (H4: g ((delta n k) + 1) >= k).
apply eta_max_by_delta. split. easy. easy.
assert (H5: g ((delta n k) + 1) > g (min_dt_with_k g k)) by omega.
assert (H6: (delta n k + 1) > min_dt_with_k g k).
assert (H7: g k + 1 >= g k /\
g ((delta n k) + 1) > g (min_dt_with_k g k)).
intros. split. easy. easy.
assert (H8: g k + 1 >= g k /\
g ((delta n k) + 1) > g (min_dt_with_k g k)
-> ((delta n k) + 1) > min_dt_with_k g k) by apply increasing_gt.
apply H8.
split. easy. easy.
omega.
Qed.
(* eta_delta_min respect is pseudo_superadditivity *)
Property conversion_eta_delta_min_superadditive:
forall (g: duration -> nb_occurrences),
eta_max g
-> pseudo_superadditive (conversion_eta_delta g).
Proof.
intros.
unfold pseudo_superadditive.
intros.
assert (H1: forall k,
lt (g (min_dt_with_k g k)) k /\ le k (g ((min_dt_with_k g k) + 1 ))).
intros. apply min_dt. easy.
unfold conversion_eta_delta.
assert (H2: lt (g (min_dt_with_k g (x+1))) (x+1) /\
le (x+1) (g ((min_dt_with_k g (x+1)) + 1 )))
by apply H1. destruct H2 as [H2 H2'].
assert (H3: lt (g (min_dt_with_k g (y+1))) (y+1) /\
le (y+1) (g ((min_dt_with_k g (y+1)) + 1 )))
by apply H1. destruct H3 as [H3 H3'].
assert (H4: lt (g (min_dt_with_k g (x+(y+1)))) (x+(y+1)) /\
le (x+(y+1)) (g ((min_dt_with_k g (x+(y+1))) + 1 )))
by apply H1. destruct H4 as [H4 H4'].
assert (H5: g (min_dt_with_k g (x+1)) + g (min_dt_with_k g (y+1)) <
x+y+1) by omega.
(* subadditivite de eta_max *)
assert (H6: g (min_dt_with_k g (x+1)) + g (min_dt_with_k g (y+1))
>= g (min_dt_with_k g (x+1) + min_dt_with_k g (y+1))).
destruct H as [H H']. apply H'.
assert (H7: g (min_dt_with_k g (x+1) + min_dt_with_k g (y+1))
< g (min_dt_with_k g (x + (y + 1)) + 1)) by omega.
(* eta_max is increasing *)
assert (H8: forall a, g a + 1 >= g a).
intros. omega.
assert (H9: min_dt_with_k g (x+1) + min_dt_with_k g (y+1)
< min_dt_with_k g (x + (y + 1)) + 1).
assert (H10 : g x + 1 >= g x /\
g (min_dt_with_k g (x+1) + min_dt_with_k g (y+1))
< g (min_dt_with_k g (x + (y + 1)) + 1)).
intros. split. easy. easy.
assert (H13: g x + 1 >= g x /\
g (min_dt_with_k g (x+1) + min_dt_with_k g (y+1))
< g (min_dt_with_k g (x + (y + 1)) + 1)
-> min_dt_with_k g (x+1) + min_dt_with_k g (y+1)
< min_dt_with_k g (x + (y + 1)) + 1).
apply increasing_gt.
apply H13.
split. easy. easy.
omega.
Qed.
(* eta_delta_min is an delta_min *)
Property conversion_eta_max_delta_min:
forall (g: duration -> nb_occurrences),
eta_max g
-> delta_min (conversion_eta_delta g).
Proof.
intros.
unfold eta_max.
split.
+ apply conversion_eta_delta_min_delta_trace. easy.
+ apply conversion_eta_delta_min_superadditive. easy.
Qed.
(* conversion from delta_min to eta_max to delta_min is the identity*)
(* conversion from delta_min to eta_max to delta_min is the identity
Property conversion_round_trip_identity:
forall (f: nb_occurrences -> duration),
delta_min f
......@@ -513,4 +471,5 @@ intros.
unfold conversion_round_trip.
unfold conversion_delta_eta.
unfold conversion_eta_delta.
Admitted.
\ No newline at end of file
Admitted.
*)
......@@ -5,37 +5,12 @@
This function is shown to be super-additive and to be minimal.
P. Fradet - 2016 *)
Require Import Arith NPeano List Omega tactics.
Require Import Arith NPeano List Omega.
Require Import util tactics.
Set Implicit Arguments.
(** General property on P:nat->Prop predicates:
if P is decidable and P holds for at least one nat
then there is a minimal integer for which P holds *)
Lemma P_upto_n : forall P n, (forall x, P x \/ ~ P x)
-> (exists m, m < n /\ P m) \/ (forall m, m < n -> ~ P m).
Proof.
introv Pdec. induction n.
- right. introv H. inverts H.
- destruct IHn as [[m IHn]|IHn].
+ left. exists m. intuition.
+ destruct (Pdec n).
* left. exists n. intuition.
* right. introv G.
apply lt_n_Sm_le in G.
destruct G; try easy.
apply IHn. omega.
Qed.
Lemma exists_min : forall n (P:nat->Prop), (forall x, P x \/ ~ P x) -> P n
-> exists m, P m /\ forall p, p < m -> ~ P p.
Proof.
induction n using lt_wf_ind; intros.
destruct (P_upto_n P n) as [[? [? ?]] | ?]; try easy.
- eauto.
- exists n; easy.
Qed.
(** Environments as association lists
used to record the known/given values of dist_min
......
Require Import Arith NPeano List Omega dmin tactics types next event_model.
Require Import Arith NPeano List Omega.
Require Import event_model types.
(* ########################################################### *)
(** * Evaluations *)
......
Require Import NPeano Arith Omega.
Require Import trace types util.
(* ######################################################## *)
(* ** Definitions related to the event load function eta ** *)
(* ######################################################## *)
(** 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.
(* ############################################################## *)
(* ** Definitions related to the event distance function delta ** *)
(* ############################################################## *)
(** The event distance function *)
Definition delta (n : id_occurrence) (k : nb_occurrences) : duration :=
instant_of (n + k - 1) - instant_of n.
(* ####################### *)
(* ** Properties of eta ** *)
(* ####################### *)
Property eta_additive:
forall dt1 dt2 t,
eta t (dt1 + dt2) = eta t dt1 + eta (t + dt1) dt2.
Proof.
intros dt1 dt2.
induction dt1.
intros. simpl. replace (t + 0) with t; easy.
intros.
simpl.
rewrite <- plus_assoc.
apply Nat.add_cancel_l.
replace (t + S dt1) with (S t + dt1).
apply (IHdt1 (S t)).
omega.
Qed.
(* ######################### *)
(* ** Properties of delta ** *)
(* ######################### *)
Property delta_additive:
forall k1 k2 n,
delta n (k1 + k2) = delta n k1 + delta (n + k1) (k2 + 1).
Proof.
intros.
unfold delta.
rewrite plus_assoc.
replace (n + (k1 + 1) - 1) with (n + k1).
Focus 2. omega.
replace (instant_of (n + k1) - instant_of n + (instant_of (n + k1 + k2 - 1) - instant_of (n + k1))) with (instant_of (n + k1 + k2 - 1) - instant_of (n + k1) + instant_of (n + k1) - instant_of n).
Admitted.