Partially revert "Adapt to rocq-prover/rocq#19530"

This partially reverts commit d8a6fca.

Author: proux01

src/IEEE754/BinarySingleNaN.v

@@ -158,21 +158,12 @@ Proof.
 now intros T fz fi fn ff [sx|sx| |sx mx ex] Hx.
 Qed.
 
-Lemma canonical_mantissa_compat mx ex :
-  canonical_mantissa mx ex
-  = match (fexp (Z.pos (digits2_pos mx) + ex) ?= ex)%Z with
-    | Eq => true
-    | _ => false
-    end.
-Proof. now unfold canonical_mantissa; rewrite ?Z.eqb_compare. Qed.
-
 Theorem canonical_canonical_mantissa :
   forall (sx : bool) mx ex,
   canonical_mantissa mx ex = true ->
   canonical radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex).
 Proof.
 intros sx mx ex H.
-rewrite ?canonical_mantissa_compat in H.
 assert (Hx := Zeq_bool_eq _ _ H). clear H.
 apply sym_eq.
 simpl.
@@ -708,7 +699,6 @@ apply Rle_trans with ((bpow radix2 (Zdigits radix2 (Z.pos mx)) - 1) * bpow radix
   { rewrite Rmult_minus_distr_r, Rmult_1_l, <- bpow_plus.
     apply Rplus_le_compat_r.
     apply bpow_le.
-    rewrite ?canonical_mantissa_compat in H1.
     apply Zeq_bool_eq in H1.
     rewrite Zpos_digits2_pos in H1.
     unfold fexp, FLT_exp in H1.
@@ -734,7 +724,6 @@ Theorem bounded_lt_emax :
 Proof.
 intros mx ex Hx.
 destruct (andb_prop _ _ Hx) as (H1,H2).
-rewrite ?canonical_mantissa_compat in H1.
 generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1.
 generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2.
 generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex).
@@ -783,7 +772,6 @@ Theorem bounded_ge_emin :
 Proof.
 intros mx ex Hx.
 destruct (andb_prop _ _ Hx) as [H1 _].
-rewrite ?canonical_mantissa_compat in H1.
 apply Zeq_bool_eq in H1.
 generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex).
 destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as [e' Ex].
@@ -848,7 +836,6 @@ Proof.
 intros mx ex Cx Bx.
 apply andb_true_intro.
 split.
-rewrite ?canonical_mantissa_compat.
 unfold canonical_mantissa.
 unfold canonical, Fexp in Cx.
 rewrite Cx at 2.
@@ -1216,7 +1203,6 @@ easy.
 unfold valid_binary, bounded.
 rewrite Zle_bool_refl.
 rewrite Bool.andb_true_r.
-rewrite ?canonical_mantissa_compat.
 apply Zeq_bool_true.
 rewrite Zpos_digits2_pos.
 replace (Zdigits radix2 _) with prec.
@@ -1378,7 +1364,6 @@ elim Rgt_not_eq with (2 := H3).
 rewrite F2R_0.
 now apply F2R_gt_0.
 destruct (binary_fit_aux_correct m (Rlt_bool x 0) m2 e2) as [H5 H6].
-  rewrite ?canonical_mantissa_compat.
   apply Zeq_bool_true.
   rewrite Zpos_digits2_pos.
   rewrite <- mag_F2R_Zdigits by easy.
@@ -1503,7 +1488,6 @@ elim Rgt_not_eq with (2 := H3).
 rewrite F2R_0.
 now apply F2R_gt_0.
 destruct (binary_fit_aux_correct m (Rlt_bool x 0) m2 e2) as [H5 H6].
-  rewrite ?canonical_mantissa_compat.
   apply Zeq_bool_true.
   rewrite Zpos_digits2_pos.
   rewrite <- mag_F2R_Zdigits by easy.
@@ -1568,7 +1552,6 @@ assert (forall m e, bounded m e = true -> fexp (Zdigits radix2 (Zpos m) + e) = e
 clear. intros m e Hb.
 destruct (andb_prop _ _ Hb) as (H,_).
 apply Zeq_bool_eq.
-rewrite ?canonical_mantissa_compat in H.
 now rewrite <- Zpos_digits2_pos.
 generalize (H _ _ Hx) (H _ _ Hy).
 clear x y sx sy Hx Hy H.
@@ -2306,11 +2289,10 @@ apply binary_round_aux_correct'.
   + rewrite <- 2!F2R_Zabs, 2!abs_cond_Zopp; simpl.
     replace (SpecFloat.new_location _ _) with (Bracket.new_location (Z.pos my) r loc_Exact);
       [exact Bz|].
-    case my as [p|p|]; unfold new_location, SpecFloat.new_location; simpl.
-    * now unfold SpecFloat.new_location_odd; rewrite ?Z.eqb_compare.
-    * unfold SpecFloat.new_location_even; rewrite ?Z.eqb_compare.
-      now unfold new_location_even; case (2 * r ?= Z.pos p~0)%Z.
-    * now unfold SpecFloat.new_location_odd; rewrite ?Z.eqb_compare.
+    case my as [p|p|]; [reflexivity| |reflexivity].
+    unfold Bracket.new_location, SpecFloat.new_location; simpl.
+    unfold Bracket.new_location_even, SpecFloat.new_location_even; simpl.
+    now case Zeq_bool; [|case r as [|rp|rp]; case Z.compare].
   + now apply F2R_neq_0 ; case sy.
 - rewrite <- cexp_abs, Rabs_mult, Rabs_Rinv.
   rewrite 2!F2R_cond_Zopp, 2!abs_cond_Ropp, <- Rabs_Rinv.
@@ -2399,8 +2381,7 @@ assert (mx' = Zpos mx * Zpower radix2 (ex - 2 * e'))%Z as <-.
   easy. }
 clearbody mx'.
 destruct Z.sqrtrem as [mz r].
