Library abstraction_phd_def



Set Implicit Arguments.

Require Import Setoid.
Require Import floor.
Require Import Bool.
Require Import Omega.
Require Import ZArith.
Require Import Znumtheory.
Require Import Z_misc.
Require Import QArith.
Require Import Q_misc.
Require Import comparison.
Require Import misc.
Require Import ibw_def.

Record abstractionh : Set :=
  abshmake { absh_b1: Q; absh_b0: Q; absh_r: Q }.

Definition well_formed_abstractionh (a:abstractionh) :=
  0 <= absh_r a <= 1.

Definition strong_well_formed_abstractionh (a:abstractionh) :=
  well_formed_abstractionh a
  /\ (absh_b0 a <= absh_b1 a)
  /\ (absh_r a == 1 -> absh_b1 a <= 0)
  /\ (absh_r a == 0 -> absh_b0 a >= 0).

Definition in_abstractionh (w: ibw) (a:abstractionh) :=
  forall i: nat,
  forall H_i_ge_1: (i >= 1)%nat,
  (w i = true -> ones w i <= absh_r a * i + absh_b1 a)
  /\
  (w i = false -> ones w i >= absh_r a * i + absh_b0 a).

Fixpoint ones_early (a:abstractionh) (i:nat) { struct i } :=
  match i with
  | O => O
  | S i' =>
    let ones_i' := ones_early a i' in
    match Qcompare (S ones_i') (absh_r a * i + absh_b1 a) with
    | Lt | Eq => S ones_i'
    | Gt => ones_i'
    end
  end.

Fixpoint ones_late (a:abstractionh) (i:nat) { struct i } :=
  match i with
  | O => O
  | S i' =>
    let ones_i' := ones_late a i' in
    match Qcompare (absh_r a * i + absh_b0 a) ones_i' with
    | Lt | Eq => ones_i'
    | _ => S ones_i'
    end
  end.

Definition ones_early_alt (a:abstractionh) (i:nat) : nat :=
  Zabs_nat (Zmax O (Zmin i (fl (absh_r a * i + absh_b1 a)))).

Definition ones_late_alt (a:abstractionh) (i:nat) : nat :=
  Zabs_nat (Zmax O (Zmin i (cg (absh_r a * i + absh_b0 a)))).

Definition w_early (a:abstractionh) : ibw :=
  ibw_of_ones (ones_early a).

Definition w_late (a:abstractionh) : ibw :=
  ibw_of_ones (ones_late a).

Definition non_empty (a: abstractionh) :=
  exists w:ibw, in_abstractionh w a.

Definition absh_std a :=
  abshmake
    ((Qnum (absh_b1 a) * QDen (absh_r a))%Z # (Qden (absh_b1 a) * Qden (absh_r a)))
    (absh_b0 a)
    ((Qnum (absh_r a) * QDen (absh_b1 a))%Z # (Qden (absh_b1 a) * Qden (absh_r a))).

Definition non_empty_test (a: abstractionh) :=
  let a_std := absh_std a in
  absh_b1 a_std - absh_b0 a_std >= 1 - (1 # Qden (absh_r a_std)).

Definition non_empty_test_alt (a: abstractionh) :=
  Qden (absh_b1 a) = Qden (absh_r a)
  /\
  absh_b1 a - absh_b0 a >= 1 - (1 # Qden (absh_r a)).

Definition absh_included (a1: abstractionh) (a2:abstractionh) :=
  forall w: ibw,
  forall H_w_in_a1: in_abstractionh w a1,
  in_abstractionh w a2.

Definition absh_included_test (a1: abstractionh) (a2:abstractionh) :=
  (absh_r a1 == absh_r a2) /\
  (absh_b1 a1) <= (absh_b1 a2) /\
  (absh_b0 a1) >= (absh_b0 a2).


Definition on_absh (a1: abstractionh) (a2:abstractionh) :=
  let absh_b0_1 :=
    match Qcompare (absh_b0 a1) 0 with
    | Gt => 0
    | _ => absh_b0 a1
    end
  in
  let absh_b0_2 :=
    match Qcompare (absh_b0 a2) 0 with
    | Gt => 0
    | _ => absh_b0 a2
    end
  in
  abshmake
    (absh_b1 a1 * absh_r a2 + absh_b1 a2)
    (absh_b0_1 * absh_r a2 + absh_b0_2)
    (absh_r a1 * absh_r a2).


Definition not_absh (a: abstractionh) :=
  abshmake
    (- absh_b0 a)
    (- absh_b1 a)
    (1 - absh_r a).


Definition sync_absh (a1 a2: abstractionh) : Prop :=
  forall w1: ibw,
  forall w2: ibw,
  forall H_w1_in_a1: in_abstractionh w1 a1,
  forall H_w2_in_a2: in_abstractionh w2 a2,
  sync w1 w2.

Definition sync_absh_test (a1 a2: abstractionh) : Prop :=
  absh_r a1 == absh_r a2.


Definition prec_absh (a1 a2: abstractionh) : Prop :=
  forall w1: ibw,
  forall w2: ibw,
  forall H_w1_in_a1: in_abstractionh w1 a1,
  forall H_w2_in_a2: in_abstractionh w2 a2,
  prec w1 w2.

Definition prec_absh_alt (a1 a2: abstractionh) : Prop :=
  prec (w_late a1) (w_early a2).

Definition prec_absh_test (a1 a2: abstractionh) : Prop :=
  absh_b1 a2 - absh_b0 a1 < 1.


Definition subtyping_absh (a1 a2: abstractionh) : Prop :=
  forall w1: ibw,
  forall w2: ibw,
  forall H_w1_in_a1: in_abstractionh w1 a1,
  forall H_w2_in_a2: in_abstractionh w2 a2,
  subtyping w1 w2.

Definition subtyping_absh_alt (a1 a2: abstractionh) : Prop :=
  prec_absh a1 a2 /\ sync_absh a1 a2.


Definition size_absh (a1 a2: abstractionh) : Z :=
  fl ((absh_b1 a1) - (absh_b0 a2)).