update wrt last mathcomp-analysis

- update opam
- trying to fix extraction

_CoqProject

@@ -94,4 +94,4 @@ toy_examples/expected_value_variance_tuple.v
 toy_examples/conditional_entropy.v
 
 -R . infotheo
--R ../analysis/theories mathcomp.analysis
+

ecc_modern/ldpc_algo.v

@@ -157,6 +157,8 @@ Fixpoint estimation {k} (n : tn_tree' k R2 R2) :=
 
 End Algo.
 
+Require Import Extraction.
+
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive seq => "list" [ "[]" "(::)" ].
@@ -165,6 +167,13 @@ Extract Inductive option => "option" ["Some" "None"].
 Extract Inlined Constant R => "float".
 Extract Inlined Constant R0 => "0.".
 Extract Inlined Constant R1 => "1.".
+Extract Constant RbaseSymbolsImpl.R => "float".
+Extract Constant RbaseSymbolsImpl.R0 => "0.".
+Extract Constant RbaseSymbolsImpl.R1 => "1.".
+Extract Constant ConstructiveCauchyReals.CReal => "float".
+Extract Constant ClassicalDedekindReals.DReal => "float".
+Extract Constant ClassicalDedekindReals.DRealQlim => "Obj.magic".
+Extract Constant ClassicalDedekindReals.DRealAbstr => "(fun x -> x)".
 Extract Constant Rmult => "( *.)".
 Extract Constant Rplus => "(+.)".
 Extract Constant Rinv  => "fun x -> 1. /. x".

opam

@@ -25,9 +25,9 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {(>= "8.10" & < "8.12~"}
+  "coq" {>= "8.10" & < "8.12~"}
   "coq-mathcomp-field" {>= "1.11" & < "1.12~"}
-  "coq-mathcomp-analysis"   {(>= "0.2.0" & <= "0.2.3")}
+  "coq-mathcomp-analysis"   {>= "0.3.0" & <= "0.3.1"}
 ]
 synopsis: "Infotheo"
 description: """
@@ -39,5 +39,5 @@ tags: [
   "keyword: probability"
   "keyword: error-correcting codes"
   "logpath:infotheo"
-  "date:2020-03-21"
+  "date:2020-05-26"
 ]

probability/necset.v

@@ -1072,9 +1072,9 @@ Definition pre_pre_conv (X Y : necset A) (p : prob) : set A :=
 Lemma pre_pre_conv_convex X Y p : is_convex_set (pre_pre_conv X Y p).
 Proof.
 apply/asboolP => u v q.
-rewrite -in_setE; rewrite inE => /asboolP [] x0 [] y0 [] x0X [] y0Y ->.
-rewrite -in_setE; rewrite inE => /asboolP [] x1 [] y1 [] x1X [] y1Y ->.
-rewrite -in_setE convACA inE asboolE.
+rewrite -in_setE => /asboolP [] x0 [] y0 [] x0X [] y0Y ->.
+rewrite -in_setE => /asboolP [] x1 [] y1 [] x1X [] y1Y ->.
+rewrite -in_setE convACA asboolE.
 exists (x0 <|q|> x1), (y0 <|q|> y1).
 split; [exact: mem_convex_set | split; [exact: mem_convex_set | by []]].
 Qed.
@@ -1085,7 +1085,7 @@ Proof.
 case/set0P: (neset_neq0 X) => x; rewrite -in_setE => xX.
 case/set0P: (neset_neq0 Y) => y; rewrite -in_setE => yY.
 apply/set0P; exists (x <| p |> y); rewrite -in_setE.
-by rewrite inE asboolE; exists x, y.
+by rewrite asboolE; exists x, y.
 Qed.
 Definition conv p X Y : necset A := locked
   (NECSet.Pack (NECSet.Class (CSet.Class (pre_pre_conv_convex X Y p))
@@ -1118,11 +1118,11 @@ rewrite/conv; unlock; apply/necset_ext => /=; apply eqEsubset => a; case => x []
 - move=> y [] xX [].
   rewrite in_setE => -[] y0 [] z0 [] y0Y [] z0Z -> ->.
   exists (x <| [r_of p, q] |> y0), z0.
-  by rewrite inE asboolE /= convA; split; try exists x, y0.
+  by rewrite asboolE /= convA; split; try exists x, y0.
 - move=> z []; rewrite in_setE => -[] x0 [] y [] x0X [] yY -> [] zZ ->.
   exists x0, (y <| q |> z).
   split => //.
-  by rewrite inE asboolE /= -convA; split; try exists y, z.
+  by rewrite asboolE /= -convA; split; try exists y, z.
 Qed.
 Definition mixin : ConvexSpace.mixin_of _ :=
   @ConvexSpace.Mixin _ conv conv1 convmm convC convA.
@@ -1318,12 +1318,11 @@ apply neset_ext => /=.
 apply eqEsubset=> i /=.
 - move/set0P: (set1_neq0 x)=> Hx.
   move/set0P: (set1_neq0 y)=> Hy.
-  move/(@hull_setU _ _ (necset1 x) (necset1 y) Hx Hy)=> [] a.
-  rewrite inE=> /asboolP ->.
-  case=> b; rewrite inE=> /asboolP ->.
+  move/(@hull_setU _ _ (necset1 x) (necset1 y) Hx Hy)=> [] a /asboolP ->.
+  case=> b /asboolP ->.
   case=> p ->.
   by eexists.
 - case=> p ? <-.
-  by apply/mem_hull_setU.
+  exact/mem_hull_setU.
 Qed.
 End technical_corollaries.