Library abstraction_jfla_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 abstractionj : Set :=
  absjmake { absj_b1: Q; absj_b0: Q; absj_r: Q }.

Definition well_formed_abstractionj (a:abstractionj) :=
  0 <= absj_r a <= 1.

Definition in_abstractionj (w: ibw) (a:abstractionj) :=
  forall i: nat,
  forall H_i_ge_1: (i >= 1)%nat,
  (w i = true -> ones w (pred i) < absj_r a * i + absj_b1 a)
  /\
  (w i = false -> ones w (pred i) >= absj_r a * i + absj_b0 a).

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

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

Definition ones_early_alt (a:abstractionj) (i:nat) : nat :=
  Zabs_nat (Zmax O (Zmin i (cg (absj_r a * i + absj_b1 a)))).

Definition ones_late_alt (a:abstractionj) (i:nat) : nat :=
  Zabs_nat (Zmax O (Zmin i (cg (absj_r a * i + absj_b0 a)))).

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

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

Definition non_empty (a: abstractionj) :=
  exists w:ibw, in_abstractionj w a.

Definition non_empty_test (a: abstractionj) :=
  absj_b0 a <= absj_b1 a.

Definition absj_included (a1: abstractionj) (a2:abstractionj) :=
  forall w: ibw,
  forall H_w_in_a1: in_abstractionj w a1,
  in_abstractionj w a2.

Definition absj_included_test (a1: abstractionj) (a2:abstractionj) :=
  (absj_r a1 == absj_r a2) /\
  (absj_b1 a1) <= (absj_b1 a2) /\
  (absj_b0 a1) >= (absj_b0 a2).


Definition on_absj_alt (a1: abstractionj) (a2:abstractionj) :=
  let absj_b0_1 :=
    match Qcompare (absj_b0 a1) 0 with
    | Gt => 0
    | _ => absj_b0 a1
    end
  in
  let absj_b0_2 :=
    match Qcompare (absj_b0 a2) 0 with
    | Gt => 0
    | _ => absj_b0 a2
    end
  in
  let delta :=
    (1 - (1 # Qden (absj_r a1) )) * ((absj_r a2) - (1 # Qden (absj_r a2)))
  in
  absjmake
    (absj_b1 a1 * absj_r a2 + absj_b1 a2 + delta)
    (absj_b0_1 * absj_r a2 + absj_b0_2)
    (absj_r a1 * absj_r a2).

Definition absj_std a :=

  absjmake
    (absj_b1 a * (QDen (absj_r a) # Qden (absj_r a)))
    (absj_b0 a)
    (absj_r a * (QDen (absj_b1 a) # Qden (absj_b1 a))).

Definition on_absj (a1: abstractionj) (a2:abstractionj) :=
  let a1_std := absj_std a1 in
  let a2_std := absj_std a2 in
  on_absj_alt a1_std a2_std.


Definition not_absj (a: abstractionj) :=
  let epsilon := 1 - (1 # Qden (absj_r a) ) in
  absjmake
    (- absj_b0 a - epsilon)
    (- absj_b1 a - epsilon)
    (1 - absj_r a).


Definition sync_absj (a1 a2: abstractionj) : Prop :=
  forall w1: ibw,
  forall w2: ibw,
  forall H_w1_in_a1: in_abstractionj w1 a1,
  forall H_w2_in_a2: in_abstractionj w2 a2,
  sync w1 w2.

Definition sync_absj_test (a1 a2: abstractionj) : Prop :=
  absj_r a1 == absj_r a2.


Definition prec_absj (a1 a2: abstractionj) : Prop :=
  forall w1: ibw,
  forall w2: ibw,
  forall H_w1_in_a1: in_abstractionj w1 a1,
  forall H_w2_in_a2: in_abstractionj w2 a2,
  prec w1 w2.

Definition prec_absj_alt (a1 a2: abstractionj) : Prop :=
  prec (w_late a1) (w_early a2).

Definition prec_absj_test (a1 a2: abstractionj) : Prop :=
  absj_b0 a1 >= absj_b1 a2.


Definition subtyping_absj (a1 a2: abstractionj) : Prop :=
  forall w1: ibw,
  forall w2: ibw,
  forall H_w1_in_a1: in_abstractionj w1 a1,
  forall H_w2_in_a2: in_abstractionj w2 a2,
  subtyping w1 w2.

Definition subtyping_absj_alt (a1 a2: abstractionj) : Prop :=
  prec_absj a1 a2 /\ sync_absj a1 a2.