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