Library ibw_prop



Set Implicit Arguments.

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

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: subtyping w1 w2,
  exists b, forall i,
    (0 <= sizei w1 w2 i <= b)%Z.
Proof.
  apply communication_through_buffer_aux.
Qed.