wip broken

Author: CohenCyril

config.nix

@@ -1,4 +1,4 @@
 {
   coq = "8.10";
-  mathcomp = "CohenCyril/maxr";
+  mathcomp = "1.11.0";
 }

default.nix

@@ -1,9 +1,10 @@
 {
   nixpkgs ? (if builtins.pathExists ./nixpkgs.nix then import ./nixpkgs.nix
-             else fetchTarball https://github.com/CohenCyril/nixpkgs/archive/mathcomp-fix-rec.tar.gz),
+             else fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/72b9660dc18ba347f7cd41a9504fc181a6d87dc3.tar.gz),
   config ? (if builtins.pathExists ./config.nix then import ./config.nix else {}),
   withEmacs ? false,
   print-env ? false,
+  do-nothing ? false,
   package ? (if builtins.pathExists ./package.nix then import ./package.nix else "mathcomp-fast"),
   src ? (if builtins.pathExists ./package.nix then ./. else false)
 }:
@@ -20,6 +21,7 @@ let
         "8.9" = coqPackages_8_9;
         "8.10" = coqPackages_8_10;
         "8.11" = coqPackages_8_11;
+        "8.12" = coqPackages_8_12;
         "default" = coqPackages_8_10;
       }.${(cfg-fun pkgs).coq or "default"}.overrideScope'
         (coqPackages: super-coqPackages:
@@ -39,17 +41,6 @@ let
             mathcomp-extra-config =
               let mec = super-coqPackages.mathcomp-extra-config; in
               lib.recursiveUpdate mec {
-                initial = {
-                  # fixing mathcomp analysis to depend on real-closed
-                  mathcomp-analysis = {version, coqPackages} @ args:
-                    let mca = mec.initial.mathcomp-analysis args; in
-                    mca // (
-                      if elem version [ "master" "cauchy_etoile" "holomorphy" ]
-                      then {
-                        propagatedBuildInputs = mca.propagatedBuildInputs ++
-                                                [coqPackages.mathcomp-real-closed];
-                      } else {});
-                };
                 for-coq-and-mc.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} =
                   (super-coqPackages.mathcomp-extra-config.${coqPackages.coq.coq-version}.${coqPackages.mathcomp.version} or {}) //
                   (removeAttrs cfg [ "mathcomp" "coq" "mathcomp-fast" "mathcomp-full" ]);
@@ -88,16 +79,38 @@ let
       for x in $propagatedBuildInputs; do printf "  "; echo $x | cut -d "-" -f "2-"; done
       echo "you can pass option --arg config '{coq = \"x.y\"; math-comp = \"x.y.z\";}' to nix-shell to change coq and/or math-comp versions"
     }
+
     printEnv () {
       for x in $buildInputs; do echo $x; done
       for x in $propagatedBuildInputs; do echo $x; done
     }
+
     cachixEnv () {
       echo "Pushing environement to cachix"
       printEnv | cachix push math-comp
     }
+
     nixDefault () {
       cat $mathcompnix/default.nix
+    } > default.nix
+
+    updateNixPkgs (){
+      HASH=$(git ls-remote https://github.com/NixOS/nixpkgs-channels refs/heads/nixpkgs-unstable | cut -f1);
+      URL=https://github.com/NixOS/nixpkgs-channels/archive/$HASH.tar.gz
+      SHA256=$(nix-prefetch-url --unpack $URL)
+      echo "fetchTarball {
+        url = $URL;
+        sha256 = \"$SHA256\";
+      }" > nixpkgs.nix
+    }
+    updateNixPkgsMaster (){
+      HASH=$(git ls-remote https://github.com/NixOS/nixpkgs refs/heads/master | cut -f1);
+      URL=https://github.com/NixOS/nixpkgs/archive/$HASH.tar.gz
+      SHA256=$(nix-prefetch-url --unpack $URL)
+      echo "fetchTarball {
+        url = $URL;
+        sha256 = \"$SHA256\";
+      }" > nixpkgs.nix
     }
   ''
   + pkgs.lib.optionalString print-env "nixEnv";
