proposition: Lemma div_u16_spec : forall a b, (1 <= a <= 65535)%Z -> (1 <= b <= 65535)%Z -> div_u16 a b = (a / b)%Z.
proof: Proof. intros a b Ba Bb. unfold div_u16. set (y0 := frcpa b). set (q0 := fma a y0 0). set (e0 := fnma b y0 (1 + pow2 (-17))). set (q1 := fma e0 q0 q0). apply Zfloor_imp. rewrite plus_IZR. simpl. apply Rmult_le_lt_reg_l with b. apply IZR_lt ; lia. apply Rplus_le_lt_reg_r with (-a). replace (b * (a / b)%Z + - a) with (-(a - (a / b)%Z * b)) by ring. replace (b * ((a / b)%Z + 1) + - a) with (b - (a - (a / b)%Z * b)) by ring. rewrite <- mult_IZR, <- minus_IZR. rewrite <- Zmod_eq_full by lia. cut (0 <= b * q1 - a < 1). cut (0 <= Zmod a b <= b - 1). lra. rewrite <- minus_IZR. apply IZR_le_le. generalize (Z_mod_lt a b). lia. assert (Ba': 1 <= a <= 65535). now split ; apply IZR_le. assert (Bb': 1 <= b <= 65535). now split ; apply IZR_le. refine (let '(conj H1 H2) := _ in conj H1 (Rnot_le_lt _ _ H2)). set (err := (q1 - a / b) / (a / b)). replace (b * q1 - a) with (a * err) by abstract (unfold err ; field ; lra). set (Mq0 := a * y0 + 0). set (Me0 := 1 + pow2 (-17) - b * y0). set (Mq1 := Me0 * Mq0 + Mq0). set (eps0 := (y0 - 1 / b) / (1 / b)). assert (H: (Mq1 - a / b) / (a / b) = -(eps0 * eps0) + (1 + eps0) * pow2 (-17)) by abstract (unfold Mq1, Me0, Mq0, eps0 ; field ; lra). revert H. unfold Mq1, Me0, Mq0, eps0, err, q1, e0, q0, y0. generalize (frcpa_spec b) (FIX_format_IZR radix2 a) (FIX_format_IZR radix2 b). gappa. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core) Gappa(Gappa_tactic)