# 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 abstraction_phd : Set :=
absmake { abs_b1: Q; abs_b0: Q; abs_r: Q }.

Definition well_formed_abstraction_phd (a:abstraction_phd) :=
0 <= abs_r a <= 1.

Definition strong_well_formed_abstraction_phd (a:abstraction_phd) :=
well_formed_abstraction_phd a
/\ (abs_b0 a <= abs_b1 a)
/\ (abs_r a == 1 -> abs_b1 a <= 0)
/\ (abs_r a == 0 -> abs_b0 a >= 0).

Definition in_abstraction_phd (w: ibw) (a:abstraction_phd) :=
forall i: nat,
forall H_i_ge_1: (i >= 1)%nat,
(w i = true -> ones w i <= abs_r a * i + abs_b1 a)
/\
(w i = false -> ones w i >= abs_r a * i + abs_b0 a).

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

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

Definition ones_early_alt (a:abstraction_phd) (i:nat) : nat :=
Zabs_nat (Zmax O (Zmin i (fl (abs_r a * i + abs_b1 a)))).

Definition ones_late_alt (a:abstraction_phd) (i:nat) : nat :=
Zabs_nat (Zmax O (Zmin i (cg (abs_r a * i + abs_b0 a)))).

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

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

Definition non_empty (a: abstraction_phd) :=
exists w:ibw, in_abstraction_phd w a.

Definition abs_std a :=
absmake
((Qnum (abs_b1 a) * QDen (abs_r a))%Z # (Qden (abs_b1 a) * Qden (abs_r a)))
(abs_b0 a)
((Qnum (abs_r a) * QDen (abs_b1 a))%Z # (Qden (abs_b1 a) * Qden (abs_r a))).

Definition non_empty_test (a: abstraction_phd) :=
let a_std := abs_std a in
abs_b1 a_std - abs_b0 a_std >= 1 - (1 # Qden (abs_r a_std)).

Definition non_empty_test_alt (a: abstraction_phd) :=
Qden (abs_b1 a) = Qden (abs_r a)
/\
abs_b1 a - abs_b0 a >= 1 - (1 # Qden (abs_r a)).

Definition abs_included (a1: abstraction_phd) (a2:abstraction_phd) :=
forall w: ibw,
forall H_w_in_a1: in_abstraction_phd w a1,
in_abstraction_phd w a2.

Definition abs_included_test (a1: abstraction_phd) (a2:abstraction_phd) :=
(abs_r a1 == abs_r a2) /\
(abs_b1 a1) <= (abs_b1 a2) /\
(abs_b0 a1) >= (abs_b0 a2).

Definition on_abs (a1: abstraction_phd) (a2:abstraction_phd) :=
let abs_b0_1 :=
match Qcompare (abs_b0 a1) 0 with
| Gt => 0
| _ => abs_b0 a1
end
in
let abs_b0_2 :=
match Qcompare (abs_b0 a2) 0 with
| Gt => 0
| _ => abs_b0 a2
end
in
absmake
(abs_b1 a1 * abs_r a2 + abs_b1 a2)
(abs_b0_1 * abs_r a2 + abs_b0_2)
(abs_r a1 * abs_r a2).

Definition not_abs (a: abstraction_phd) :=
absmake
(- abs_b0 a)
(- abs_b1 a)
(1 - abs_r a).

Definition sync_abs (a1 a2: abstraction_phd) : Prop :=
forall w1: ibw,
forall w2: ibw,
forall H_w1_in_a1: in_abstraction_phd w1 a1,
forall H_w2_in_a2: in_abstraction_phd w2 a2,
sync w1 w2.

Definition sync_abs_test (a1 a2: abstraction_phd) : Prop :=
abs_r a1 == abs_r a2.

Definition prec_abs (a1 a2: abstraction_phd) : Prop :=
forall w1: ibw,
forall w2: ibw,
forall H_w1_in_a1: in_abstraction_phd w1 a1,
forall H_w2_in_a2: in_abstraction_phd w2 a2,
prec w1 w2.

Definition prec_abs_alt (a1 a2: abstraction_phd) : Prop :=
prec (w_late a1) (w_early a2).

Definition prec_abs_test (a1 a2: abstraction_phd) : Prop :=
abs_b1 a2 - abs_b0 a1 < 1.

Definition adaptability_abs (a1 a2: abstraction_phd) : Prop :=
forall w1: ibw,
forall w2: ibw,
forall H_w1_in_a1: in_abstraction_phd w1 a1,
forall H_w2_in_a2: in_abstraction_phd w2 a2,