Commit 4387b7c1 authored by Pascal Fradet's avatar Pascal Fradet

Clean PF version

parent 968de8c7
Require Import NPeano Arith Omega.
Require Import event_models event_functions trace types util.
Require Import NPeano Arith Omega.
Require Import event_models event_functions trace types util tactics.
(* ########################## *)
(* ** Conversion functions ** *)
(* ########################## *)
Definition conversion_delta_eta (f: nb_occurrences -> duration)
: duration -> nb_occurrences :=
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_delta_eta (f: nb_occurrences -> duration)
: duration -> nb_occurrences :=
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.
(* ############################################ *)
(* ** 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.
(*
Definition subNat a b :=
if (ltb a b) then 0 else (a-b).
Lemma delta_n_0_is_null :
forall n, delta n 0 = 0.
Proof.
Admitted.
Lemma first_occ_in_t :
forall t, sigma t > 0 -> instant_of(first_occ_after t) = t.
Proof.
Admitted.
Lemma first_occ_after_t_n :
forall t, sigma t = 0 -> instant_of(first_occ_after t) > t.
Proof.
Admitted.
Lemma occ_simultaneously :
forall t, sigma t > 0 -> instant_of(first_occ_after t) =
instant_of ((first_occ_after t) + (sigma t) - 1).
Proof.
Admitted.
Lemma nb_occ_null_at_inst :
forall t dt, eta t dt = 0 -> sigma t = 0 /\ forall t', t' > t /\ t' < t + dt /\ sigma t' = 0.
Proof.
Admitted.
Lemma instant_of_increasing:
forall k, instant_of(k) <= instant_of(k+1).
Proof.
intros.
unfold instant_of.
Admitted.
*)
(* Property' test *)
(* 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.
(* cas initial dt = 1 *)
+ assert (H2: sigma t = k).
assert (H3: eta t 1 = k).
replace 1 with dt by omega. easy.
unfold eta in H3.
replace (sigma t) with ((sigma t) + 0) by omega.
easy.
(* 2 cas soit k = 0 ou k > 0 *)
induction k.
- (* cas sigma t = 0 *)
assert (H3: delta (first_occ_after t) 0 = 0) by
apply delta_n_0_is_null. omega.
- (* cas sigma t > 0 *)
unfold delta.
assert (H5: delta (first_occ_after t) (S k) =
instant_of (first_occ_after t + S k - 1) - instant_of (first_occ_after t)).
unfold delta. easy.
assert (H4: instant_of(first_occ_after t) = t).
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_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).
unfold eta.
assert (H9: (sigma t + 0) = S k).
assert (H10: sigma t + 0 = sigma t).
replace (sigma t) with (sigma t + 0) by omega.
replace (sigma t + 0 + 0) with (sigma t + 0) by omega.
easy.
replace (sigma t + 0) with (sigma t) by omega. easy.
replace (sigma t + 0) with (S k) by omega.
unfold delta.
replace (S k) with (sigma t) by omega. easy.
replace (S k) with (sigma t) by omega. omega.
+ (* cas ou dt > 1 *)
induction k.
- (* cas ou eta t dt = 0 *)
assert (H3: instant_of (first_occ_after t) > t). apply first_occ_after_t_n.
(* eta (t, dt) = 0 -> sigma (t) = 0 *)
assert (H5: sigma t = 0 /\ (forall t', t' > t /\ t' < t + dt /\ sigma t' = 0)).
apply nb_occ_null_at_inst. easy.
destruct H5 as [H3 H4]. easy.
(* forall n, delta(n, 0) = 0*)
assert (H4: delta (first_occ_after t) 0 = 0) by
apply delta_n_0_is_null.
omega.
- (* cas ou eta t dt > 0 *)
assert (tmp: eta t dt = eta t (S m)).
replace (S m) with (dt) by omega. easy.
assert (H3: (sigma t + eta (S t) (m)) = eta t (S m)).
easy.
assert (H4: dt - 1 = m) by omega.
assert (H5: (sigma t + eta (S t) (m)) = eta t dt) by omega.
assert (H6: (sigma t + eta (S t) (dt - 1)) = eta t dt).
replace (dt - 1) with (m) by omega. omega.
replace (S k) with (sigma t + eta (S t) (dt - 1)) by omega.
induction (sigma t).
* (* sub-cas ou first_occ_after t > t *)
simpl.
replace (eta (S t) (dt - 1)) with (eta t dt) by omega.
replace (eta t dt) with (S k) by omega.
replace (first_occ_after t + S k - 1) with (first_occ_after t + k) by omega.
induction k.
(* case k = 0 *)
unfold delta.
assert (H7: forall x, x + 1 - 1 = x). intros. omega.
assert (H8: (first_occ_after t) + 1 - 1 = (first_occ_after t)).
apply H7 with (x := (first_occ_after t)).
replace (first_occ_after t + 1 - 1) with
(first_occ_after t) by apply H8. omega.
unfold delta in IHk.
(* case where k >= 1*)
(* instant_of croissante => inst(k-1) <= inst(k)*)
assert (H7: instant_of ((first_occ_after t) + k - 1) <=
instant_of ((first_occ_after t) + k) ).
Check instant_of_increasing.
replace (instant_of ((first_occ_after t) + k)) with
(instant_of ((first_occ_after t) + k -1 + 1)).
apply instant_of_increasing with (k := (first_occ_after t) + k-1).
(* only true if k > 0*)
assert (H7: forall x, x > 0 -> x - 1 + 1 = x).
intros. inversion H7. simpl. easy.
simpl. omega.
apply instant_of_increasing with (k := k-1).
apply IHk with (k := S k).
assert (H7: (eta (t + 1) (dt - 1)) < (eta t dt)).
replace (t+1) with (S t) by omega.
assert (H8: (dt > 0 ) -> eta t dt = (sigma t) + eta (S t) (dt - 1)).
intro.
case dt.
replace (0-1) with 0 by omega.
assert (H8: (eta (S t) 0) = 0) by trivial.
replace (eta (S t) 0) with 0 by omega. simpl.
SearchAbout case.
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 *)
+ assert(H1: k = 0).
assert(H2: eta t 0 = 0). simpl. easy.
easy.
replace k with 0 by omega.
unfold delta.
simpl.
(* instant_of est une fonction croissante *)
assert (H2: forall (a: nat), instant_of(a-1) <= instant_of(a)).
- intros.
unfold instant_of.
induction a.
easy.
simpl.
replace (a-0) with a by omega.
assert (H2: decidable ((instant_after a 0) <= (instant_after (S a) 0)))
by apply dec_le.
destruct H2. omega.
assert (H3: instant_after a 0 > instant_after (S a) 0) by omega.
assert (IHa': instant_after (subNat a 1) 0 <= instant_after (S (subNat a 1)) 0).
assert (H4: (S (subNat a 1)) = a).
assert (H5: (S (a - 1)) = (a -1) + 1). omega.
assert (H6: (subNat a 1) + 1 = a).
induction a. simpl.
assert (H5: forall a, S a = a +1). intro. omega.
assert (H6: forall a, a + 1 - 1 = a). intro. omega.
assert (H7: forall a, a - 1 + 1 = a + 1 - 1). intro.
assert (H8: (a0 - 1) + 1 = a0). omega.
Check Z_N_nat.
Check Z.of_N.
(*Check inj_sub.
Check inj_sub_max.*)
assert (H9: Z.of_N(-1 + 1) = 0).
replace (-1 + 1) with 0 by omega.
apply H5 with (a0 = (a-1)).
simpl.
replace (S (a - 1)) with a by omega.
assert (H4: a > S a).
assert (H4: instant_after (a - 1) 0 > instant_after (S (a - 1)) 0).
apply H3.
*)
(* 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].
assert (H2:
(eta t dt) = (eta t dt) -> lt (delta (first_occ_after t) (eta t dt)) dt)
by apply eta_to_delta.
assert (H3:
delta (first_occ_after t) (eta t dt) >= f (eta t dt)).
assert (H4: delta_min f). split. easy. easy.
apply H.
assert (H4: (f (eta t dt)) < dt).
assert(H5: delta (first_occ_after t) (eta t dt) >= f (eta t dt)) by apply H3.
assert(H6: eta t dt = eta t dt). easy.
assert(H7: delta (first_occ_after t) (eta t dt) < dt). apply H2. easy.
assert(H8: delta (first_occ_after t) (eta t dt) >= f (eta t dt)) by apply H.
assert(H9: f (eta t dt) < dt) by omega.
omega. easy.
Qed.
*)
(* delta_eta_max respect the max_eta_trace property *)
Property conversion_delta_eta_max_eta_trace :
forall (f : nb_occurrences -> duration),
delta_min f
-> max_eta_trace (conversion_delta_eta f).
Proof.
Admitted.
(*
intros.
unfold max_eta_trace.
intros.
unfold conversion_delta_eta.
(* delta_min is increasing *)
assert (H1: forall a, f a + 1 >= f a).
intros. omega.
assert (H2:
lt (f (max_nb_occ_in_dt f dt)) dt /\ le dt (f ((max_nb_occ_in_dt f dt) + 1 ))).
intros. apply max_nb_occ. easy.
destruct H2 as [H2 H3].
destruct H as [H H'].
assert (H4: (f (eta t dt)) < dt).
apply delta_min_by_eta. split. easy. easy.
assert (H5: f (eta t dt) < f (max_nb_occ_in_dt f dt + 1)) by omega.
assert (H6: eta t dt < max_nb_occ_in_dt f dt + 1).
assert (H7: f dt + 1 >= f dt /\
f (eta t dt) < f (max_nb_occ_in_dt f dt + 1)).
intros. split. easy. easy.
assert (H8: f dt + 1 >= f dt /\
f (eta t dt) < f (max_nb_occ_in_dt f dt + 1)
-> eta t dt < max_nb_occ_in_dt f dt + 1) by apply increasing_lt.
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).
Proof.
Admitted.
(*intros.
unfold subadditive.
intros.
(* eta_max (dt) = max {k | delta_min (k) < dt }*)
assert (H1: forall dt,
lt (f (max_nb_occ_in_dt f dt)) dt /\ le dt (f ((max_nb_occ_in_dt f dt) + 1 ))).
intros. apply max_nb_occ. easy.
unfold conversion_delta_eta.
(* eta_max (x) = max {k | delta_min (k) < x }*)
assert (H2: f (max_nb_occ_in_dt f x) < x /\ f (max_nb_occ_in_dt f x + 1) >= x)
by apply H1. destruct H2 as [H2 H2'].
(* eta_max (y) = max {k | delta_min (k) < y }*)
assert (H3: f (max_nb_occ_in_dt f y) < y /\ f (max_nb_occ_in_dt f y + 1) >= y)
by apply H1. destruct H3 as [H3 H3'].
(* delta_min (eta_max (x) + 1) + delta_min (eta_max (x) + 1) >= x + y*)
assert (H4: f (max_nb_occ_in_dt f x + 1) + f (max_nb_occ_in_dt f y + 1) >= x + y) by omega.
(* eta_max (x + y) = max {k | delta_min (k) < x + y } *)
assert (H5: f (max_nb_occ_in_dt f (x +y)) < (x +y)
/\ f (max_nb_occ_in_dt f (x +y) + 1) >= (x +y)) by apply H1.
destruct H5 as [H5 H5'].
(* delta_min (eta_max (x) + 1) + delta_min (eta_max (x) + 1) > delta_min (eta_max (x + y))*)
assert (H6: f (max_nb_occ_in_dt f x + 1) + f (max_nb_occ_in_dt f y + 1)
> f (max_nb_occ_in_dt f (x +y))) by omega.
destruct H as [H H'].
unfold pseudo_superadditive in H'.
assert (H7: f ((max_nb_occ_in_dt f x) + ((max_nb_occ_in_dt f y) + 1))
>= f (max_nb_occ_in_dt f x + 1) + f (max_nb_occ_in_dt f y + 1))
by apply H'.
assert (H8: f ((max_nb_occ_in_dt f x) + ((max_nb_occ_in_dt f y) + 1)) >
f (max_nb_occ_in_dt f (x + y))). omega.
(* delta_min is increasing *)
assert (H10: forall a, f a + 1 >= f a).
intros. omega.
assert (H11: (max_nb_occ_in_dt f x) + ((max_nb_occ_in_dt f y) + 1) >
max_nb_occ_in_dt f (x + y)).
assert (H12: f x + 1 >= f x /\
f ((max_nb_occ_in_dt f x) + ((max_nb_occ_in_dt f y) + 1)) >
f (max_nb_occ_in_dt f (x + y))).
intros. split. easy. easy.
assert (H13: f x + 1 >= f x /\
f ((max_nb_occ_in_dt f x) + ((max_nb_occ_in_dt f y) + 1)) >
f (max_nb_occ_in_dt f (x + y))
-> (max_nb_occ_in_dt f x) + ((max_nb_occ_in_dt f y) + 1) >
max_nb_occ_in_dt f (x + y)).
apply increasing_gt.
apply H13.
split. easy. easy.
omega.
Qed.
*)
(* delta_eta_max is an eta_max *)
Property conversion_delta_min_eta_max:
forall (f : nb_occurrences -> duration),
delta_min f
-> eta_max (conversion_delta_eta f).
intros.
unfold eta_max.
split.
+ apply conversion_delta_eta_max_eta_trace. easy.
+ apply conversion_delta_eta_sub_additive. easy.
Qed.
(* 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
-> f = conversion_round_trip f.
Proof.
intros.
unfold conversion_round_trip.
unfold conversion_delta_eta.
unfold conversion_eta_delta.
Admitted.
*)
(* ############################################ *)
Property g_min_dt_lt : forall (g : duration -> nb_occurrences) (dt d: duration) (k : nb_occurrences),
g 0 = 0 -> 1 <= k
-> min_dt_with_k' dt g k = d -> g d + 1 <= k.
Proof.
induction dt; introv G H M.
- cbn in *. subst. omega.
- dupl G G1. cbn in M.
destruct k; cbn in *.
+ apply IHdt; easy.
+ destruct (le_lt_dec (g dt) k) as [I|I].
* replace (g dt <=? k) with true in M
by (symmetry; apply leb_correct; easy).
subst. omega.
* replace (g dt <=? k) with false in M
by (symmetry; apply leb_correct_conv; easy).
apply IHdt; easy.
Qed.
Property g_min_dt_le : forall (g : duration -> nb_occurrences) (dt d: duration) (k : nb_occurrences),
g 0 = 0 -> k <= g dt
-> min_dt_with_k' dt g k = d -> k <= g (d + 1).
Proof.
induction dt; introv H G M.
- cbn in *. subst. omega.
- dupl G G1. cbn in M.
destruct k; cbn in *.
+ apply IHdt; try easy. omega.
+ destruct (le_lt_dec (g dt) k) as [I|I].
* replace (g dt <=? k) with true in M
by (symmetry; apply leb_correct; easy).
subst. replace (d+1) with (S d) by omega. exact G.
* replace (g dt <=? k) with false in M
by (symmetry; apply leb_correct_conv; easy).
apply IHdt. easy. omega. easy.
Qed.
Property relation_eta_plus_delta_min_min : forall (g: duration -> nb_occurrences) k,
g 0 = 0 -> 1 <= k
-> g (conversion_eta_delta g k) + 1 <= k .
Proof.
intros.
unfold conversion_eta_delta.
unfold min_dt_with_k.
apply g_min_dt_lt with (dt:=(S (dt_max * k))); easy.
Qed.
Property relation_eta_plus_delta_min_maj : forall (g: duration -> nb_occurrences) k,
g 0 = 0 -> k <= g (S (dt_max * k))
-> k <= g (conversion_eta_delta g k + 1).
Proof.
intros.
unfold conversion_eta_delta.
unfold min_dt_with_k.
apply g_min_dt_le with (dt:=(S (dt_max * k))); easy.
Qed.
(* Properties needed on eta functions ... *)
Definition wf_nf nf := nf 0 = 0 /\ non_decreasing nf /\ forall k, k <= nf (S (dt_max * k)).
(* These three properties hold for eta t *)
Property eta_wf_nf : forall t, eta t 0 = 0 /\ non_decreasing (eta t) /\ forall k, k <= eta t (S (dt_max * k)).
Proof.
intros. split.
easy. split.
apply eta_nd.
intros; apply eta_k_dtmax.
Qed.
(* eta_delta_min respects the min_delta_trace property *)
Property conversion_eta_delta_min_delta_trace :
forall (eta_plus: duration -> nb_occurrences),
max_eta_trace eta_plus
-> wf_nf eta_plus
-> min_delta_trace (conversion_eta_delta eta_plus).
Proof.
intros eta_plus H_max_eta_trace [etaZero [etaIncr etaBound]].
unfold min_delta_trace.
intros n k In.
destruct k. cbn. rewrite Nat.mul_0_r. cbn. omega.
assert (eta_plus (conversion_eta_delta eta_plus (S k)) + 1 <= eta_plus (delta n (S k) + 1)).
transitivity (S k).
apply (relation_eta_plus_delta_min_min eta_plus (S k)); try omega; try easy.
apply eta_max_by_delta; try omega; try easy.
apply plus_le_reg_r with (c := 1).
apply non_decreasing_lemma with (f := eta_plus). easy. easy.
Qed.
(* eta_delta_min is pseudo_superadditive *)
Property conversion_eta_delta_min_superadditive:
forall (eta_plus: duration -> nb_occurrences),
subadditive eta_plus -> wf_nf eta_plus
-> pseudo_superadditive (conversion_eta_delta eta_plus).
Proof.
intros eta_plus H_eta_subadditive [etaZero [etaIncr etaBound]].
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).