Library inw_aux
Set Implicit Arguments.
Require Import Bool.
Require Import Omega.
Require Import misc.
Require Import inw_def.
Definition well_formed_inw (w:inw) := w 0 = 0.
Definition well_formed_inw_n (w:inw) (n:nat) :=
well_formed_inw w /\
forall i, w i <= n.
Definition delay (d:nat) (w:inw) : inw :=
fun i => w (i - d).
Definition non_null_stream (w: inw) :=
forall i: nat, exists j: nat, j > i /\ ~ w j = 0.
Definition well_formed_ones (ones_w: nat -> nat) :=
ones_w 0 = 0
/\
forall i, (ones_w i <= ones_w (S i)).
Definition well_formed_ones_n (ones_w: nat -> nat) (n: nat) :=
well_formed_ones ones_w
/\
forall i, ones_w (S i) <= n + (ones_w i).
Section well_formed_n_properties.
Property well_formed_inw_n_weakening:
forall w: inw,
forall n,
forall H_wf: well_formed_inw_n w n,
forall n',
forall H_n_le_n': n <= n',
well_formed_inw_n w n'.
Proof.
intros.
unfold well_formed_inw_n.
destruct H_wf.
split; auto.
intros.
apply (le_trans (w i) n n'); auto.
Qed.
Property well_formed_ones_n_weakening:
forall w: inw,
forall n,
forall H_wf: well_formed_ones_n w n,
forall n',
forall H_n_le_n': n <= n',
well_formed_ones_n w n'.
Proof.
intros.
unfold well_formed_ones_n.
destruct H_wf.
split; auto.
intros.
apply (le_trans (w (S i)) (n + w i) (n' + w i)); auto.
apply plus_le_compat_r.
assumption.
Qed.
End well_formed_n_properties.
Section ones_properties.
Property red_ones:
forall w: inw,
forall i,
ones w i =
match i with
| 0 => 0
| S i' =>
w i + ones w i'
end.
Proof.
intros.
induction i.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
Property ones_S_i_eq_n_plus_ones_i:
forall (w:inw),
forall i,
ones w (S i) = (w (S i)) + ones w i.
Proof.
intros.
simpl.
trivial.
Qed.
Property ones_pred_i_eq_ones_i_minus_n:
forall (w:inw),
forall i,
ones w (pred i) = ones w i - w i.
Proof.
intros.
case_eq i.
compute.
reflexivity.
intros i' H_i.
simpl.
omega.
Qed.
Property ones_increasing_one:
forall (w:inw) i,
ones w i <= ones w (S i).
Proof.
intros.
simpl.
omega.
Qed.
Property ones_increasing_x:
forall (w:inw) i x,
ones w i <= ones w (x + i).
Proof.
intros.
induction x.
simpl.
trivial.
assert (H_add: S x + i = S (x + i)); auto with arith.
rewrite H_add.
simpl.
omega.
Qed.
Property ones_increasing:
forall (w:inw) i j,
forall (H_i_le_j: i <= j),
ones w i <= ones w j.
Proof.
intros.
case_eq j.
case_eq i.
trivial.
intros n H_i_pos H_j.
rewrite H_i_pos in H_i_le_j.
rewrite H_j in H_i_le_j.
absurd (S n <= 0); auto with arith.
intros j' H_j.
rewrite H_j in H_i_le_j.
assert (exists x, j = x + i).
exists (S j' - i).
omega.
inversion H.
rewrite <- H_j.
rewrite H0.
eapply ones_increasing_x.
Qed.
Property ones_i_le_i_mult_n:
forall w:inw,
forall n: nat,
forall H_wf_n: well_formed_inw_n w n,
forall i,
ones w i <= n * i.
Proof.
intros.
induction i.
simpl.
omega.
rewrite red_ones.
rewrite <- mult_n_Sm.
rewrite plus_comm.
apply plus_le_compat; auto.
destruct H_wf_n.
apply (H0 (S i)).
Qed.
Property ones_impl_well_formed_ones:
forall w: inw,
well_formed_ones (ones w).
Proof.
intros.
split.
simpl.
reflexivity.
apply ones_increasing_one.
Qed.
Property ones_n_impl_well_formed_ones_n:
forall w: inw,
forall n: nat,
forall H_wf_n: well_formed_inw_n w n,
well_formed_ones_n (ones w) n.
Proof.
intros.
split;
try solve [ apply ones_impl_well_formed_ones ].
intros.
rewrite red_ones.
apply plus_le_compat_r.
destruct H_wf_n.
apply (H0 (S i)).
Qed.
Remark le_prop_aux:
forall i j x,
forall H_i_le_j: i <= j,
i <= x + j.
Proof.
intros.
omega.
Qed.
Property ones_increasing_rev:
forall (w:inw) i j,
forall (H_ones_i_le_ones_j: ones w i < ones w j),
i <= j.
Proof.
intros.
elim (le_lt_dec i j); auto.
intros H_j_lt_i.
absurd (ones w i < ones w j); auto.
apply le_not_lt.
apply ones_increasing.
apply lt_le_weak.
assumption.
Qed.
Property w_i_ge_1_impl_ones_pos:
forall w:inw,
forall H_wf: well_formed_inw w,
forall i,
forall H_w: w i >= 1,
ones w i > 0.
Proof.
intros.
case_eq i.
intro H_i.
unfold well_formed_inw in H_wf.
rewrite H_i in H_w.
rewrite H_wf in H_w.
auto with arith.
intros i' H_i.
simpl.
rewrite H_i in H_w.
omega.
Qed.
Property ones_eq_0_impl_w_eq_0:
forall w: inw,
forall H_wf: well_formed_inw w,
forall i,
forall H_ones_eq_0: ones w i = 0,
w i = 0.
Proof.
intros.
case_eq i.
intros H_i.
assumption.
intros i' H_i.
rewrite H_i in H_ones_eq_0.
clear H_i i.
induction i'.
simpl in H_ones_eq_0.
omega.
assert (H_S_i'_ge_1: S i' >= 1);
auto with arith.
assert (H_ones_S_i'_eq_0: ones w (S i') = 0).
assert (H_tmp: 0 = ones w (S i')).
apply le_n_O_eq.
rewrite <- H_ones_eq_0.
apply ones_increasing_one.
auto.
rewrite red_ones in H_ones_eq_0.
rewrite H_ones_S_i'_eq_0 in H_ones_eq_0.
omega.
Qed.
Property ones_i_eq_0_impl_w_i'_eq_0:
forall w: inw,
forall H_wf: well_formed_inw w,
forall i,
forall H_ones_eq_0: ones w i = 0,
forall i',
forall H_i'_le_i: i' <= i,
w i' = 0.
Proof.
intros.
apply ones_eq_0_impl_w_eq_0; auto.
assert (H_cc: 0 = ones w i').
apply le_n_O_eq.
rewrite <- H_ones_eq_0.
apply ones_increasing.
assumption.
auto.
Qed.
Property w_i'_eq_0_impl_ones_i_eq_0:
forall w: inw,
forall i,
forall H_w: (forall i', forall H_i'_le_i: i' <= i, w i' = 0),
ones w i = 0.
Proof.
induction i.
intros.
simpl.
trivial.
intros.
rewrite ones_S_i_eq_n_plus_ones_i.
rewrite IHi; auto.
rewrite H_w; auto.
Qed.
Property non_null_impl_ones_i_ge_j:
forall w: inw,
forall H_non_null_stream: non_null_stream w,
forall j,
exists i,
ones w i >= j.
Proof.
induction j.
exists 0.
simpl.
unfold ge.
apply le_refl.
elim IHj.
intros i IH.
elim (H_non_null_stream i).
intros i' H_tmp.
destruct H_tmp.
exists i'.
assert (H_aux: i' = S (pred i')).
apply (S_pred i' i).
assumption.
rewrite H_aux.
rewrite H_aux in H0.
rewrite ones_S_i_eq_n_plus_ones_i; auto.
replace (S j) with (1 + j); auto.
unfold ge.
apply plus_le_compat; try omega.
unfold ge in IH.
apply (le_trans j (ones w i) (ones w (pred i'))); auto.
apply ones_increasing.
apply lt_n_Sm_le.
rewrite <- H_aux.
assumption.
Qed.
Property non_null_impl_ones_i_le_j:
forall w: inw,
forall H_non_null_stream: non_null_stream w,
forall j,
exists i,
ones w i <= j.
Proof.
intros.
exists 0.
simpl.
auto with arith.
Qed.
Property w_eq_impl_ones_eq:
forall w1 w2: inw,
forall H_ones_eq: (forall i, i > 0 -> w1 i = w2 i),
forall i,
ones w1 i = ones w2 i.
Proof.
induction i.
simpl.
reflexivity.
simpl.
rewrite IHi.
rewrite (H_ones_eq (S i)); auto with arith.
Qed.
Property ones_eq_impl_w_eq:
forall (w1: inw) ,
forall (w2: inw) ,
forall H_ones_eq: (forall i, ones w1 i = ones w2 i),
forall i,
forall H_i_ge_1: i > 0,
w1 i = w2 i.
Proof.
intros.
case_eq i.
intro H_i.
rewrite H_i in H_i_ge_1.
absurd (0 > 0); auto with arith.
intros i' H_i.
apply (plus_reg_l (w1 (S i')) (w2 (S i')) (ones w1 i')).
rewrite (H_ones_eq i') at 2.
generalize (H_ones_eq (S i')).
intros H_ones_eq_S_i'.
rewrite red_ones in H_ones_eq_S_i'.
rewrite plus_comm.
rewrite H_ones_eq_S_i'.
rewrite red_ones.
rewrite plus_comm.
reflexivity.
Qed.
Property inw_of_ones_ones_w_eq_w:
forall w: inw,
forall H_wf_w: well_formed_inw w,
forall i,
inw_of_ones (ones w) i = w i.
Proof.
induction i.
simpl.
rewrite H_wf_w.
reflexivity.
simpl.
omega.
Qed.
Property ones_inw_of_ones_ones_w_eq_ones_w:
forall ones_w: nat -> nat,
forall H_wf_ones: well_formed_ones ones_w,
forall i,
ones (inw_of_ones ones_w) i = ones_w i.
Proof.
induction i.
simpl.
destruct H_wf_ones.
rewrite H.
reflexivity.
simpl.
rewrite IHi.
rewrite plus_comm.
apply le_plus_minus_r.
unfold well_formed_ones in H_wf_ones.
destruct H_wf_ones.
apply (H0 i).
Qed.
End ones_properties.
Section delay_properties.
Property delay_d_w_eq_w:
forall w: inw,
forall d,
forall i,
(delay d w) (i + d) = w i.
Proof.
intros.
unfold delay.
replace (i + d - d) with i; auto.
omega.
Qed.
Property delay_d_w_eq_false:
forall w: inw,
forall H_wf: well_formed_inw w,
forall d,
forall i,
forall H_i_le_d: i <= d,
(delay d w) i = 0.
Proof.
intros.
unfold delay.
assert (H_aux: i - d = 0).
omega.
rewrite H_aux; clear H_aux.
assumption.
Qed.
Property ones_delay_d_w_eq_0:
forall w: inw,
forall H_wf: well_formed_inw w,
forall d,
forall i,
forall H_i_le_d: i <= d,
ones (delay d w) i = 0.
Proof.
intros.
generalize (delay_d_w_eq_false H_wf H_i_le_d).
intro.
apply w_i'_eq_0_impl_ones_i_eq_0.
intros.
apply delay_d_w_eq_false; auto.
apply (le_trans i' i d); auto.
Qed.
Property ones_delay_d_w_eq_ones_w:
forall w: inw,
forall H_wf: well_formed_inw w,
forall d,
forall i,
ones (delay d w) (i + d) = ones w i.
Proof.
double induction d i.
replace (i + 0) with i; auto.
intros i' IHi.
simpl.
rewrite IHi.
unfold delay.
replace (S (i' + 0) - 0) with (S i'); auto.
omega.
intros d' IHd.
rewrite <- (IHd 0).
simpl.
repeat rewrite ones_delay_d_w_eq_0; auto.
unfold delay.
replace (S d' - S d') with 0; auto with arith.
rewrite H_wf.
trivial.
intros i' IH1 d' IH2.
replace (S i' + S d') with (S (i' + S d')); auto.
rewrite red_ones.
rewrite IH1; auto.
simpl.
unfold delay.
replace (S (i' + S d') - S d') with (S i'); auto.
omega.
Qed.
Property ones_delay_d_w_i_eq_ones_w_i_m_d:
forall w: inw,
forall H_wf: well_formed_inw w,
forall d,
forall i,
ones (delay d w) i = ones w (i - d).
Proof.
intros.
elim (le_lt_dec i d).
intro H_i_le_d.
rewrite ones_delay_d_w_eq_0; auto.
replace (i - d) with 0;
try solve [ simpl; reflexivity ].
omega.
intro H_d_lt_i.
replace i with ((i - d) + d); try omega.
rewrite ones_delay_d_w_eq_ones_w; auto.
replace (i - d + d - d) with (i - d); try omega.
Qed.
End delay_properties.
Definition w_true :=
(fun i:nat =>
match i with
| 0 => 0
| _ => 1
end).
Definition w_false := (fun i:nat => 0).
Section true_and_false_properties.
Property w_true_well_formed:
well_formed_inw w_true.
Proof.
unfold well_formed_inw.
simpl.
reflexivity.
Qed.
Property w_false_well_formed:
well_formed_inw w_false.
Proof.
unfold well_formed_inw.
simpl.
reflexivity.
Qed.
Property w_false_well_formed_n:
well_formed_inw_n w_false 0.
Proof.
split; try solve [apply w_false_well_formed].
intro.
compute.
apply le_refl.
Qed.
Property ones_true_i_eq_i:
forall i, ones w_true i = i.
Proof.
induction i.
simpl.
reflexivity.
simpl.
rewrite IHi.
reflexivity.
Qed.
Property ones_false_i_eq_0:
forall i, ones w_false i = 0.
Proof.
induction i.
simpl.
reflexivity.
simpl.
rewrite IHi.
reflexivity.
Qed.
End true_and_false_properties.
Section on_properties.
Property on_gt_0_impl_w1_gt_0:
forall (w1:inw) (w2:inw) i,
forall (H_on_gt_0: on w1 w2 i > 0),
w1 i > 0.
Proof.
intros.
unfold on in H_on_gt_0.
case_eq (w1 i).
intro H_w1.
rewrite H_w1 in H_on_gt_0.
simpl in H_on_gt_0.
congruence.
intros n H_w1.
auto with arith.
Qed.
Theorem ones_on_def:
forall w1 w2 :inw,
forall i,
ones (on w1 w2) i = ones w2 (ones w1 i).
Proof.
intros.
induction i.
simpl.
trivial.
simpl.
case_eq (w1 (S i)).
intro H_w1.
simpl.
rewrite <- IHi.
unfold on at 1.
rewrite H_w1.
simpl.
reflexivity.
intros n H_w1.
rewrite IHi.
simpl.
unfold on.
rewrite H_w1.
simpl.
rewrite <- plus_assoc.
assert (plus_eq_compat_l: forall n m p : nat, n = m -> p + n = p + m).
intros; omega.
apply plus_eq_compat_l.
clear H_w1.
induction n.
simpl.
reflexivity.
simpl.
rewrite <- plus_assoc.
apply plus_eq_compat_l.
assumption.
Qed.
Property on_wf_compat:
forall (w1: inw) (H_wf1: well_formed_inw w1),
forall (w2: inw),
well_formed_inw (on w1 w2).
Proof.
intros.
unfold well_formed_inw.
unfold on.
rewrite H_wf1.
trivial.
Qed.
Property on_w_true:
forall w: inw,
forall i,
forall H_i_ge_1: i > 0,
(on w w_true) i = w i.
Proof.
intros.
apply ones_eq_impl_w_eq; auto.
clear H_i_ge_1 i.
intros.
rewrite ones_on_def.
induction (ones w i).
simpl.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.
Property on_true_w:
forall w: inw,
forall i,
forall H_i_ge_1: i > 0,
(on w_true w) i = w i.
Proof.
intros.
apply ones_eq_impl_w_eq; auto.
clear H_i_ge_1 i.
intros.
rewrite ones_on_def.
rewrite ones_true_i_eq_i.
reflexivity.
Qed.
Property on_w_false:
forall w: inw,
forall i,
forall H_i_ge_1: i > 0,
(on w w_false) i = w_false i.
Proof.
intros.
apply ones_eq_impl_w_eq; auto.
intros.
rewrite ones_on_def.
repeat rewrite ones_false_i_eq_0.
reflexivity.
Qed.
Property on_false_w:
forall w: inw,
forall i,
forall H_i_ge_1: i > 0,
(on w_false w) i = w_false i.
Proof.
intros.
apply ones_eq_impl_w_eq; auto.
Qed.
Property on_assoc_aux:
forall w1 w2 w3: inw,
forall i,
forall H_i_ge_1: i > 0,
(on (on w1 w2) w3) i = (on w1 (on w2 w3)) i.
Proof.
intros.
apply ones_eq_impl_w_eq; auto.
intro.
repeat rewrite ones_on_def.
reflexivity.
Qed.
End on_properties.
Section prec_properties.
Lemma prec_refl:
forall w: inw,
prec w w.
Proof.
intros.
unfold prec.
intros.
unfold ge.
apply le_refl.
Qed.
Lemma prec_trans:
forall w1 w2 w3: inw,
forall H_prec_w1_w2: prec w1 w2,
forall H_prec_w2_w3: prec w2 w3,
prec w1 w3.
Proof.
intros.
unfold prec.
intros.
unfold ge.
apply
(le_trans
(ones w3 i)
(ones w2 i)
(ones w1 i)).
apply H_prec_w2_w3.
apply H_prec_w1_w2.
Qed.
Lemma prec_antisym:
forall (w1: inw) ,
forall (w2: inw) ,
forall H_prec_w1_w2: prec w1 w2,
forall H_prec_w2_w1: prec w2 w1,
forall i,
forall H_i_ge_1: i > 0,
w1 i = w2 i.
Proof.
intros w1 w2 H_prec_w1_w2 H_prec_w2_w1.
apply ones_eq_impl_w_eq; auto.
intro.
apply le_antisym.
apply H_prec_w2_w1.
apply H_prec_w1_w2.
Qed.
Lemma on_prec_compat:
forall w1 w2 w1' w2': inw,
forall H_prec_w1_w2: prec w1 w2,
forall H_prec_w1'_w2': prec w1' w2',
prec (on w1 w1') (on w2 w2').
Proof.
intros.
unfold prec.
intros.
repeat rewrite ones_on_def.
apply
(le_trans
(ones w2' (ones w2 i))
(ones w2' (ones w1 i))
(ones w1' (ones w1 i))).
apply ones_increasing.
apply H_prec_w1_w2.
apply H_prec_w1'_w2'.
Qed.
Property supremum_well_formed:
forall w1 w2: inw,
well_formed_inw (supremum w1 w2).
Proof.
intros.
unfold well_formed_inw.
simpl.
trivial.
Qed.
Property infimum_well_formed:
forall w1 w2: inw,
well_formed_inw (infimum w1 w2).
Proof.
intros.
unfold well_formed_inw.
simpl.
trivial.
Qed.
Property ones_supremum_well_formed:
forall w1 w2: inw,
well_formed_ones (ones_supremum w1 w2).
Proof.
unfold well_formed_ones.
split.
unfold ones_supremum.
simpl.
reflexivity.
intros.
case_eq (w1 (S i));
case_eq (w2 (S i)).
intros H_w2 H_w1.
unfold ones_supremum.
simpl.
rewrite H_w1, H_w2.
simpl.
apply le_refl.
intros n H_w2 H_w1.
unfold ones_supremum.
simpl.
rewrite H_w1, H_w2.
simpl.
elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp;
intro H_cmp;
repeat rewrite Min.min_l; try omega.
intro H_cmp.
rewrite Min.min_r; try omega.
elim (lt_eq_lt_dec (ones w1 i) (S (n + ones w2 i))).
intro H_tmp.
elim H_tmp; clear H_tmp;
intro H_cmp';
repeat rewrite Min.min_l; try omega.
intro H_cmp';
repeat rewrite Min.min_r; try omega.
intros H_w2 n H_w1.
unfold ones_supremum.
simpl.
rewrite H_w2, H_w1.
elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp.
intro H_cmp.
rewrite Min.min_l; try omega.
elim (lt_eq_lt_dec (S n + ones w1 i) (ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp;
intro H_cmp';
repeat rewrite Min.min_l; try omega.
intro H_cmp';
repeat rewrite Min.min_r; try omega.
intro H_cmp.
repeat rewrite Min.min_r; try omega.
intro H_cmp.
repeat rewrite Min.min_r; try omega.
intros n2 H_w2 n1 H_w1.
unfold ones_supremum.
simpl.
rewrite H_w1, H_w2.
elim (lt_eq_lt_dec (ones w1 i) (ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp.
intro H_cmp.
rewrite Min.min_l; try omega.
elim (lt_eq_lt_dec (S n1 + ones w1 i) (S n2 + ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp;
intro H_cmp';
repeat rewrite Min.min_l; try omega.
intro H_cmp';
repeat rewrite Min.min_r; try omega.
intro H_cmp.
rewrite Min.min_l; try omega.
elim (lt_eq_lt_dec (S n1 + ones w1 i) (S n2 + ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp;
intro H_cmp';
repeat rewrite Min.min_l; try omega.
intro H_cmp';
repeat rewrite Min.min_r; try omega.
intro H_cmp.
rewrite Min.min_r; try omega.
elim (lt_eq_lt_dec (S n1 + ones w1 i) (S n2 + ones w2 i)).
intro H_tmp.
elim H_tmp; clear H_tmp;
intro H_cmp';
repeat rewrite Min.min_l; try omega.
intro H_cmp';
repeat rewrite Min.min_r; try omega.
Qed.
End prec_properties.
Section sync_properties.
Property sync_sym:
forall w1 w2: inw,
sync w1 w2 -> sync w2 w1.
Proof.
intros w1 w2 H_sync.
unfold sync.
elim H_sync.
intros b1 H_tmp.
elim H_tmp; clear H_tmp.
intros b2 H_cmp.
exists (-b2)%Z.
exists (-b1)%Z.
intros.
destruct (H_cmp i); auto.
split; omega.
Qed.
Property sync_refl:
forall w: inw,
sync w w.
Proof.
intros.
unfold sync.
exists 0.
exists 0.
intros.
split; auto with zarith.
apply Zle_minus_le_0.
apply Zle_refl.
Qed.
Property sync_trans:
forall w1 w2 w3: inw,
forall H_sync12: sync w1 w2,
forall H_sync23: sync w2 w3,
sync w1 w3.
Proof.
intros.
elim H_sync12.
intros b1 H_tmp.
elim H_tmp; clear H_tmp.
intros b2 H_cmp12.
elim H_sync23.
intros b1' H_tmp.
elim H_tmp; clear H_tmp.
intros b2' H_cmp23.
unfold sync.
exists (b1 + b1')%Z.
exists (b2 + b2')%Z.
intros.
destruct (H_cmp12 i); auto.
destruct (H_cmp23 i); auto.
assert (H_aux:
(ones w3 i - ones w1 i =
(ones w3 i - ones w2 i) + (ones w2 i - ones w1 i))%Z).
omega.
rewrite H_aux; clear H_aux.
split; omega.
Qed.
End sync_properties.
Section adaptability_properties.
End adaptability_properties.