-rewrite ?Z.eqb_compare; unfold Zeq_bool.
-set (lz := if match (r ?= 0)%Z with Eq => true | _ => _ end then _ else _).
+set (lz := if Zeq_bool r 0 then _ else _).
 clearbody lz.
 intros Bz.
 refine (_ (binary_round_aux_correct' m (sqrt (F2R (Float radix2 (Zpos mx) ex))) mz e' lz _ _ _)) ; cycle 1.
@@ -2563,8 +2544,7 @@ Proof.
   { unfold mrs'. case Zlt_bool_spec; [ | easy]. intros Hex1. symmetry.
     apply shr_limit; simpl; [now left |]. apply Z.lt_le_trans with (radix2 ^ prec)%Z.
     - unfold bounded, canonical_mantissa, fexp in Hmxex. apply andb_prop in Hmxex.
-      destruct Hmxex as [Hmxex _].
-      rewrite ?Z.eqb_compare in Hmxex. apply Zeq_bool_eq in Hmxex.
+      destruct Hmxex as [Hmxex _]. apply Zeq_bool_eq in Hmxex.
       rewrite Zpos_digits2_pos in Hmxex. apply Z.eq_le_incl in Hmxex.
       apply Z.max_lub_l in Hmxex.
       assert (Hmx : (Zdigits radix2 (Z.pos mx) <= prec)%Z) by lia.
@@ -2606,9 +2586,7 @@ Proof.
           * apply Z.opp_pos_neg in Hex0. apply Z.div_le_compat_l; [lia |].
             split; [lia |]. apply Z.pow_le_mono_r; lia.
         + rewrite Zdigits_div_Zpower; [| lia |].
-          * rewrite Z.sub_add.
-            rewrite ?Z.eqb_compare in Hmxex. apply Zeq_bool_eq in Hmxex.
-            unfold fexp in *.
+          * rewrite Z.sub_add. apply Zeq_bool_eq in Hmxex. unfold fexp in *.
             rewrite Z.max_lub_iff. split; [| lia]. apply (Zplus_le_reg_l _ _ ex).
             rewrite Zplus_0_r. rewrite Z.add_sub_assoc. rewrite Z.add_comm.
             rewrite <-Hmxex at 2. apply Z.le_max_l.
@@ -2617,8 +2595,7 @@ Proof.
     refine (_ (shl_align_correct' p 0 (fexp (Z.pos (digits2_pos p) + 0)) _)).
     + rewrite H1. intros [H2 H3]. rewrite <-H3 in H2.
       apply andb_true_intro; split.
-      * rewrite ?Z.eqb_compare.
-        apply Zeq_bool_true. rewrite H3 at 2. rewrite !Zpos_digits2_pos.
+      * apply Zeq_bool_true. rewrite H3 at 2. rewrite !Zpos_digits2_pos.
         rewrite <-!mag_F2R_Zdigits; [| lia | lia].
         now apply (f_equal (fun f => fexp (mag radix2 f))).
       * apply Zle_bool_true. rewrite H3. transitivity 0%Z; [assumption|].
@@ -2808,7 +2785,7 @@ Lemma Bmax_float_proof :
   = true.
 Proof.
 unfold valid_binary, bounded; apply andb_true_intro; split.
-- rewrite ?canonical_mantissa_compat; unfold canonical_mantissa; apply Zeq_bool_true.
+- unfold canonical_mantissa; apply Zeq_bool_true.
   set (p := Z.pos (digits2_pos _)).
   assert (H : p = prec).
   { unfold p; rewrite Zpos_digits2_pos, Pos2Z.inj_sub.
@@ -2871,7 +2848,7 @@ cut (Z.pos (digits2_pos m) = prec)%Z.
 { now intro H; split; [ |exact H]; ring_simplify; rewrite H. }
 revert B; unfold bounded, canonical_mantissa.
 intro H; generalize (andb_prop _ _ H); clear H; intros [H _]; revert H.
-intro H; rewrite ?Z.eqb_compare in H; generalize (Zeq_bool_eq _ _ H); clear H.
+intro H; generalize (Zeq_bool_eq _ _ H); clear H.
 unfold fexp, emin.
 unfold Prec_gt_0 in prec_gt_0_; unfold Prec_lt_emax in prec_lt_emax_.
 lia.
@@ -2969,10 +2946,7 @@ set (z := fst _).
 set (e := snd _); simpl.
 assert (Dmx_le_prec : (Z.pos (digits2_pos mx) <= prec)%Z).
 { revert Bx; unfold bounded; rewrite Bool.andb_true_iff.
-  rewrite ?canonical_mantissa_compat.
-  unfold canonical_mantissa.
-  fold (Zeq_bool (fexp (Z.pos (digits2_pos mx) + ex)) ex).
-  rewrite <-Zeq_is_eq_bool; unfold fexp, FLT_exp.
+  unfold canonical_mantissa; rewrite <-Zeq_is_eq_bool; unfold fexp, FLT_exp.
   case (Z.max_spec (Z.pos (digits2_pos mx) + ex - prec) emin); lia. }
 assert (Dmx_le_prec' : (digits2_pos mx <= Z.to_pos prec)%positive).
 { change (_ <= _)%positive
@@ -2994,7 +2968,6 @@ case (Pos.leb_spec _ _); simpl; intro Dmx.
   + apply andb_true_intro.
     split ; cycle 1.
     { apply Zle_bool_true. clear -Hp ; lia. }
-    rewrite ?canonical_mantissa_compat.
     apply Zeq_bool_true; unfold fexp, FLT_exp.
     rewrite Dmx', Z2Pos.id by apply prec_gt_0_.
     rewrite Z.max_l.
@@ -3028,7 +3001,6 @@ case (Pos.leb_spec _ _); simpl; intro Dmx.
   + unfold bounded; apply andb_true_intro.
     split ; cycle 1.
     { apply Zle_bool_true. clear -Hp ; lia. }
-    rewrite ?canonical_mantissa_compat.
     apply Zeq_bool_true; unfold fexp, FLT_exp.
     rewrite Zpos_digits2_pos, shift_pos_correct, Z.pow_pos_fold.
     rewrite Z2Pos.id; [|lia].
@@ -3115,8 +3087,6 @@ Lemma Bulp_correct_aux :
   bounded 1 emin = true.
 Proof.
 unfold bounded, canonical_mantissa.
-rewrite ?Z.eqb_compare.
-fold (Zeq_bool (fexp (Z.pos (digits2_pos 1) + emin)) emin).
 rewrite Zeq_bool_true.
 apply Zle_bool_true.
 apply Z.max_l_iff, fexp_emax.

src/IEEE754/Bits.v

@@ -264,7 +264,6 @@ assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z).
 destruct (andb_prop _ _ Hx) as (Hx', _).
 unfold canonical_mantissa in Hx'.
 rewrite Zpos_digits2_pos in Hx'.
-rewrite ?Z.eqb_compare in Hx'.
 generalize (Zeq_bool_eq _ _ Hx').
 unfold fexp, FLT_exp, emin.
 clear ; lia.
@@ -321,8 +320,7 @@ intros [sx|sx|sx pl pl_range|sx mx ex H].
 - unfold bounded in H.
   apply Bool.andb_true_iff in H ; destruct H as [A B].
   apply Z.leb_le in B.
-  unfold canonical_mantissa, fexp, FLT_exp in A.
-  rewrite ?Z.eqb_compare in A; apply Zeq_bool_eq in A.
+  unfold canonical_mantissa, fexp, FLT_exp in A. apply Zeq_bool_eq in A.
   case Zle_bool_spec ; intros H.
   + apply join_bits_range.
     * split.
@@ -535,7 +533,6 @@ apply refl_equal.
 discriminate.
 clear -Hew ; lia.
 destruct (andb_prop _ _ Bx) as (H1, _).
-rewrite ?canonical_mantissa_compat in H1.
 generalize (Zeq_bool_eq _ _ H1).
 rewrite Zpos_digits2_pos.
 unfold FLT_exp, emin.
@@ -548,7 +545,6 @@ rewrite Zeq_bool_true. 2: apply refl_equal.
 simpl.
 apply f_equal.
 destruct (andb_prop _ _ Bx) as (H1, _).
-rewrite ?canonical_mantissa_compat in H1.
 generalize (Zeq_bool_eq _ _ H1).
 rewrite Zpos_digits2_pos.
 unfold FLT_exp, emin, prec.