Infotheo052 (#102)

* compat with Coq 8.17
affeldt-aist · Jun 3, 2023 · fdf42c6 · fdf42c6
1 parent 5f9efb8
commit fdf42c6
Show file tree

Hide file tree

Showing 21 changed files with 59 additions and 80 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,10 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/README.md b/README.md
@@ -31,7 +31,7 @@ information theory, and linear error-correcting codes.
   - Takafumi Saikawa, Nagoya U.
   - Naruomi Obata, Titech (M2)
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.15, Coq 8.16
+- Compatible Coq versions: Coq 8.17
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

diff --git a/changelog.txt b/changelog.txt
@@ -1,4 +1,11 @@
 -------------------
+from 0.5.1 to 0.5.2
+-------------------
+compatibility release
+- generalized:
+  + invRK
+-------------------
+-------------------
 from 0.5.0 to 0.5.1
 -------------------
 compatibility release

diff --git a/coq-infotheo.opam b/coq-infotheo.opam
@@ -21,12 +21,12 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.15" & < "8.17~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.17~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
-  "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
-  "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
-  "coq-mathcomp-field" { (>= "1.14.0" & < "1.17~") | (= "dev")  }
+  "coq" { (>= "8.17" & < "8.18~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.15.0" & < "1.18~") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "1.15.0" & < "1.18~") | (= "dev")  }
+  "coq-mathcomp-algebra" { (>= "1.15.0" & < "1.18~") | (= "dev")  }
+  "coq-mathcomp-solvable" { (>= "1.15.0" & < "1.18~") | (= "dev")  }
+  "coq-mathcomp-field" { (>= "1.15.0" & < "1.18~") | (= "dev")  }
   "coq-mathcomp-analysis" { (>= "0.5.4") & (< "0.7~")}
   "coq-hierarchy-builder" { >= "1.3.0" }
 ]

diff --git a/ecc_modern/degree_profile.v b/ecc_modern/degree_profile.v
@@ -3709,8 +3709,7 @@ apply Order.POrderTheory.le_trans.
 apply ler_expn2r.
     by rewrite rpred_div // nnegrE ler0n.
   by rewrite rpred_div // nnegrE ler0n.
-apply ler_pmul => //.
-    by apply ler0n.
+rewrite ler_pmul//.
   by rewrite invr_ge0 ler0n.
 by rewrite subnDA subnAC ler_nat leq_subr.
 Qed.

diff --git a/ecc_modern/ldpc.v b/ecc_modern/ldpc.v
@@ -521,8 +521,7 @@ transitivity (\sum_(t in 'rV['F_2]_n)
       exact/eqP/invR_neq0.
       rewrite (eq_bigl (fun x => x \in [set cw in C])); last by move=> i; rewrite inE.
       by rewrite -not_receivable_prop_uniform receivableP.
-    rewrite invRK //; last  exact/eqP.
-    rewrite -mulRA mulRC mulVR ?mulR1 ?mulRV //; first by exact/eqP.
+    rewrite invRK -mulRA mulRC mulVR ?mulR1 ?mulRV //; first by exact/eqP.
     set tmp1 := \sum_(_ | _) _.
     rewrite /tmp1 (eq_bigl (fun x => x \in [set cw in C])); last by move=> i; rewrite inE.
     by rewrite -not_receivable_prop_uniform receivableP.

diff --git a/information_theory/channel_coding_converse.v b/information_theory/channel_coding_converse.v
@@ -149,10 +149,7 @@ rewrite expRM -mulRA; apply leR_pmul => //.
     rewrite -mulRA mulRC invRM; last 2 first.
     - by apply/eqP/invR_neq0/eqP; rewrite expR_eq0 mulR_neq0' ln2_neq0 andbT; exact/gtR_eqF.
     - by apply/eqP/invR_neq0/eqP; by rewrite INR_eq0'.
