# Library abstraction_hfl_prim_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 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. ```