Library inw_prop

Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.
Require Import inw_def.
Require Import inw_aux.

Remark ones_eq_equiv_w_eq:
  forall (w1: inw) ,
  forall (w2: inw) ,
  (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 inw_of_ones_correctness:
  forall w: inw,
  forall H_wf_w: well_formed_inw w,
  forall i,
  
  inw_of_ones (ones w) i = w i.
Proof.
  apply inw_of_ones_ones_w_eq_w.
Qed.

Remark inw_of_ones_correctness2:
  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.
  apply ones_inw_of_ones_ones_w_eq_ones_w.
Qed.

Property ones_on:
  forall w1 w2 :inw,
  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: inw,
  
  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: inw, prec w w)
  /\
  (forall w1 w2 w3: inw, prec w1 w2 -> prec w2 w3 -> prec w1 w3)
  /\
  forall w1 w2: inw, well_formed_inw w1 -> well_formed_inw w2 ->
    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.



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