fix extraction (based on the analysis PR that deprecates Rinvx)

coq-infotheo.opam

@@ -27,8 +27,8 @@ depends: [
   "coq-mathcomp-algebra" { (>= "2.3.0") }
   "coq-mathcomp-solvable" { (>= "2.3.0") }
   "coq-mathcomp-field" { (>= "2.3.0") }
-  "coq-mathcomp-analysis" { (>= "1.7.0") }
-  "coq-mathcomp-reals-stdlib" { (>= "1.7.0") }
+  "coq-mathcomp-analysis" { (>= "1.9.0") }
+  "coq-mathcomp-reals-stdlib" { (>= "1.9.0") }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-mathcomp-algebra-tactics" { >= "1.2.0" }
   "coq-interval" { >= "4.10.0"}

ecc_modern/ldpc_algo.v

@@ -197,7 +197,11 @@ Extract Constant Rdefinitions.Rmult => "( *.)".
 Extract Constant Rdefinitions.Rplus => "(+.)".
 Extract Constant Rdefinitions.Rinv  => "fun x -> 1. /. x".
 Extract Constant Rdefinitions.Ropp  => "(~-.)".
-Extraction "extraction/sumprod.ml" sumprod estimation.
+
+Definition sumprod_ext := Eval compute in sumprod.
+Definition estimation_ext := Eval compute in estimation.
+
+Extraction "extraction/sumprod.ml" sumprod_ext estimation_ext.
 
 Section ToGraph.
 

extraction/sumprod_test.ml

@@ -1,6 +1,9 @@
 (* #load "sumprod.cmo" *)
 open Sumprod;;
 
+let sumprod = sumprod_ext
+let estimation = estimation_ext
+
 let rabst = RbaseSymbolsImpl.coq_Rabst
 let rrepr = RbaseSymbolsImpl.coq_Rrepr
 

information_theory/entropy_convex.v

@@ -4,7 +4,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import ring.
 From mathcomp Require boolp.
-From mathcomp Require Import mathcomp_extra Rstruct reals set_interval.
+From mathcomp Require Import mathcomp_extra Rstruct reals interval_inference.
+From mathcomp Require Import set_interval.
 From mathcomp Require Import functions topology normedtype realfun derive exp.
 From mathcomp Require convex.
 Require Import ssr_ext ssralg_ext bigop_ext realType_ext realType_ln.
@@ -251,10 +252,10 @@ From mathcomp Require Import -(notations) convex.
 
 (* TODO: introduce two notations and make two conventions more symmetric *)
 Definition prob_itv (p : {prob R}) :
-  itv.Itv.def R `[(ssrint.Posz 0), (ssrint.Posz 1)].
+  Itv.def (@Itv.num_sem R) (Itv.Real `[(ssrint.Posz 0), (ssrint.Posz 1)]).
 Proof.
-apply (@itv.Itv.Def _ _ (p.~)).
-rewrite /itv.Itv.itv_cond.
+exists p.~ => /=; apply/andP; split.
+  by rewrite num_real.
 by rewrite in_itv /=; apply/andP; split.
 Defined.
 

information_theory/string_entropy.v

@@ -1,7 +1,7 @@
 (* infotheo: information theory and error-correcting codes in Coq             *)
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
-From mathcomp Require Import classical_sets reals exp itv.
+From mathcomp Require Import classical_sets reals exp interval_inference.
 From mathcomp Require convex.
 Require Import ssr_ext ssralg_ext realType_ext realType_ln.
 Require Import fdist entropy convex jensen num_occ.
@@ -39,18 +39,21 @@ Import (canonicals) analysis.convex.
 Variable R : realType.
 
 Definition i01_of_prob : {prob R} -> {i01 R}.
-case => p H. exists p.
-abstract (by case/andP: H => H0 H1; apply/andP; split).
+case => p H; exists p => /=.
+by apply/andP; split => //; exact: num_real.
 Defined.
 Definition prob_of_i01 : {i01 R} -> {prob R}.
-case => p H. exists p.
-abstract (by case/andP: H => H0 H1; apply/andP; split).
+by case => p /andP[_ H]; exists p => //.
 Defined.
 
 Lemma i01_of_probK : cancel i01_of_prob prob_of_i01.
-Proof. case => p H. by apply/val_inj. Qed.
+Proof.
+by case => p H /=; case: (elimTF _ _) => /= _ ?; exact/val_inj.
+Qed.
 Lemma prob_of_i01K : cancel prob_of_i01 i01_of_prob.
-Proof. case => p H. by apply/val_inj. Qed.
+Proof.
+by case=> p H/=; case: (elimTF _ _) => _ ?; apply/val_inj.
+Qed.
 
 Lemma mc_convE (a b : R^o) (p : {prob R}) :
   conv p a b = mathcomp.analysis.convex.conv (i01_of_prob p) b a :> R^o.

lib/coqRE.v

@@ -16,20 +16,6 @@ Delimit Scope R_scope with coqR.
 Lemma R1E : 1%coqR = 1%mcR. Proof. by []. Qed.
 Lemma R0E : 0%coqR = 0%mcR. Proof. by []. Qed.
 
-(* NB: PR https://github.com/math-comp/analysis/pull/1461 in progress in MCA *)
-Lemma RsqrtE' (x : Rdefinitions.R) : sqrt x = Num.sqrt x.
-Proof.
-set Rx := Rcase_abs x.
-have RxE: Rx = Rcase_abs x by [].
-rewrite /sqrt.
-rewrite -RxE.
-move: RxE.
-case: Rcase_abs=> x0 RxE.
-  by rewrite RxE; have/RltP/ltW/ler0_sqrtr-> := x0.
-rewrite /Rx -/(sqrt _) RsqrtE //.
-by have/Rge_le/RleP:= x0.
-Qed.
-
 Definition coqRE :=
   (R0E, R1E, INRE, IZRposE,
-    RinvE, RoppE, RdivE, RminusE, RplusE, RmultE, RpowE, RsqrtE').
+    RinvE, RoppE, RdivE, RminusE, RplusE, RmultE, RpowE, RsqrtE).

lib/realType_ln.v

@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later            *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import reals signed topology normedtype derive.
 From mathcomp Require Import sequences exp realfun.
 Require Import ssralg_ext realType_ext derive_ext.
 
@@ -329,7 +329,7 @@
 (* TODO: PR to analysis *)
 Lemma ltr0_derive1_decr (R : realType) (f : R -> R) (a b : R) :
   (forall x, x \in `]a, b[%R -> derivable f x 1) ->
-  (forall x, x \in `]a, b[%R -> f^`() x < 0) ->
+  (forall x, x \in `]a, b[%R -> (f^`())%classic x < 0) ->
   {within `[a, b], continuous f}%classic ->
   forall x y, a <= x -> x < y -> y <= b -> f y < f x.
 Proof.
@@ -339,10 +339,10 @@
   by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
 have itvWlt : {subset `]x, y[%R <= `]a, b[%R}.
   by apply subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
-have fdrv z : z \in `]x, y[%R -> is_derive z 1 f (f^`()z).
+have fdrv z : z \in `]x, y[%R -> is_derive z 1 f (f^`() z)%classic.
   rewrite in_itv/= => /andP[xz zy]; apply: DeriveDef; last by rewrite derive1E.
   by apply: fdrvbl; rewrite in_itv/= (le_lt_trans _ xz)// (lt_le_trans zy).
-have [] := @MVT _ f (f^`()) x y xlty fdrv.
+have [] := @MVT _ f (f^`())%classic x y xlty fdrv.
   apply: (@continuous_subspaceW _ _ _ `[a, b]); first exact: itvW.
   by rewrite continuous_subspace_in.
 move=> t /itvWlt dft dftxy; rewrite -oppr_lt0 opprB dftxy.
@@ -352,7 +352,7 @@
 (* TODO: PR to analysis *)
 Lemma gtr0_derive1_incr (R : realType) (f : R -> R) (a b : R) :
   (forall x, x \in `]a, b[%R -> derivable f x 1) ->
-  (forall x, x \in `]a, b[%R -> 0 < f^`() x) ->
+  (forall x, x \in `]a, b[%R -> 0 < (f^`())%classic x) ->
   {within `[a, b], continuous f}%classic ->
   forall x y, a <= x -> x < y -> y <= b -> f x < f y.
 Proof.

meta.yml

@@ -80,12 +80,12 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.7.0") }'
+    version: '{ (>= "1.9.0") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
     name: coq-mathcomp-reals-stdlib
-    version: '{ (>= "1.7.0") }'
+    version: '{ (>= "1.9.0") }'
   description: |-
     [MathComp analysis reals standard library](https://github.com/math-comp/analysis)
 - opam: