# Library ibw_prop

Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.
Require Import ibw_def.
Require Import ibw_aux.

Remark zeros_def:
forall w: ibw,
forall i,
zeros w i = i - ones w i.
Proof.
exact zeros_def_aux.
Qed.

Remark ones_i_le_i:
forall w:ibw,
forall i,
ones w i <= i.
Proof.
apply ones_i_le_i_aux.
Qed.

Remark ones_increasing_by_one:
forall w: ibw,
forall i,
0 <= ones w (S i) - ones w i <= 1.
Proof.
intros w i.
split.
case_eq (w (S i)).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
omega.
intro H_w.
rewrite ones_S_i_eq_ones_i; auto.
omega.

case_eq (w (S i)).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
omega.
intro H_w.
rewrite ones_S_i_eq_ones_i; auto.
omega.
Qed.

Remark ones_eq_equiv_w_eq:
forall (w1: ibw) ,
forall (w2: ibw) ,
(forall i, ones w1 i = ones w2 i) <-> (forall i, i > 0 -> w1 i = w2 i).
Proof.
intros w1 w2.
split.
intros H_ones i H_i_ge_1.
apply ones_eq_impl_w_eq; auto.
intro H_w.
apply w_eq_impl_ones_eq; auto.
Qed.

Remark ibw_of_ones_correctness:
forall w: ibw,

forall i,
forall H_i_ge_1: i > 0,
ibw_of_ones (ones w) i = w i.
Proof.
apply ibw_of_ones_ones_w_eq_w.
Qed.

Remark ibw_of_ones_correctness2:
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.
apply ones_ibw_of_ones_ones_w_eq_ones_w.
Qed.

Property ones_on:
forall w1 w2 :ibw,
forall i,
ones (on w1 w2) i = ones w2 (ones w1 i).
Proof.
apply ones_on_def.
Qed.

Corollary on_assoc:
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.
apply on_assoc_aux.
Qed.

Remark prec_partial_order:
(forall w: ibw, prec w w)
/\
(forall w1 w2 w3: ibw, prec w1 w2 -> prec w2 w3 -> prec w1 w3)
/\
forall w1 w2: ibw,
prec w1 w2 -> prec w2 w1 -> (forall i, i > 0 -> w1 i = w2 i).
Proof.
repeat split.
apply prec_refl.
apply prec_trans.
intros; apply prec_antisym; auto.
Qed.

Lemma supremum_is_upperbound:
forall w1 w2: ibw,
prec w1 (supremum w1 w2) /\ prec w2 (supremum w1 w2).
Proof.
intros w1 w2.
split.
apply prec_w1_supremum.
apply prec_w2_supremum.
Qed.

Lemma infimum_is_lowerbound:
forall w1 w2: ibw,
prec (infimum w1 w2) w1 /\ prec (infimum w1 w2) w2.
Proof.
intros w1 w2.
split.
apply prec_infimum_w1.
apply prec_infimum_w2.
Qed.

Lemma supremum_prec_upperbounds:
forall w1 w2 w: ibw,
forall H_w_is_ub: prec w1 w /\ prec w2 w,
prec (supremum w1 w2) w.
Proof.
intros w1 w2 w H_w_is_ub.
destruct H_w_is_ub as [H_prec_1 H_prec_2].
unfold prec in *.
intro i.
rewrite ones_supremum_correctness.
unfold ones_supremum.
elim (Min.min_dec (ones w1 i) (ones w2 i)).
intro H_min; rewrite H_min.
exact (H_prec_1 i).
intro H_min; rewrite H_min.
exact (H_prec_2 i).
Qed.

Lemma lowerbound_prec_infimum:
forall w1 w2 w: ibw,
forall H_w_is_gl: prec w w1 /\ prec w w2,
prec w (infimum w1 w2).
Proof.
intros w1 w2 w H_w_is_ub.
destruct H_w_is_ub as [H_prec_1 H_prec_2].
unfold prec in *.
intro i.
rewrite ones_infimum_correctness.
unfold ones_infimum.
elim (Max.max_dec (ones w1 i) (ones w2 i)).
intro H_max; rewrite H_max.
exact (H_prec_1 i).
intro H_max; rewrite H_max.
exact (H_prec_2 i).
Qed.

Property supremum_correctness:
forall w1 w2: ibw,
(prec w1 (supremum w1 w2) /\ prec w2 (supremum w1 w2))
/\
(forall w: ibw, prec w1 w /\ prec w2 w -> prec (supremum w1 w2) w).
Proof.
intros.
split.
apply supremum_is_upperbound.
apply supremum_prec_upperbounds.
Qed.

Property infimum_correctness:
forall w1 w2: ibw,
(prec (infimum w1 w2) w1 /\ prec (infimum w1 w2) w2)
/\
(forall w: ibw, prec w w1 /\ prec w w2 -> prec w (infimum w1 w2)).
Proof.
intros.
split.
apply infimum_is_lowerbound.
apply lowerbound_prec_infimum.
Qed.

Remark sync_equiv_relation:
(forall w: ibw, sync w w)
/\
(forall w1 w2 w3: ibw, sync w1 w2 -> sync w2 w3 -> sync w1 w3)
/\
(forall w1 w2: ibw, sync w1 w2 -> sync w2 w1).
Proof.
intros.
repeat split.
apply sync_refl.
apply sync_trans.
apply sync_sym.
Qed.

Property communication_through_buffer:
forall (w1: ibw),
forall (w2: ibw),
forall H_sub_w1_w2: adaptability w1 w2,
exists b, forall i,
(0 <= sizei w1 w2 i <= b)%Z.
Proof.
apply communication_through_buffer_aux.
Qed.