-    - rewrite invRK; last first.
-        by rewrite expR_eq0 mulR_neq0' ln2_neq0 andbT; exact/gtR_eqF.
-      rewrite invRK; last by rewrite INR_eq0'.
-      rewrite (_ : / (/ n%:R) ^ K = n%:R ^ K); last first.
+    - rewrite 2!invRK (_ : / (/ n%:R) ^ K = n%:R ^ K); last first.
         rewrite expRV ?INR_eq0' // invRK //; apply/expR_neq0; by rewrite INR_eq0'.
       rewrite -mulRA {1}/Rdiv (mulRA n%:R) -expRS mulRA -expRM.
       by rewrite -/(Rdiv _ _) mulRCA -mulRA (mulRC (ln 2)).

diff --git a/information_theory/source_coding_fl_converse.v b/information_theory/source_coding_fl_converse.v
@@ -63,7 +63,9 @@ by case: Hepsilon => ? ?; lra.
 Qed.
 
 Lemma lambda0 : 0 < lambda.
-Proof. rewrite /lambda; apply P_Rmin => //; [exact Hepsilon1 | exact Hr1]. Qed.
+Proof.
+by rewrite /lambda; apply Rmin_case => //; [exact Hepsilon1 | exact Hr1].
+Qed.
 
 Lemma Hdelta : 0 < delta.
 Proof.

diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v
@@ -198,10 +198,8 @@ rewrite inE /=; apply/negPn/negPn.
    apply Exp_le_increasing => //; apply leR_add2r.
     move/leR_max : Hdelta => [_ Hlambda].
     apply (@leR_pmul2r (2 / lambda)%R); first by apply/divR_gt0 => //; exact: lambda_gt0.
-    rewrite mul1R -mulRA -{2}(Rinv_Rdiv lambda 2); last 2 first.
-      by apply/eqP; rewrite gtR_eqF //; exact/lambda_gt0.
-      by move=> ?; lra.
-      by rewrite mulRV ?mulR1 //; exact/gtR_eqF/lambda2_gt0.
+    rewrite mul1R -mulRA -{2}(Rinv_div lambda 2).
+    by rewrite mulRV ?mulR1 //; exact/gtR_eqF/lambda2_gt0.
   apply: leR_trans; first exact/leR_add2l/TS_sup.
   apply (@leR_trans (exp2 (INR k* (`H P + lambda / 2)) +
                         exp2 (INR k * (`H P + lambda / 2)))%R).

diff --git a/information_theory/source_coding_vl_converse.v b/information_theory/source_coding_vl_converse.v
@@ -355,8 +355,7 @@ rewrite [X in _ <= X](_ :_ = log ( alp / (1 - alp)) - (log alp) * `E X);
   rewrite [in LHS]mulRDl mulRC oppRD mulN1R oppRK; congr (_ + _).
   rewrite -[in RHS]addRA -[LHS]addR0; congr (_ + _).
   rewrite mulRDl mulRV; last exact/gtR_eqF/EX_gt0.
-  rewrite mulN1R !addR_opp subRB subRR add0R invRK ?Rplus_opp_l //.
-  exact/gtR_eqF/EX_gt0.
+  by rewrite mulN1R !addR_opp subRB subRR add0R invRK ?Rplus_opp_l.
 apply: (@leR_trans (log (alp * (1 - (alp ^ (\max_(a | a \in A) size (f a))))
                                / (1 - alp)) - log alp * `E X ) _); last first.
   rewrite leR_add2r.

diff --git a/information_theory/source_coding_vl_direct.v b/information_theory/source_coding_vl_direct.v
@@ -292,7 +292,7 @@ Proof.
 move: (fdist_supp_lg_add_1_neq_0 P) => ?.
 rewrite mulRC /Rdiv -?mulRA; apply: (Rmult_lt_compat_l _ _ _ eps_pos); rewrite ?mulRA (mulRC _ 2).
 apply: (Rmult_lt_reg_l 3); first exact: Rplus_lt_pos.
-rewrite Rinv_mult_distr // ?mulRA (mulRC 3 2) Rinv_r_simpl_l //.
+rewrite Rinv_mult // ?mulRA (mulRC 3 2) Rinv_r_simpl_l //.
 apply: (Rmult_lt_reg_l (INR n)); first exact/ltR0n.
 rewrite mulRC -mulRA (mulRC _ (INR n)) ?mulRA Rinv_r_simpl_l; last first.
   by apply/eqP; rewrite INR_eq0'.
