Merge pull request #1921 from proux01/reworder

proux01 · web-flow · commit bd05c57283ab · 2026-03-27T15:38:48.000+01:00
Port last files to new rewrite goals order
diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v
@@ -17,7 +17,7 @@ From mathcomp Require normedtype sequences.
 (* The following line is for RlnE. *)
 From mathcomp Require exp.
 
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v
@@ -5,7 +5,7 @@ From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssr
 From mathcomp Require Import boolp reals Rstruct_topology ereal classical_sets.
 From mathcomp Require Import interval_inference topology normedtype landau.
 
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/classical/boolp.v b/classical/boolp.v
@@ -73,6 +73,7 @@ From mathcomp Require internal_Eqdep_dec.
 (*                                                                            *)
 (******************************************************************************)
 
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set   Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/experimental_reals/discrete.v b/experimental_reals/discrete.v
@@ -11,7 +11,7 @@ From mathcomp.classical Require Import boolp.
 From mathcomp Require Import xfinmap reals.
 
 (* -------------------------------------------------------------------- *)
-Set   SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set   Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/experimental_reals/xfinmap.v b/experimental_reals/xfinmap.v
@@ -7,7 +7,7 @@
 From mathcomp Require Import all_ssreflect_compat all_algebra.
 From mathcomp Require Export finmap.
 
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -139,7 +139,7 @@ Lemma big_nat_mkfset (F : nat -> R) n :
 Proof.
 rewrite -(big_map val xpredT) /=; apply/perm_big.
 apply/uniq_perm; rewrite ?iota_uniq //.
-  rewrite map_inj_uniq /=; last apply/val_inj.
+  rewrite map_inj_uniq /=; first apply/val_inj.
   by rewrite /index_enum -enumT enum_uniq.
 by move=> i; rewrite /index_enum -enumT -enum_fsetE in_fset /index_iota subn0.
 Qed.
diff --git a/reals/reals.v b/reals/reals.v
@@ -52,7 +52,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
 Declare Scope real_scope.
 
 (* -------------------------------------------------------------------- *)
-Set   SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set   Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -349,7 +349,7 @@ Lemma inf_sumE (A B : set R) :
 Proof.
 move/has_inf_supN => ? /has_inf_supN ?; rewrite /inf.
 rewrite [X in - sup X = _](_ : _ =
-    [set x + y | x in [set - x | x in A ] & y in [set - x | x in B]]).
+    [set x + y | x in [set - x | x in A ] & y in [set - x | x in B]]); last first.
   by rewrite sup_sumE // -opprD.
 rewrite eqEsubset; split => /= t [] /= x []a Aa.
   case => b Bb <- <-; exists (- a); first by exists a.
@@ -607,9 +607,9 @@ have [supA|supNA] := pselect (has_sup A); last first.
   by rewrite !sup_out // => /has_sup_down.
 have supDA : has_sup (down A) by apply/has_sup_down.
 apply/eqP; rewrite eq_le !sup_le //.
+- by case: supA => -[x xA] _; exists x; apply/le_down.
 - by rewrite downK; exact: le_down.
 - by case: supA.
-- by case: supA => -[x xA] _; exists x; apply/le_down.
 Qed.
 
 Lemma lt_sup_imfset {T : Type} (F : T -> R) l :
diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v
@@ -39,7 +39,7 @@ the economic rights, and the successive licensors have only limited
 liability. See the COPYING file for more details.
 *)
 
-Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -284,7 +284,7 @@ apply/RltbP/Rabs_def1.
   apply: (Rlt_le_trans _ (IZR (up x)))=> //.
   elim/(well_founded_ind (Zwf_well_founded 0)): (up x) => z IHz.
   case: (Z_lt_le_dec 0 z) => [zp | zn].
-    rewrite [z]Hz plus_IZR Zabs_nat_Zplus //; last exact: Zlt_0_le_0_pred.
+    rewrite [z]Hz plus_IZR Zabs_nat_Zplus //; first exact: Zlt_0_le_0_pred.
     rewrite plusE mulrnDr.
     apply/Rplus_le_compat_r/IHz; split; first exact: Zlt_le_weak.
     exact: Zlt_pred.
@@ -296,7 +296,7 @@ apply: (Rlt_le_trans _ (IZR (up x) - 1)).
   elim/(well_founded_ind (Zwf_well_founded 0)): (- up x)%Z => z IHz .
   case: (Z_lt_le_dec 0 z) => [zp | zn].
   rewrite [z]Hz Zabs_nat_Zopp plus_IZR.
-  rewrite Zabs_nat_Zplus //; last exact: Zlt_0_le_0_pred.
+  rewrite Zabs_nat_Zplus //; first exact: Zlt_0_le_0_pred.
     rewrite plusE -Rplus_assoc -addnA [(_ + 2)%N]addnC addnA mulrnDr.
     apply: Rplus_lt_compat_r; rewrite -Zabs_nat_Zopp.
     apply: IHz; split; first exact: Zlt_le_weak.
@@ -503,7 +503,7 @@ Proof. by rewrite -Pos_to_natE INR_IPR. Qed.
 Let ge0_RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
 Proof.
 move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
-rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last exact/RleP.
+rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; first exact/RleP.
 by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP.
 Qed.
 
@@ -584,10 +584,10 @@ Proof.
 #[warning="-deprecated"]
 rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i).
   #[warning="-deprecated"]
-  case: s => // ? t; rewrite big_cons /bigmaxr.
-  by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
+  by case: s => //=; rewrite /bigmaxr big_nil.
 #[warning="-deprecated"]
-by case: s => //=; rewrite /bigmaxr big_nil.
+case: s => // ? t; rewrite big_cons /bigmaxr.
+by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
 Qed.
 
 #[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
@@ -753,7 +753,7 @@ Lemma bmaxrf_index n (f : {ffun 'I_n.+1 -> R}) :
 Proof.
 #[warning="-deprecated"]
 rewrite /bmaxrf.
-rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)); last first.
+rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)).
   by rewrite size_codom card_ord.
 #[warning="-deprecated"]
 by apply: bigmaxr_index; rewrite size_codom card_ord.
@@ -777,9 +777,9 @@ move: (bmaxrf_index f).
 rewrite -[X in _ (_ < X)%N]card_ord -(size_codom f) index_mem.
 move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
   #[warning="-deprecated"]
-  by rewrite (ordnat (bmaxrf_index _)) /index_bmaxrf nth_ord_enum.
+  by rewrite size_enum_ord; apply: bmaxrf_index.
 #[warning="-deprecated"]
-by rewrite size_enum_ord; apply: bmaxrf_index.
+by rewrite (ordnat (bmaxrf_index _)) /index_bmaxrf nth_ord_enum.
 Qed.
 
 #[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
diff --git a/reals_stdlib/nsatz_realtype.v b/reals_stdlib/nsatz_realtype.v
@@ -16,6 +16,8 @@ From mathcomp Require Import boolp reals constructive_ereal.
 
 Import GRing.Theory Num.Theory.
 
+Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
+
 Local Open Scope ring_scope.
 
 Section Nsatz_realType.
