Library inw_def

Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.

Coercion Local Z_of_nat : nat >-> Z.

Definition inw := nat -> nat.

Fixpoint ones (w:inw) (i:nat) { struct i } :=
  match i with
  | 0 => 0
  | S i' =>
     w i + ones w i'
  end.

Definition inw_of_ones (ones_w: nat -> nat): inw :=
  fun i =>
    match i with
    | O => 0
    | S i' => (ones_w i) - (ones_w i')
    end.


Fixpoint sum (w:inw) d k { struct k } :=
  match k with
  | 0 => 0
  | S k' => w (k + d) + sum w d k'
  end.

Definition on (w1:inw) (w2:inw) : inw :=
  (fun i => sum w2 (ones w1 (pred i)) (w1 i)).


Definition prec (w1 w2: inw) : Prop :=
  forall i,
  ones w1 i >= ones w2 i.

Definition ones_supremum (w1 w2: inw) : nat -> nat :=
  fun i => Arith.Min.min (ones w1 i) (ones w2 i).

Definition ones_infimum (w1 w2: inw) : nat -> nat :=
  fun i => Arith.Max.max (ones w1 i) (ones w2 i).

Definition supremum (w1 w2: inw) : inw :=
  inw_of_ones (ones_supremum w1 w2).

Definition infimum (w1 w2: inw) : inw :=
  inw_of_ones (ones_infimum w1 w2).


Definition sync (w1 w2: inw) : Prop :=
  exists b1: Z,
  exists b2: Z,
  forall i,
  (b1 <= ones w2 i - ones w1 i <= b2)%Z.


Definition adaptability (w1 w2: inw) : Prop :=
  prec w1 w2 /\ sync w1 w2.


Definition size (w1 w2: inw) (s: nat) :=
  forall i,
    (ones w1 i) - (ones w2 i) <= s
    /\
    exists i, (ones w1 i) - (ones w2 i) = s.