@@ -111,5 +124,12 @@ let
 in
 if pkgs.lib.trivial.inNixShell then pkg.overrideAttrs (old: {
   inherit shellHook mathcompnix;
-  buildInputs = (old.buildInputs or []) ++ pkgs.lib.optional withEmacs emacs;
+  
+  buildInputs = if do-nothing then []
+                else (old.buildInputs ++
+                (if pkgs.lib.trivial.inNixShell then pkgs.lib.optional withEmacs pkgs.emacs
+                 else []));
+
+  propagatedBuildInputs = if do-nothing then [] else old.propagatedBuildInputs;
+
 }) else pkg

theories/polyrcf.v

@@ -171,7 +171,6 @@ Section CauchyBound.
 Definition cauchy_bound (p : {poly R}) :=
   1 + `|lead_coef p|^-1 * \sum_(i < size p) `|p`_i|.
 
-(* Could be a sharp bound *)
 Lemma cauchy_boundP (p : {poly R}) x :
   p != 0 -> p.[x] = 0 -> `| x | < cauchy_bound p.
 Proof.
@@ -746,11 +745,11 @@ rewrite mem_pmap; apply/mapP/idP => [[i i_in /some_eq_iroot[]//]|rpx].
 have xcpoo : x \in cpi.
   apply: subitvP (root_in_cauchy_bound p_neq0 _) => //=.
   by rewrite ler_opp2 andbb le_maxr lexx.
-exists (rindex rs x); first by rewrite mem_iota add0n -lock/= ltnS.
-have rprev_cp : edflt1 0 (rprev rs x) \in cpi.
-  have := map_f (edflt1 0) (in_rprev rs x); rewrite /= inE => /predU1P[->//|].
+exists (rindex rs x); first by rewrite mem_iota add0n -lock/= ltnS rindex_size.
+have rprev_cp : edflt1 0 (aprev rs x) \in cpi.
+  have := map_f (edflt1 0) (in_aprev rs x); rewrite /= inE => /predU1P[->//|].
   by rewrite -map_comp /= map_id => /rscpi.
-have rnext_cp : edflt1 0 (rnext rs x) \in cpi.
+have rnext_cp : edflt1 0 (anext rs x) \in cpi.
   have := map_f (edflt1 0) (in_rnext rs x); rewrite /= inE => /predU1P[->//|].
   by rewrite -map_comp /= map_id => /rscpi.
 apply/some_eq_iroot; split => //; apply: eq_iroot => //; last 1 first.

theories/table.v

@@ -211,16 +211,14 @@ Lemma all_find (s : seq T) : find predT s = 0. Proof. by elim: s. Qed.
 Section lrindex_def.
 Variable (x0 : T) (s : seq T).
 Hypothesis s_sorted : sorted <=%O s.
-(* Let leT_trans := @le_trans _ T. *)
+Let leT_trans := @le_trans _ T.
 
 Notation lindex t := (find (>= t) s).
 Notation rindex t := (find (> t) s).
 
-Print HintDb core.
-
 Lemma eq_count_undup : s = flatten [seq nseq (count_mem x s) x | x <- undup s].
 Proof.
-rewrite (eq_sorted _ le_anti _ _ ((@perm_count_undup _ _)))//.
+rewrite (eq_sorted le_trans le_anti _ _ ((@perm_count_undup _ _)))//.
 have := subseq_sorted le_trans (undup_subseq s) s_sorted.
 elim: (undup) => //= x l ihl; rewrite path_sortedE// => /andP[/allP le_xl l_s].
 elim: (count_mem _ _)=> [|/= k ihk]; rewrite ?path_min_sorted ?ihl//.
@@ -247,7 +245,7 @@ Lemma lindex_le t j : (j < size s)%N -> (lindex t <= j)%N = (t <= nth x0 s j)%O.
 Proof.
 move=> j_lt; set i := find _ _.
 case: (leqP i) => [ij|/(before_find x0)//]; have i_lt := leq_ltn_trans ij j_lt.
-by rewrite (@le_trans _ _ (nth x0 s i)) ?sorted_le_nth ?nth_find ?has_find.
+rewrite (@le_trans _ _ (nth x0 s i)) ?sorted_le_nth ?nth_find ?has_find//.
 Qed.
 
 Lemma lindex_gt t j : (j < size s)%N -> (j < lindex t)%N = (nth x0 s j < t)%O.
@@ -620,12 +618,12 @@ End sorted_mono.
 
 Lemma lindex_eq i : {in [pred t | [i] < t%:x <= [i.+1]], forall t, lindex s t = i}.
 Proof. by move=> t; apply: eq_from_lindex; rewrite gt_sprev le_anext. Qed.
-Print HintDb core.
-Lemma lindex_eq' u : {in [pred t | sprev u < t%:x <= u%:x],
+
+Lemma lindex_eql u : {in [pred t | sprev u < t%:x <= u%:x],
   forall t, lindex s t = lindex s u}.
 Proof.
-move=> t; rewrite inE => /andP[ut tu]; apply: eq_lindex.
-by rewrite  le_anext.
+move=> t; rewrite inE => /andP[ut tu].
+by rewrite (@lindex_eq (lindex s u))// inE ut (le_trans tu)// le_anext.
 Qed.
 
 Lemma rindex_eq i : {in [pred t | [i] <= t%:x < [i.+1]], forall t, rindex s t = i}.
@@ -634,24 +632,24 @@ Proof. by move=> t; apply: eq_from_rindex; rewrite ge_aprev lt_snext. Qed.
 Lemma ext_inF i : {in [pred t | [i] < t%:x < [i.+1]], forall t, t \in s = false}.
 Proof.
 move=> t; rewrite inE => /andP[t_gt t_lt]; have := t_lt.
-
-rewrite -(@lindexE i t); last by rewrite inE t_gt ltW.
-by apply: contraTF => /mem_rnext->; rewrite ltxx.
-Qed.
+(* rewrite -(@lindexE i t); last by rewrite inE t_gt ltW. *)
+(* by apply: contraTF => /mem_rnext->; rewrite ltxx. *)
+Admitted.
 
 Lemma lrindex_notin i :
   {in [pred t | [i] < t%:x < [i.+1]], forall t, t \notin s}.
-Proof. by move=> x /lindex_inF->. Qed.
+Proof. (* by move=> x /lindex_inF->. Qed. *) Admitted.
 
-Lemma lindex_next t tnext : rnext t = tnext%:x -> lindex s tnext = lindex s t.
-Proof. by move=> sneq; apply: lindexE; rewrite inE -sneq lexx andbT. Qed.
+Lemma lindex_next t tnext : anext t = tnext%:x -> lindex s tnext = lindex s t.
+(* Proof. by move=> sneq; apply: lindexE; rewrite inE -sneq lexx andbT. Qed. *)
+Admitted.
 
 End ext_seq.
-End lindex.
+End rindex.
 
 Bind Scope ext_scope with ext.
 Notation edflt1 t := (edflt t t).
 Notation "s `[ i ]" := (nth +oo%x (ext_seq s) i) : ext_scope.
-Notation rprev s t := s`[lindex s t].
-Notation rnext s t := s`[(lindex s t).+1].
-Hint Resolve lrindex_size lrindexP gt_rprev ge_rprev le_rnext lt_rprev_rnext.
+Notation lindex s t := (find (>= t) s).
+Notation rindex s t := (find (> t) s).
+(* Hint Resolve lrindex_size lrindexP gt_rprev ge_rprev le_rnext lt_rprev_rnext. *)