@@ -377,7 +377,7 @@ apply: (Rle_lt_trans _  (INR n'.+1 * (`H P + epsilon') + 1 + 1 +
   rewrite mulRDr (addRC (epsilon' * log (INR #|X|)) _) addRC addRA -addRA
     (addRC _ epsilon') -{2}(mulR1 epsilon') -mulRDr -addRA
     (addRC (epsilon' * (2 / INR n)) _) addRA addRC  mulRC addRC /epsilon'
-    -{1}(mulR1 3) -{3}(mulR1 3) -mulRDr /Rdiv {1}(Rinv_mult_distr) // mulRA
+    -{1}(mulR1 3) -{3}(mulR1 3) -mulRDr /Rdiv {1}Rinv_mult // mulRA
     -mulRA -Rinv_l_sym // mulR1.
   apply: (Rle_lt_trans _ (epsilon / 4 + epsilon * / 3 + epsilon / 3)).
   * apply: Rplus_le_compat.

diff --git a/information_theory/string_entropy.v b/information_theory/string_entropy.v
@@ -96,8 +96,7 @@ rewrite /entropy /nHs /num_occ_dist /= -mulRN1 big_distrl big_distrr /=.
 apply eq_bigr => a _ /=; rewrite ffunE.
 case: ifPn => [/eqP -> | Hnum]; first by rewrite !mulRA !simplR.
 rewrite {1}/Rdiv (mulRC N(a | s)) 3![in LHS]mulRA mulRV ?INR_eq0' // ?mul1R.
-rewrite -mulRA mulRN1 -logV; last by apply divR_gt0; rewrite ltR0n lt0n.
-rewrite Rinv_Rdiv //; apply/eqP; by rewrite INR_eq0'.
+by rewrite -mulRA mulRN1 -logV ?Rinv_div//; apply divR_gt0; rewrite ltR0n lt0n.
 Qed.
 
 Definition mulnRdep (x : nat) (y : x != O -> R) : R.

diff --git a/information_theory/types.v b/information_theory/types.v
@@ -459,8 +459,7 @@ Qed.
 
 Lemma card_typed_tuples : INR #| T_{ P } | <= exp2 (INR n * `H P).
 Proof.
-rewrite -(invRK (exp2 (INR n * `H P))%R); last exact/eqP.
-rewrite -exp2_Ropp -mulNR.
+rewrite -(invRK (exp2 (INR n * `H P))%R) -exp2_Ropp -mulNR.
 set aux := - INR n * `H P.
 rewrite -div1R leR_pdivl_mulr // {}/aux.
 case/boolP : [exists x, x \in T_{P}] => x_T_P.

diff --git a/lib/num_occ.v b/lib/num_occ.v
@@ -105,8 +105,7 @@ Lemma sum_num_occ_size (A : finType) s : (\sum_(a in A) N(a|s))%nat = size s.
 Proof.
 elim: s => [|a s IH] /=.
 + by apply big1_eq.
-+ rewrite big_split /= IH -big_mkcond /= (big_pred1 a) //.
-  by move=> i; rewrite eq_sym.
++ by rewrite big_split /= IH -big_mkcond /= (big_pred1 a).
 Qed.
 
 Lemma num_occ_flatten (A : finType) (a : A) ss :

diff --git a/lib/ssrR.v b/lib/ssrR.v
@@ -595,11 +595,11 @@ Proof. by move/eqP/invR_eq0/eqP. Qed.
 
 Definition invR1 : / 1 = 1 := Rinv_1.
 
-Definition invRK (r : R) : r != 0 -> / / r = r.
-Proof. by move/eqP; exact: Rinv_involutive. Qed.
+Definition invRK (r : R) : / / r = r.
+Proof. exact: Rinv_inv. Qed.
 
 Lemma invRM (r1 r2 : R) : r1 != 0 -> r2 != 0 -> / (r1 * r2) = / r1 * / r2.
-Proof. by move=> /eqP r10 /eqP r20; rewrite Rinv_mult_distr. Qed.
+Proof. by move=> /eqP r10 /eqP r20; rewrite Rinv_mult. Qed.
 
 Lemma leR_inv x y : 0 < y -> y <= x -> / x <= / y.
 Proof. by move=> x0 y0; apply/Rinv_le_contravar. Qed.
@@ -609,9 +609,7 @@ Proof. by move=> a b; rewrite !inE => _ /ltRP b0 ba; exact/Rinv_le_contravar. Qe
 
 Lemma invR_le x y : 0 < x -> 0 < y -> / y <= / x -> x <= y.
 Proof.
-move=> x0 y0 H.
-rewrite -(invRK x); last exact/gtR_eqF.
-rewrite -(invRK y); last exact/gtR_eqF.
+move=> x0 y0 H; rewrite -(invRK x) -(invRK y).
 by apply leR_inv => //; exact/invR_gt0.
 Qed.
 
@@ -727,7 +725,7 @@ Proof. by move=> x0; apply/idP/idP => /leRP/(invR_le1 _ x0)/leRP. Qed.
 Lemma invR_gt1 x : 0 < x -> (1 < / x) <-> (x < 1).
 Proof.
 move=> x0; split => x1; last by rewrite -invR1; apply ltR_inv.
-move/ltR_inv : x1; rewrite invRK ?invR1; last exact/gtR_eqF.
+move/ltR_inv : x1; rewrite invRK invR1.
 by apply => //; exact/invR_gt0.
 Qed.
 Lemma invR_gt1' x : 0 < x -> (1 <b / x) = (x <b 1).

diff --git a/lib/ssr_ext.v b/lib/ssr_ext.v
@@ -904,11 +904,11 @@ apply eq_from_tnth; case.
 destruct n as [|n] => //.
 case=> [Hi | i Hi].
   rewrite (tnth_nth (thead a, thead b)) (tnth_nth (thead (zip_tuple a b))).
-  rewrite /= enum_ordS /= (tnth_nth (thead a, thead b)) /= nth_zip; last first.
+  rewrite /= enum_ordSl /= (tnth_nth (thead a, thead b)) /= nth_zip; last first.
     by rewrite (size_tuple a) (size_tuple b).
   by rewrite (tnth_nth (thead a)) /= (tnth_nth (thead b)).
 rewrite (tnth_nth (thead a, thead b)) (tnth_nth (thead (zip_tuple a b))) /=.
-rewrite enum_ordS /= nth_zip; last by rewrite 4!size_map size_enum_ord.
+rewrite enum_ordSl /= nth_zip; last by rewrite 4!size_map size_enum_ord.
 rewrite [in RHS](nth_map ord0); last by rewrite size_map size_enum_ord.
 rewrite [in RHS](tnth_nth (thead a, thead b)) [in RHS]/zip_tuple /=.
 rewrite [in RHS]nth_zip; last by rewrite (size_tuple a) (size_tuple b).

diff --git a/meta.yml b/meta.yml
@@ -41,43 +41,39 @@ license:
 nix: true
 
 supported_coq_versions:
-  text: Coq 8.15, Coq 8.16
-  opam: '{ (>= "8.15" & < "8.17~") | (= "dev") }'
+  text: Coq 8.17
+  opam: '{ (>= "8.17" & < "8.18~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.15.0-coq-8.15'
+- version: '1.16.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.16'
+- version: '1.17.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev") }'
+    version: '{ (>= "1.15.0" & < "1.18~") | (= "dev") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
+    version: '{ (>= "1.15.0" & < "1.18~") | (= "dev")  }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
+    version: '{ (>= "1.15.0" & < "1.18~") | (= "dev")  }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
+    version: '{ (>= "1.15.0" & < "1.18~") | (= "dev")  }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.14.0" & < "1.17~") | (= "dev")  }'
+    version: '{ (>= "1.15.0" & < "1.18~") | (= "dev")  }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:

diff --git a/probability/divergence.v b/probability/divergence.v
@@ -86,8 +86,7 @@ rewrite /div [X in _ <= X](_ : _ =
   case/boolP : (P a == 0) => [/eqP ->|H0]; first by rewrite !mul0R.
   congr (_ * _).
   have Qa0 := dominatesEN P_dom_by_Q H0.
-  rewrite -logV; last by apply divR_gt0; rewrite -fdist_gt0.
-  rewrite Rinv_Rdiv //; exact/eqP.
+  by rewrite -logV ?Rinv_div//; apply divR_gt0; rewrite -fdist_gt0.
 rewrite leR_oppr oppR0.
 apply (@leR_trans ((\sum_(a | a \in A) (Q a - P a)) * log (exp 1))).
   rewrite (big_morph _ (morph_mulRDl _) (mul0R _)).
@@ -117,8 +116,7 @@ apply/esym; move: a (erefl true); apply leR_sumR_eq.
     case/boolP : (P a == 0) => [/eqP ->| H0]; first by rewrite !mul0R.
     congr (_ * _).
     have Qa0 := dominatesEN P_dom_by_Q H0.
-    rewrite -logV; last by apply divR_gt0; rewrite -fdist_gt0.
-    rewrite Rinv_Rdiv //; exact/eqP.
+    by rewrite -logV ?Rinv_div//; apply divR_gt0; rewrite -fdist_gt0.
   rewrite -(big_morph _ (morph_mulRDl _) (mul0R _)) big_split /=.
   by rewrite -big_morph_oppR !FDist.f1 addR_opp subRR mul0R.
 Qed.

diff --git a/probability/ln_facts.v b/probability/ln_facts.v
@@ -189,22 +189,21 @@ case (total_order_T 0 r) ; first case ; move=> Hcase.
       rewrite -mulRN.
       apply (@ltR_pmul2r (/ - X)); first exact/invR_gt0/oppR_gt0.
       rewrite -mulRA mulRV ?mulR1; last by rewrite oppR_eq0; apply/ltR_eqF.
-      rewrite -(invRK 2); last exact/eqP.
-      rewrite -mulRA ( _ : forall r, r * r = r ^ 2); last by move=> ?; rewrite /pow mulR1.
+      rewrite -(invRK 2) -mulRA.
+      rewrite ( _ : forall r, r * r = r ^ 2); last by move=> ?; rewrite /pow mulR1.
       rewrite expRV; last exact/eqP/not_eq_sym/eqP/ltR_eqF/oppR_gt0.
       rewrite -invRM; last 2 first.
         by rewrite invR_neq0' //; exact/gtR_eqF.
         by rewrite expR_eq0 oppR_eq0; exact/ltR_eqF.
-      rewrite -(invRK (exp X)); last exact/gtR_eqF/exp_pos.
+      rewrite -(invRK (exp X)).
       apply ltR_inv => //.
         exact/invR_gt0/exp_pos.
         by apply/mulR_gt0; [lra | apply expR_gt0; lra].
       rewrite -exp_Ropp mulRC (_ : 2 = INR 2`!) //.
       exact/exp_strict_lb/oppR_gt0.
     * apply (@leR_pmul2r (/ 2)); first exact/invR_gt0.
       rewrite mulRC mulRA mulVR ?mul1R //; last exact/gtR_eqF.
-      rewrite -(invRK eps); last exact/gtR_eqF.
-      rewrite -invRM //; last 2 first.
+      rewrite -(invRK eps) -invRM //; last 2 first.
         exact/gtR_eqF/invR_gt0.
         exact/eqP.
       apply leR_inv => //.

diff --git a/probability/log_sum.v b/probability/log_sum.v
@@ -114,9 +114,7 @@ rewrite -[X in _ <= X]oppRK leR_oppr -ln_Rinv; last first.
 rewrite invRM; last 2 first.
   exact/gtR_eqF/(fspos _ C_a).
   by rewrite invR_neq0' // gtR_eqF //; exact/(gspos _ C_a).
-rewrite invRK; last exact/gtR_eqF/(gspos _ C_a).
-rewrite mulRC.
-apply: leR_trans.
+rewrite invRK mulRC; apply: leR_trans.
   by apply/ln_id_cmp/divR_gt0; [apply gspos | apply fspos].
 apply Req_le.
 by field; exact/eqP/gtR_eqF/(fspos _ C_a).
@@ -157,7 +155,7 @@ suff : \sum_{D} f * log (\sum_{D} f / \sum_{D} g) <=
     by apply sumR_ge0 => ? ?; exact: nneg_finfun_ge0.
   apply (@leR_trans (\sum_{C} f * log (\sum_{C} f / \sum_{D} g))).
     case/Rle_lt_or_eq_dec : pos_F => pos_F; last first.
-      rewrite -pos_F !mul0R; exact/leRR.
+      by rewrite -pos_F !mul0R; exact/leRR.
     have H2 : 0 <= \sum_(a | a \in D) g a.
       by apply: sumR_ge0 => ? _; exact: nneg_finfun_ge0.
     case/Rle_lt_or_eq_dec : H2 => H2; last first.
@@ -186,7 +184,7 @@ suff : \sum_{D} f * log (\sum_{D} f / \sum_{D} g) <=
   rewrite (_ : \sum_(_ | _ \in D') _ = 0); last first.
     transitivity (\sum_(a | a \in D') 0).
       apply eq_bigr => a.
-      rewrite /D' in_set => /andP[a_C /eqP ->]; by rewrite mul0R.
+      by rewrite /D' in_set => /andP[a_C /eqP ->]; rewrite mul0R.
     by rewrite big_const iter_addR mulR0.
   by rewrite add0R; exact/leRR.
 apply log_sum1 => // a.

diff --git a/probability/pinsker.v b/probability/pinsker.v
@@ -74,13 +74,7 @@ rewrite !(derive_pt_minus,derive_pt_plus,derive_pt_comp,derive_pt_ln,derive_pt_c
 rewrite !(mul0R,mulR0,addR0,add0R,Rminus_0_l) /= (_ : INR 2 = 2) //.
 rewrite /pinsker_fun' /div_fct [X in _ = X]mulRBr.
 f_equal; last by field.
-rewrite (_ : id q = q) //.
-rewrite Rinv_Rdiv; last 2 first.
-  move=> ?; lra.
-  move=> ?; lra.
-rewrite Rinv_Rdiv; last 2 first.
-  move=> ?; lra.
-  move=> ?; lra.
+rewrite (_ : id q = q)// 2!Rinv_div.
 have -> : p * (/ ln 2 * (q / p) * (p * (-1 / q²))) = - (p / q) * / ln 2.
   rewrite !mulRA /Rsqr.
   field.
@@ -92,7 +86,7 @@ have -> : (1 - p) * (/ ln 2 * ((1 - q) / (1 - p)) * (- (-1 * (1 - p)) / (1 - q)
   split; [exact/eqP/ln2_neq0 | split => ?; lra].
 rewrite /inv_fct.
 field.
-split; [exact/eqP/ln2_neq0 | split => ?; lra].
+by split; [exact/eqP/ln2_neq0 | split => ?; lra].
 Qed.
 
 Definition pinsker_function_spec c q := - log (1 - q) - 4 * c * q ^ 2.
@@ -229,7 +223,7 @@ have X : 0 <= (/ (t * (1 - t) * ln 2) - 8 * c).
     by apply/gtR_eqF/mulR_gt0; lra.
     exact/ln2_neq0.
   apply leR_wpmul2r => //.
-  rewrite -(invRK 4); last exact/eqP.
+  rewrite -(invRK 4).
   apply leR_inv => //.
     by apply/mulR_gt0 => //; lra.
   exact: x_x2_max.
@@ -270,7 +264,7 @@ have X : 0 <= (/ (t * (1 - t) * ln 2) - 8 * c).
     by apply leR_wpmul2r => //; lra.
   rewrite invRM //; last exact/ln2_neq0.
   apply leR_wpmul2r => //.
-  rewrite -(invRK 4) //=; last exact/eqP.
+  rewrite -(invRK 4) //=.
   apply leR_inv => //.
     by apply/mulR_gt0; lra.
   exact: x_x2_max.