Library ibw_aux
Set Implicit Arguments.
Require Import Bool.
Require Import Omega.
Require Import misc.
Require Import ibw_def.
Definition well_formed_ibw (w:ibw) := w 0 = false.
Definition delay (d:nat) (w:ibw) : ibw :=
fun i => w (i - d).
Definition non_null_stream (w: ibw) :=
forall i: nat, exists j: nat, j > i /\ w j = true.
Inductive index_of_one (w: ibw) (j: nat) (i: nat) : Prop :=
iof: ones w i = j -> (forall i', ones w i' = j -> i <= i') -> index_of_one w j i.
Property index_of_one_functional:
forall w j i i',
index_of_one w j i -> index_of_one w j i' -> i = i'.
Proof.
intros.
inversion H.
inversion H0.
apply le_antisym;
[ apply H2 | apply H4 ]; assumption.
Qed.
Definition well_formed_ones (ones_w: nat -> nat) :=
ones_w 0 = 0
/\
forall i, (ones_w (S i) = S (ones_w i) \/ ones_w (S i) = ones_w i).
Section ones_properties.
Property ones_impl_well_formed_ones:
forall w: ibw,
well_formed_ones (ones w).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (w (S i)).
intro H_w.
left.
simpl.
reflexivity.
intro H_w.
right.
simpl.
reflexivity.
Qed.
Property red_ones:
forall w: ibw,
forall i,
ones w i =
match i with
| 0 => 0
| S i' =>
let w_i := if w i then 1 else 0 in
w_i + ones w i'
end.
Proof.
intros.
induction i.
simpl.
reflexivity.
simpl.
reflexivity.
Qed.
Property ones_S_i_eq_S_ones_i:
forall (w:ibw),
forall i,
forall H_w_S_i_eq_1: w (S i) = true,
ones w (S i) = 1 + ones w i.
Proof.
intros.
simpl.
rewrite H_w_S_i_eq_1.
trivial.
Qed.
Property ones_S_i_eq_ones_i:
forall (w:ibw) i,
forall H_w_S_i_eq_0: w (S i) = false,
ones w (S i) = ones w i.
Proof.
intros.
simpl.
rewrite H_w_S_i_eq_0.
trivial.
Qed.
Property ones_pred_i_eq_pred_ones_i:
forall (w:ibw),
forall i,
forall H_w_S_i_eq_1: w i = true,
ones w (pred i) = pred (ones w i).
Proof.
intros.
case_eq i.
compute.
reflexivity.
intros i' H_i.
simpl.
rewrite <- H_i.
rewrite H_w_S_i_eq_1.
simpl.
reflexivity.
Qed.
Property ones_pred_i_eq_ones_i:
forall (w:ibw),
forall i,
forall H_w_S_i_eq_1: w i = false,
ones w (pred i) = ones w i.
Proof.
intros.
case_eq i.
compute.
reflexivity.
intros i' H_i.
simpl.
rewrite <- H_i.
rewrite H_w_S_i_eq_1.
simpl.
reflexivity.
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_one:
forall (w:ibw) i,
ones w i <= ones w (S i).
Proof.
intros.
simpl.
eapply le_prop_aux.
trivial.
Qed.
Property ones_increasing_x:
forall (w:ibw) 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.
eapply le_prop_aux.
trivial.
Qed.
Property ones_increasing:
forall (w:ibw) 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_increasing_rev:
forall (w:ibw) 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 ones_i_le_i_aux:
forall w:ibw,
forall i,
ones w i <= i.
Proof.
intros.
induction i.
simpl.
trivial.
case_eq (w (S i)).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
simpl.
auto with arith.
intro H_w.
rewrite ones_S_i_eq_ones_i; trivial.
auto with arith.
Qed.
Property w_i_eq_true_impl_ones_pos:
forall w:ibw,
forall i,
forall H_i_ge_1: i > 0,
forall H_w: w i = true,
ones w i > 0.
Proof.
intros.
case_eq i.
intro H_i.
rewrite H_i in H_i_ge_1.
absurd (0 > 0); auto with arith.
intros n H_i.
simpl.
rewrite H_i in H_w.
rewrite H_w.
auto with arith.
Qed.
Property ones_eq_0_impl_w_eq_false:
forall w: ibw,
forall i,
forall H_i_ge_1: i > 0,
forall H_ones_eq_0: ones w i = 0,
w i = false.
Proof.
intros.
case_eq i.
intros H_i.
rewrite H_i in H_i_ge_1.
absurd (0 > 0); auto with arith.
intros i' H_i.
rewrite H_i in H_ones_eq_0.
clear H_i H_i_ge_1 i.
induction i'.
simpl in H_ones_eq_0.
case_eq (w 1).
intro H_w.
rewrite H_w in H_ones_eq_0.
simpl in H_ones_eq_0.
congruence.
trivial.
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.
simpl in H_ones_eq_0.
case_eq (w (S (S i'))).
intro H_w.
rewrite H_w in H_ones_eq_0.
simpl in H_ones_eq_0.
congruence.
trivial.
Qed.
Property ones_i_eq_0_impl_w_i'_eq_false:
forall w: ibw,
forall i,
forall H_ones_eq_0: ones w i = 0,
forall i',
forall H_i'_ge_1: i' > 0,
forall H_i'_le_i: i' <= i,
w i' = false.
Proof.
intros.
apply ones_eq_0_impl_w_eq_false; 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_false_impl_ones_i_eq_0:
forall w: ibw,
forall i,
forall H_w: (forall i', forall H_i'_le_i: i' <= i, w i' = false),
ones w i = 0.
Proof.
induction i.
intros.
simpl.
trivial.
intros.
rewrite ones_S_i_eq_ones_i.
rewrite IHi; auto.
apply H_w.
apply le_refl.
Qed.
Property non_null_impl_ones_i_ge_j:
forall w: ibw,
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_S_ones_i; auto.
simpl.
unfold ge.
apply le_n_S.
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: ibw,
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.
Lemma ones_continuous:
forall w: ibw,
forall k i,
forall H_k_le_ones: k <= ones w i,
exists j, j <= i /\ ones w j = k.
Proof.
induction i.
simpl; intro; exists 0; split; simpl; try omega.
case_eq (w (S i)); intro Hw; simpl; rewrite Hw; simpl.
intro Hlt; inversion Hlt.
exists (S i); split; auto. simpl; rewrite Hw; reflexivity.
destruct (IHi H0) as [j [Hj1 Hj2]].
exists j; split; omega.
intro H; destruct (IHi H) as [j [Hj1 Hj2]].
exists j; split; auto.
Qed.
Property non_null_impl_ones_i_eq_j:
forall w: ibw,
forall H_non_null_stream: non_null_stream w,
forall j,
exists i,
ones w i = j.
Proof.
intros.
elim (non_null_impl_ones_i_ge_j H_non_null_stream j).
intros i H_ones_ge_j.
unfold ge in H_ones_ge_j.
elim (ones_continuous w i H_ones_ge_j).
intros i_cc H_tmp.
destruct H_tmp.
exists i_cc.
assumption.
Qed.
Property w_eq_impl_ones_eq:
forall w1 w2: ibw,
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: ibw) ,
forall (w2: ibw) ,
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.
clear H_i H_i_ge_1 i.
case_eq (w1 (S i'));
case_eq (w2 (S i')).
trivial.
intros H_w2 H_w1.
absurd (ones w1 (S i') = ones w2 (S i')); auto.
simpl.
rewrite H_w1, H_w2.
simpl.
rewrite (H_ones_eq i');
auto.
intros H_w2 H_w1.
absurd (ones w1 (S i') = ones w2 (S i')); auto.
simpl.
rewrite H_w1, H_w2.
simpl.
rewrite (H_ones_eq i').
auto.
trivial.
Qed.
Property ibw_of_ones_ones_w_eq_w:
forall w: ibw,
forall i,
forall H_i_ge_1: i > 0,
ibw_of_ones (ones w) i = w i.
Proof.
induction i.
intro H_i_ge_1.
absurd (0 > 0); auto with arith.
simpl.
case_eq (w (S i)).
intro H_w.
change (1 + ones w i) with (S (ones w i)).
rewrite S_n_nbeq_n.
simpl.
reflexivity.
intro H_w.
simpl.
rewrite <- beq_nat_refl.
simpl.
reflexivity.
Qed.
Property ones_ibw_of_ones_ones_w_eq_ones_w:
forall ones_w: nat -> nat,
forall H_wf_ones: well_formed_ones ones_w,
forall i,
ones (ibw_of_ones ones_w) i = ones_w i.
Proof.
induction i.
simpl.
destruct H_wf_ones.
rewrite H.
reflexivity.
simpl.
rewrite IHi.
destruct H_wf_ones.
elim (H0 i).
intro H_ones.
rewrite H_ones.
rewrite S_n_nbeq_n.
simpl.
reflexivity.
intro H_ones.
rewrite H_ones.
rewrite <- beq_nat_refl.
simpl.
reflexivity.
Qed.
End ones_properties.
Fixpoint zeros (w:ibw) (i:nat) { struct i } :=
match i with
| 0 => 0
| S i' =>
let not_w_i := if w i then 0 else 1 in
not_w_i + zeros w i'
end.
Theorem zeros_def:
forall w: ibw,
forall i,
zeros w i = i - ones w i.
Proof.
intros.
induction i.
simpl.
reflexivity.
case_eq (w (S i)).
intro H_w_S_i.
simpl.
rewrite H_w_S_i.
simpl.
exact IHi.
intro H_w_S_i.
simpl.
rewrite H_w_S_i.
simpl.
case_eq (ones w i).
intro H_ones.
rewrite H_ones in IHi.
replace (i - 0) with i in IHi.
rewrite <- IHi at 2.
reflexivity.
auto with arith.
intros n H_ones.
rewrite H_ones in IHi.
assert (H_cc: S (zeros w i) = S (i - S n)).
auto with arith.
rewrite minus_Sn_m in H_cc;
try solve [ rewrite <- H_ones;
apply ones_i_le_i_aux ].
change ( S i - S n) with (i - n) in H_cc.
exact H_cc.
Qed.
Section delay_properties.
Property delay_d_w_eq_w:
forall w: ibw,
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: ibw,
forall H_wf: well_formed_ibw w,
forall d,
forall i,
forall H_i_le_d: i <= d,
(delay d w) i = false.
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: ibw,
forall H_wf: well_formed_ibw 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_false_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: ibw,
forall H_wf: well_formed_ibw 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: ibw,
forall H_wf: well_formed_ibw 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.
Property ones_w_le_ones_delay_d_w_p_d:
forall w: ibw,
forall H_wf: well_formed_ibw w,
forall d,
forall i,
ones w i <= ones (delay d w) i + d.
Proof.
double induction d i.
simpl.
apply le_refl.
intros i' IH.
rewrite <- (ones_delay_d_w_eq_ones_w H_wf 0 (S i')).
replace (S i' + 0) with (S i'); auto.
replace (ones (delay 0 w) (S i') + 0) with (ones (delay 0 w) (S i')); auto.
intros d' IH.
simpl.
auto with arith.
intros i' IH1 d' IH2.
apply
(le_trans
(ones w (S i'))
(ones (delay d' w) (S i') + d')
(ones (delay (S d') w) (S i') + S d'));
auto.
elim (le_lt_dec (S i') d').
intro H_i_le_d.
repeat rewrite ones_delay_d_w_eq_0; auto.
simpl.
auto.
intro H_d_lt_i.
assert (H_aux: S i' = (S i' - d') + d').
omega.
auto with arith.
rewrite H_aux at 1; clear H_aux.
rewrite ones_delay_d_w_eq_ones_w; auto.
assert (H_aux: S i' = (S i' - S d') + S d').
omega.
auto with arith.
rewrite H_aux at 2; clear H_aux.
rewrite ones_delay_d_w_eq_ones_w; auto.
rewrite <- minus_Sn_m; auto with arith.
replace (S i' - S d') with (i' - d'); auto.
replace (ones w (i' - d') + S d')
with (S (ones w (i' - d') + d')); auto.
case_eq (w (S (i' - d'))).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
intro H_w.
rewrite ones_S_i_eq_ones_i; auto.
Qed.
Property ones_w_m_d_le_ones_delay_d_w:
forall w: ibw,
forall H_wf: well_formed_ibw w,
forall d: nat,
forall i: nat,
(ones w i - d <= ones (delay d w) i)%Z.
Proof.
intros.
unfold Zminus.
apply <- Zle_plus_swap.
unfold Zminus.
rewrite Zopp_involutive.
generalize (ones_w_le_ones_delay_d_w_p_d H_wf d i).
intro.
auto with zarith.
Qed.
End delay_properties.
Definition w_true :=
(fun i:nat =>
match i with
| 0 => false
| _ => true
end).
Definition w_false := (fun i:nat => false).
Section true_and_false_properties.
Property w_true_well_formed:
well_formed_ibw w_true.
Proof.
unfold well_formed_ibw.
simpl.
reflexivity.
Qed.
Property w_false_well_formed:
well_formed_ibw w_false.
Proof.
unfold well_formed_ibw.
simpl.
reflexivity.
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 not_properties.
Theorem ones_not_def:
forall (w: ibw) i,
ones (not w) i = i - ones w i.
Proof.
intros.
induction i.
simpl.
trivial.
case_eq (w (S i)).
intro H_w.
assert (H_not_w: not w (S i) = false).
unfold not.
rewrite H_w.
simpl.
trivial.
rewrite ones_S_i_eq_ones_i; auto.
rewrite ones_S_i_eq_S_ones_i; auto.
intro H_w.
assert (H_not_w: not w (S i) = true).
unfold not.
rewrite H_w.
simpl.
trivial.
rewrite ones_S_i_eq_S_ones_i; auto.
rewrite ones_S_i_eq_ones_i; auto.
rewrite IHi.
assert (H_aux: 1 + (i - ones w i) = S (i - ones w i)).
simpl.
trivial.
rewrite H_aux; clear H_aux.
generalize (ones_i_le_i_aux w i).
intro H_f'_i_le_i.
rewrite minus_Sn_m; auto.
Qed.
Property not_wf_compat:
forall (w: ibw),
well_formed_ibw (not w).
Proof.
intros.
unfold well_formed_ibw.
simpl.
trivial.
Qed.
End not_properties.
Section on_properties.
Property on_eq_1_impl_w1_eq_1:
forall (w1:ibw) (w2:ibw) i,
forall (H_on_eq_1: on w1 w2 i = true),
w1 i = true.
Proof.
intros.
unfold on in H_on_eq_1.
case_eq (w1 i).
trivial.
intro.
rewrite H in H_on_eq_1.
congruence.
Qed.
Property on_eq_1_impl_w2_eq_1:
forall (w1:ibw) (w2:ibw) i,
forall (H_on_eq_1: on w1 w2 i = true),
w2 (ones w1 i) = true.
Proof.
intros.
generalize (on_eq_1_impl_w1_eq_1 w1 w2 i H_on_eq_1).
intro H_w1_eq_1.
unfold on in H_on_eq_1.
rewrite H_w1_eq_1 in H_on_eq_1.
trivial.
Qed.
Property on_eq_0_and_w1_eq_1_impl_w2_eq_0:
forall (w1:ibw) (w2:ibw) i,
forall (H_on_eq_0: on w1 w2 i = false),
forall (H_w1_eq_1: w1 i = true),
w2 (ones w1 i) = false.
Proof.
intros.
unfold on in H_on_eq_0.
rewrite H_w1_eq_1 in H_on_eq_0.
trivial.
Qed.
Theorem ones_on_def:
forall w1 w2 :ibw,
forall i,
ones (on w1 w2) i = ones w2 (ones w1 i).
Proof.
intros.
induction i.
simpl.
trivial.
case_eq (on w1 w2 (S i)).
intro H_on_eq_1.
generalize (on_eq_1_impl_w1_eq_1 w1 w2 (S i) H_on_eq_1).
intro H_w1_eq_1.
generalize (on_eq_1_impl_w2_eq_1 w1 w2 (S i) H_on_eq_1).
intro H_w2_eq_1.
simpl.
rewrite H_w1_eq_1.
rewrite H_on_eq_1.
unfold ones at 2.
simpl.
simpl in IHi.
rewrite IHi.
apply trans_eq with (1+ones w2 (ones w1 i)); auto with arith.
rewrite <- ones_S_i_eq_S_ones_i with w2 (ones w1 i); auto.
rewrite ones_S_i_eq_S_ones_i in H_w2_eq_1.
simpl in H_w2_eq_1; assumption.
exact H_w1_eq_1.
intro H_on_eq_0.
simpl.
rewrite H_on_eq_0.
simpl.
simpl in IHi.
rewrite IHi.
case_eq (w1 (S i)).
intro H_w1_eq_1.
generalize (on_eq_0_and_w1_eq_1_impl_w2_eq_0 w1 w2 (S i) H_on_eq_0 H_w1_eq_1).
intro H_w2_eq_0.
simpl in H_w2_eq_0.
rewrite H_w1_eq_1 in H_w2_eq_0.
simpl in H_w2_eq_0.
simpl.
case_eq (ones w1 i);
intros;
rewrite H in H_w2_eq_0;
simpl;
rewrite H_w2_eq_0;
trivial.
intro H_w1_eq_0.
trivial.
Qed.
Property ones_on_le_ones_w1:
forall w1 w2 i, ones (on w1 w2) i <= ones w1 i.
Proof.
intros.
induction i.
unfold on.
simpl.
case_eq (w1 0).
intro H_w1.
simpl.
case_eq (w2 0).
trivial.
auto with arith.
trivial.
simpl.
case_eq (w1 (S i)).
intro H_w1.
unfold on at 1.
simpl.
rewrite H_w1.
simpl.
case_eq (w2 (S (ones w1 i))).
intro H_w2.
simpl.
auto with arith.
intro H_w2.
simpl.
auto with arith.
intro H_w1.
unfold on at 1.
rewrite H_w1.
simpl.
trivial.
Qed.
Property ones_on_le_ones_w2:
forall (w1:ibw) (w2:ibw) i, ones (on w1 w2) i <= ones w2 i.
Proof.
intros.
rewrite ones_on_def.
eapply ones_increasing.
eapply ones_i_le_i_aux.
Qed.
Lemma on_le_i:
forall (w1:ibw) (w2:ibw) i,
forall (H_on: on w1 w2 i = true),
(ones (on w1 w2) i <= i)%nat.
Proof.
intros.
eapply ones_i_le_i_aux.
Qed.
Property on_wf_compat:
forall (w1: ibw) (H_wf1: well_formed_ibw w1),
forall (w2: ibw),
well_formed_ibw (on w1 w2).
Proof.
intros.
unfold well_formed_ibw.
unfold on.
rewrite H_wf1.
trivial.
Qed.
Property on_w_true:
forall w: ibw,
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: ibw,
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: ibw,
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.
clear H_i_ge_1 i.
intros.
rewrite ones_on_def.
repeat rewrite ones_false_i_eq_0.
reflexivity.
Qed.
Property on_false_w:
forall w: ibw,
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: ibw,
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: ibw,
prec w w.
Proof.
intros.
unfold prec.
intros.
unfold ge.
apply le_refl.
Qed.
Lemma prec_trans:
forall w1 w2 w3: ibw,
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: ibw) ,
forall (w2: ibw) ,
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 i H_i_ge_1.
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': ibw,
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.
Lemma on_prec_reg_l:
forall w1 w2 w3: ibw,
forall H_non_null: non_null_stream w3,
forall H_prec_on: prec (on w3 w1) (on w3 w2),
prec w1 w2.
Proof.
unfold prec.
intros.
elim (non_null_impl_ones_i_eq_j H_non_null i).
intros i' H_i.
pose (H_cc:= H_prec_on i').
repeat rewrite (ones_on_def ) in H_cc.
rewrite H_i in H_cc.
exact H_cc.
Qed.
Property supremum_well_formed:
forall w1 w2: ibw,
well_formed_ibw (supremum w1 w2).
Proof.
intros.
unfold well_formed_ibw.
simpl.
trivial.
Qed.
Property infimum_well_formed:
forall w1 w2: ibw,
well_formed_ibw (infimum w1 w2).
Proof.
intros.
unfold well_formed_ibw.
simpl.
trivial.
Qed.
Property ones_supremum_well_formed:
forall w1 w2: ibw,
well_formed_ones (ones_supremum w1 w2).
Proof.
unfold well_formed_ones.
split.
unfold ones_supremum.
simpl.
reflexivity.
intros.
case_eq (w1 (S i)); intro H_w1;
case_eq (w2 (S i)); intro H_w2.
left.
unfold ones_supremum.
simpl.
rewrite H_w1, H_w2.
simpl.
reflexivity.
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.
left.
repeat rewrite Min.min_l; try omega.
intro H_cmp.
right.
repeat rewrite Min.min_r; try omega.
intro H_cmp.
right.
repeat rewrite Min.min_r; try omega.
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.
right.
repeat rewrite Min.min_l; try omega.
intro H_cmp.
right.
repeat rewrite Min.min_l; try omega.
intro H_cmp.
left.
repeat rewrite Min.min_r; try omega.
right.
unfold ones_supremum.
simpl.
rewrite H_w1, H_w2.
simpl.
reflexivity.
Qed.
Property ones_infimum_well_formed:
forall w1 w2: ibw,
well_formed_ones (ones_infimum w1 w2).
Proof.
unfold well_formed_ones.
split.
unfold ones_infimum.
simpl.
reflexivity.
intros.
case_eq (w1 (S i)); intro H_w1;
case_eq (w2 (S i)); intro H_w2.
left.
unfold ones_infimum.
simpl.
rewrite H_w1, H_w2.
simpl.
reflexivity.
unfold ones_infimum.
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.
right.
repeat rewrite Max.max_r; try omega.
intro H_cmp.
left.
repeat rewrite Max.max_l; try omega.
intro H_cmp.
left.
repeat rewrite Max.max_l; try omega.
unfold ones_infimum.
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.
left.
repeat rewrite Max.max_r; try omega.
intro H_cmp.
left.
repeat rewrite Max.max_r; try omega.
intro H_cmp.
right.
repeat rewrite Max.max_l; try omega.
right.
unfold ones_infimum.
simpl.
rewrite H_w1, H_w2.
simpl.
reflexivity.
Qed.
Property ones_supremum_correctness:
forall w1 w2: ibw,
forall i,
ones (supremum w1 w2) i = (ones_supremum w1 w2) i.
Proof.
induction i.
unfold ones_supremum.
simpl.
reflexivity.
simpl.
rewrite IHi.
case_eq (beq_nat (ones_supremum w1 w2 (S i)) (ones_supremum w1 w2 i)).
intro H_cmp.
simpl.
rewrite (beq_nat_true _ _ H_cmp).
reflexivity.
intro H_cmp.
simpl.
elim (ones_supremum_well_formed w1 w2).
intros H_ones_0 H_tmp.
elim (H_tmp i); clear H_tmp.
intro H_ones.
rewrite H_ones.
reflexivity.
intro H_ones.
absurd (ones_supremum w1 w2 (S i) = ones_supremum w1 w2 i);
auto.
apply beq_nat_false.
assumption.
Qed.
Property ones_infimum_correctness:
forall w1 w2: ibw,
forall i,
ones (infimum w1 w2) i = (ones_infimum w1 w2) i.
Proof.
induction i.
unfold ones_infimum.
simpl.
reflexivity.
simpl.
rewrite IHi.
case_eq (beq_nat (ones_infimum w1 w2 (S i)) (ones_infimum w1 w2 i)).
intro H_cmp.
simpl.
rewrite (beq_nat_true _ _ H_cmp).
reflexivity.
intro H_cmp.
simpl.
elim (ones_infimum_well_formed w1 w2).
intros H_ones_0 H_tmp.
elim (H_tmp i); clear H_tmp.
intro H_ones.
rewrite H_ones.
reflexivity.
intro H_ones.
absurd (ones_infimum w1 w2 (S i) = ones_infimum w1 w2 i);
auto.
apply beq_nat_false.
assumption.
Qed.
Property prec_w1_supremum:
forall w1 w2: ibw,
prec w1 (supremum w1 w2).
Proof.
intros.
unfold prec.
intros.
rewrite ones_supremum_correctness.
unfold ones_supremum.
unfold ge.
apply Min.le_min_l.
Qed.
Property prec_w2_supremum:
forall w1 w2: ibw,
prec w2 (supremum w1 w2).
Proof.
intros.
unfold prec.
intros.
rewrite ones_supremum_correctness.
unfold ones_supremum.
unfold ge.
apply Min.le_min_r.
Qed.
Property prec_infimum_w1:
forall w1 w2: ibw,
prec (infimum w1 w2) w1.
Proof.
intros.
unfold prec.
intros.
rewrite ones_infimum_correctness.
unfold ones_infimum.
unfold ge.
apply Max.le_max_l.
Qed.
Property prec_infimum_w2:
forall w1 w2: ibw,
prec (infimum w1 w2) w2.
Proof.
intros.
unfold prec.
intros.
rewrite ones_infimum_correctness.
unfold ones_infimum.
unfold ge.
apply Max.le_max_r.
Qed.
Property on_supremum_distr_r:
forall (w1: ibw) ,
forall w2 w3: ibw,
forall i,
forall H_i_ge_1: i > 0,
on w1 (supremum w2 w3) i = supremum (on w1 w2) (on w1 w3) i.
Proof.
intros w1 w2 w3 i H_i_ge_1.
apply ones_eq_impl_w_eq; auto.
intros.
rewrite ones_on_def.
repeat rewrite ones_supremum_correctness.
unfold ones_supremum.
repeat rewrite ones_on_def.
reflexivity.
Qed.
Property on_supremum_distr_l:
forall w1 w2 w3: ibw,
forall i,
forall H_i_ge_1: i > 0,
on (supremum w1 w2) w3 i = supremum (on w1 w3) (on w2 w3) i.
Proof.
intros w1 w2 w3 i.
apply ones_eq_impl_w_eq; auto.
clear i.
intros.
rewrite ones_on_def.
repeat rewrite ones_supremum_correctness.
unfold ones_supremum.
repeat rewrite ones_on_def.
elim (le_ge_dec (ones w1 i) (ones w2 i)); intro H_cmp.
rewrite Min.min_l; auto.
symmetry.
apply Min.min_l.
apply ones_increasing.
exact H_cmp.
rewrite Min.min_r; auto.
symmetry.
apply Min.min_r.
apply ones_increasing.
exact H_cmp.
Qed.
Property on_infimum_distr_r:
forall (w1: ibw),
forall w2 w3: ibw,
forall i,
forall H_i_ge_1: i > 0,
on w1 (infimum w2 w3) i = infimum (on w1 w2) (on w1 w3) i.
Proof.
intros w1 w2 w3 i H_i_ge_1.
apply ones_eq_impl_w_eq; auto.
intros.
rewrite ones_on_def.
repeat rewrite ones_infimum_correctness.
unfold ones_infimum.
repeat rewrite ones_on_def.
reflexivity.
Qed.
Property on_infimum_distr_l:
forall w1 w2 w3: ibw,
forall i,
forall H_i_ge_1: i > 0,
on (infimum w1 w2) w3 i = infimum (on w1 w3) (on w2 w3) i.
Proof.
intros w1 w2 w3 i H_i_ge_1.
apply ones_eq_impl_w_eq; auto.
clear H_i_ge_1 i.
intros.
rewrite ones_on_def.
repeat rewrite ones_infimum_correctness.
unfold ones_infimum.
repeat rewrite ones_on_def.
elim (le_ge_dec (ones w1 i) (ones w2 i)); intro H_cmp.
rewrite Max.max_r; auto.
symmetry.
apply Max.max_r.
apply ones_increasing.
exact H_cmp.
rewrite Max.max_l; auto.
symmetry.
apply Max.max_l.
apply ones_increasing.
exact H_cmp.
Qed.
End prec_properties.
Definition sync_popl (w1 w2: ibw) : Prop :=
exists d1,
exists d2,
prec w1 (delay d2 w2)
/\
prec w2 (delay d1 w1).
Section sync_properties.
Property sync_popl_impl_sync:
forall w1: ibw,
forall H_wf_1: well_formed_ibw w1,
forall w2: ibw,
forall H_wf_2: well_formed_ibw w2,
forall H_sync: sync_popl w1 w2,
sync w1 w2.
Proof.
intros.
elim H_sync.
intros d1 H_tmp.
elim H_tmp; clear H_tmp.
intros d2 H_tmp.
elim H_tmp; clear H_tmp.
intros H_prec_w1_w2 H_prec_w2_w1.
unfold sync.
unfold prec in H_prec_w1_w2, H_prec_w2_w1.
exists (- d1)%Z.
exists d2.
intros.
split.
apply Zle_left_rev.
replace (ones w2 i - ones w1 i + - - d1)%Z
with (ones w2 i + - (ones w1 i - d1))%Z;
auto with zarith.
apply Zle_left.
apply
(Zle_trans
(ones w1 i - d1)%Z
(ones (delay d1 w1) i)%Z
(ones w2 i)%Z);
try solve [ apply inj_le;
apply H_prec_w2_w1 ].
apply ones_w_m_d_le_ones_delay_d_w; auto.
apply Zle_left_rev.
replace (d2 + - (ones w2 i - ones w1 i))%Z
with (ones w1 i + - (ones w2 i - d2))%Z;
auto with zarith.
apply Zle_left.
apply
(Zle_trans
(ones w2 i - d2)%Z
(ones (delay d2 w2) i)%Z
(ones w1 i)%Z);
try solve [ apply inj_le;
apply H_prec_w1_w2 ].
apply ones_w_m_d_le_ones_delay_d_w; auto.
Qed.
Property sync_sym:
forall w1 w2: ibw,
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: ibw,
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: ibw,
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.
Lemma on_sync_compat:
forall (w1: ibw),
forall (w2: ibw),
forall (w1': ibw) (H_wf1': well_formed_ibw w1'),
forall (w2': ibw) (H_wf2': well_formed_ibw w2'),
forall H_sync_w1_w2: sync w1 w2,
forall H_sync_w1'_w2': sync w1' w2',
sync (on w1 w1') (on w2 w2').
Proof.
intros.
elim H_sync_w1_w2.
intros b1 H_tmp.
elim H_tmp; clear H_tmp.
intros b2 H_b1_le_ones_diff_le_b2.
elim H_sync_w1'_w2'.
intros b1' H_tmp.
elim H_tmp; clear H_tmp.
intros b2' H_b1'_le_ones_diff_le_b2'.
unfold sync.
pose (m_min_0_b1:= Zabs_nat (Zmin 0 b1)).
pose (max_0_b2:= Zabs_nat (Zmax 0 b2)).
exists (- m_min_0_b1 + b1')%Z.
exists (max_0_b2 + b2')%Z.
intro.
repeat rewrite ones_on_def.
split.
apply
(Zle_trans
(- m_min_0_b1 + b1')%Z
(ones w2' (ones w1 i - m_min_0_b1) - ones w1' (ones w1 i))%Z
(ones w2' (ones w2 i) - ones w1' (ones w1 i))%Z).
apply
(Zle_trans
(- m_min_0_b1 + b1')%Z
(ones w2' (ones w1 i) - m_min_0_b1 - ones w1' (ones w1 i))%Z
(ones w2' (ones w1 i - m_min_0_b1) - ones w1' (ones w1 i))%Z).
destruct (H_b1'_le_ones_diff_le_b2' (ones w1 i)); auto.
replace (ones w2' (ones w1 i) - m_min_0_b1 - ones w1' (ones w1 i))%Z
with (- m_min_0_b1 + (ones w2' (ones w1 i) - ones w1' (ones w1 i)))%Z;
auto with zarith.
apply Zplus_le_compat; try solve [ apply Zle_refl ].
generalize (ones_w_m_d_le_ones_delay_d_w H_wf2' m_min_0_b1 (ones w1 i)).
rewrite ones_delay_d_w_i_eq_ones_w_i_m_d; auto.
unfold Zminus.
apply Zplus_le_compat_r.
apply inj_le.
apply ones_increasing.
apply inj_le_rev.
assert (H_cmp: (ones w1 i + b1 <= ones w2 i)%Z).
destruct (H_b1_le_ones_diff_le_b2 i).
apply Zle_0_minus_le.
replace (ones w2 i - (ones w1 i + b1))%Z
with (ones w2 i - ones w1 i + - b1)%Z; auto with zarith.
unfold m_min_0_b1.
elim (Zmin_spec 0 b1).
intro H_tmp.
elim H_tmp; clear H_tmp.
intros H_0_le_b1 H_min.
rewrite H_min.
simpl.
replace (ones w1 i - 0)%nat with (ones w1 i); auto with arith.
apply (Zle_trans (ones w1 i) (ones w1 i + b1) (ones w2 i));
try omega.
intro H_tmp.
elim H_tmp; clear H_tmp.
intros H_0_gt_b1 H_min.
rewrite H_min.
elim (le_lt_dec (Zabs_nat b1) (ones w1 i)).
intro H_diff.
rewrite inj_minus1; auto.
unfold Zminus.
assert (H_aux: (- Zabs_nat b1 = b1)%Z).
rewrite inj_Zabs_nat.
elim (Zabs_spec b1).
intro H_tmp.
destruct H_tmp.
congruence.
intro H_tmp.
destruct H_tmp.
rewrite H0.
auto with zarith.
rewrite H_aux; clear H_aux.
exact H_cmp.
intro H_diff.
apply
(Zle_trans
(ones w1 i - Zabs_nat b1)%nat
0
(ones w2 i)); try omega.
rewrite inj_minus2; try solve [apply Zle_refl].
unfold gt.
exact H_diff.
apply
(Zle_trans
(ones w2' (ones w2 i) - ones w1' (ones w1 i))%Z
(ones w2' (ones w2 i) - ones w1' (ones w2 i - max_0_b2))%Z
(max_0_b2 + b2')%Z).
apply Zplus_le_compat; try solve [ apply Zle_refl ].
assert (H_cc:
(ones w1' (ones w2 i - max_0_b2) <= ones w1' (ones w1 i))%Z).
apply inj_le.
apply ones_increasing.
unfold max_0_b2.
destruct (H_b1_le_ones_diff_le_b2 i).
elim (Zmax_spec 0 b2).
intro H_tmp.
elim H_tmp; clear H_tmp.
intros H_b2 H_max.
rewrite H_max.
simpl.
omega.
intro H_tmp.
elim H_tmp; clear H_tmp.
intros H_b2 H_max.
rewrite H_max.
apply inj_le_rev.
elim (le_lt_dec (Zabs_nat b2) (ones w2 i)).
intro H_diff.
rewrite inj_minus1; auto.
rewrite inj_Zabs_nat.
elim (Zabs_spec b2).
intro H_tmp.
destruct H_tmp.
rewrite H2.
auto with zarith.
intro H_tmp.
destruct H_tmp.
congruence.
intro H_diff.
apply
(Zle_trans
(ones w2 i - Zabs_nat b2)%nat
0
(ones w1 i)); try omega.
rewrite inj_minus2; try solve [apply Zle_refl].
unfold gt.
exact H_diff.
omega.
apply
(Zle_trans
(ones w2' (ones w2 i) - ones w1' (ones w2 i - max_0_b2))%Z
(ones w2' (ones w2 i) - (ones w1' (ones w2 i) - max_0_b2))%Z
(max_0_b2 + b2')).
apply Zplus_le_compat; try solve [ apply Zle_refl ].
assert (H_cc:
((ones w1' (ones w2 i) - max_0_b2) <= ones w1' (ones w2 i - max_0_b2))%Z).
generalize (ones_w_m_d_le_ones_delay_d_w H_wf1' max_0_b2 (ones w2 i)).
rewrite ones_delay_d_w_i_eq_ones_w_i_m_d; auto.
omega.
destruct (H_b1'_le_ones_diff_le_b2' (ones w2 i)).
omega.
Qed.
End sync_properties.
Section subtyping_properties.
Lemma on_subtyping_compat:
forall (w1: ibw),
forall (w2: ibw),
forall (w1': ibw) (H_wf1': well_formed_ibw w1'),
forall (w2': ibw) (H_wf2': well_formed_ibw w2'),
forall H_sub_w1_w2: subtyping w1 w2,
forall H_sub_w1'_w2': subtyping w1' w2',
subtyping (on w1 w1') (on w2 w2').
Proof.
intros.
destruct H_sub_w1_w2.
destruct H_sub_w1'_w2'.
split.
apply on_prec_compat; auto.
apply on_sync_compat; auto.
Qed.
End subtyping_properties.