Merge pull request #1915 from proux01/classical-rworder

Port classical and reals to new rewrite goal order

Author: proux01

classical/cardinality.v

@@ -38,7 +38,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 (*                                                                            *)
 (******************************************************************************)
 
-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.
@@ -656,7 +656,7 @@ Lemma finite_setX_or T T' (A : set T) (B : set T') :
 Proof.
 have [->|/set0P[a Aa]] := eqVneq A set0; first by left.
 have /sub_finite_set : [set a] `*` B `<=` A `*` B by move=> x/= [] -> ?; split.
-move => /[apply]/(finite_image snd); rewrite (_ : _ @` _ = B); first by right.
+move => /[apply]/(finite_image snd); rewrite (_ : _ @` _ = B); last by right.
 by apply/seteqP; split=> [b [[? ?] [? ?] <-//]|b ?]/=; exists (a, b).
 Qed.
 
@@ -803,7 +803,7 @@ Lemma fset_setU {T : choiceType} (A B : set T) :
   fset_set (A `|` B) = (fset_set A `|` fset_set B)%fset.
 Proof.
 move=> fA fB; apply/fsetP=> x.
-rewrite ?(inE, in_fset_set)//; last by rewrite finite_setU.
+rewrite ?(inE, in_fset_set)//; first by rewrite finite_setU.
 by apply/idP/orP; rewrite ?inE.
 Qed.
 
@@ -812,7 +812,7 @@ Lemma fset_setI {T : choiceType} (A B : set T) :
   fset_set (A `&` B) = (fset_set A `&` fset_set B)%fset.
 Proof.
 move=> fA fB; apply/fsetP=> x.
-rewrite ?(inE, in_fset_set)//; last by apply: finite_setI; left.
+rewrite ?(inE, in_fset_set)//; first by apply: finite_setI; left.
 by apply/idP/andP; rewrite ?inE.
 Qed.
 
@@ -825,7 +825,7 @@ Lemma fset_setD {T : choiceType} (A B : set T) :
   fset_set (A `\` B) = (fset_set A `\` fset_set B)%fset.
 Proof.
 move=> fA fB; apply/fsetP=> x.
-rewrite ?(inE, in_fset_set)//; last exact: finite_setD.
+rewrite ?(inE, in_fset_set)//; first exact: finite_setD.
 by apply/idP/andP; rewrite ?inE => -[]; rewrite ?notin_setE.
 Qed.
 
@@ -894,10 +894,10 @@ Lemma trivIset_sum_card (T : choiceType) (F : nat -> set T) n :
    #|` fset_set (\big[setU/set0]_(k < n) F k)|)%N.
 Proof.
 move=> finF tF; elim: n => [|n ih]; first by rewrite !big_ord0 fset_set0.
-rewrite big_ord_recr//= ih big_ord_recr/= fset_setU//; last first.
+rewrite big_ord_recr//= ih big_ord_recr/= fset_setU//.
   by rewrite -bigcup_mkord; exact: bigcup_finite.
 rewrite cardfsU [X in (_ - X)%N](_ : _  = O) ?subn0// ?EFinD ?natrD//.
-apply/eqP; rewrite cardfs_eq0 -fset_setI//; last first.
+apply/eqP; rewrite cardfs_eq0 -fset_setI//.
   by rewrite -bigcup_mkord; exact: bigcup_finite.
 rewrite (@trivIset_bigsetUI _ xpredT)// ?fset_set0//.
 by rewrite [X in trivIset X F](_ : _ = [set: nat])//; exact/seteqP.
@@ -935,7 +935,7 @@ Lemma fset_set_image {T U : choiceType} (f : T -> U) (A : set T) :
   finite_set A -> fset_set (f @` A) = (f @` fset_set A)%fset.
 Proof.
 move=> Afset; apply/fsetP=> i.
-rewrite !in_fset_set; last exact: finite_image.
+rewrite !in_fset_set; first exact: finite_image.
 apply/idP/imfsetP; rewrite !inE/=.
   by move=> [x Ax <-]; exists x; rewrite ?in_fset_set ?inE.
 by move=> [x + ->]; rewrite in_fset_set// inE; exists x.
@@ -1068,7 +1068,7 @@ Lemma infinite_set_fset {T : choiceType} (A : set T) n :
 Proof.
 elim/choicePpointed: T => T in A *; first by rewrite emptyE.
 move=> /infiniteP/ppcard_leP[f]; exists (fset_set [set f i | i in `I_n]).
-  rewrite fset_setK//; last exact: finite_image.
+  rewrite fset_setK//; first exact: finite_image.
   by apply: subset_trans (fun_image_sub f); apply: image_subset.
 rewrite fset_set_image// card_imfset//= fset_set_II/=.
 by rewrite card_imfset//= ?size_enum_ord//; apply: val_inj.

classical/classical_orders.v

@@ -18,7 +18,7 @@ From mathcomp Require Import functions set_interval.
 (*                                                                            *)
 (******************************************************************************)
 
-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.

classical/classical_sets.v

@@ -217,7 +217,7 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*                                                                            *)
 (******************************************************************************)
 
-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.
@@ -2222,9 +2222,9 @@ Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T}) (f : T -> set U) :
 Proof.
 apply/predeqP => u; split=> [[x Px fxu]|]; first by rewrite (bigD1 x)//; left.
 move=> /mem_set; rewrite (@big_morph _ _ (fun X => u \in X) false orb).
-- by rewrite big_has_cond => /hasP[x _ /andP[xP]]; rewrite inE => ufx; exists x.
 - by move=> /= x y; apply/idP/orP; rewrite !inE.
 - by rewrite in_set0.
+- by rewrite big_has_cond => /hasP[x _ /andP[xP]]; rewrite inE => ufx; exists x.
 Qed.
 
 Section smallest.
@@ -3024,7 +3024,7 @@ Proof. by rewrite /supremum eqxx. Qed.
 
 Lemma supremum1 x0 x : supremum x0 [set x] = x.
 Proof.
-rewrite /supremum ifF; last first.
+rewrite /supremum ifF.
   by apply/eqP; rewrite predeqE => /(_ x)[+ _]; apply.
 by rewrite supremums1; case: xgetP => // /(_ x) /(_ erefl).
 Qed.

classical/contra.v

@@ -2,7 +2,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 From mathcomp Require Import boolp.
 
-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.

classical/filter.v

@@ -169,7 +169,7 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 (*   variable                                                                 *)
 (******************************************************************************)
 
-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.
@@ -1419,7 +1419,7 @@ Lemma in_ultra_setVsetC T (F : set_system T) (A : set T) :
 Proof.
 move=> FU; case: (pselect (F (~` A))) => [|nFnA]; first by right.
 left; suff : ProperFilter (filter_from (F `|` [set A `&` B | B in F]) id).
-  move=> /max_filter <-; last by move=> B FB; exists B => //; left.
+  move=> /max_filter <-; first by move=> B FB; exists B => //; left.
   by exists A => //; right; exists setT; [exact: filterT|rewrite setIT].
 apply: filter_from_proper; last first.
   move=> B [|[C FC <-]]; first exact: filter_ex.

classical/fsbigop.v

@@ -25,7 +25,7 @@ Reserved Notation "\sum_ ( i '\in' A ) F"
   (F at level 41, A at level 60,
     format "'[' \sum_ ( i  '\in'  A ) '/  '  F ']'").
 
-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.
@@ -115,7 +115,7 @@ elim/Peq: R => R in idx op f *.
 move=> Af; have Afin : finite_set (f @^-1` [set~ idx]).
   by apply: (finite_subfset A) => x; apply: contra_notT => /Af.
 rewrite [in RHS](big_fsetID _ [pred x | f x == idx])/=.
-rewrite [X in _ = op X _]big_fset [X in _ = op X _]big1 ?Monoid.simpm//; last first.
+rewrite [X in _ = op X _]big_fset [X in _ = op X _]big1 ?Monoid.simpm//.
   by move=> i /= /eqP.
 apply eq_fbigl => r.
 rewrite in_finite_support// ?setTI// /preimage/=; apply/idP/idP => /=.
@@ -170,7 +170,7 @@ Lemma bigfs (R : Type) (idx : R) (op : Monoid.com_law idx) (T : choiceType)
   \big[op/idx]_(i <- r | P i) f i = \big[op/idx]_(i \in [set` P]) f i.
 Proof.
 move=> r_uniq fidx; rewrite fsbig_mkcond.
-rewrite (fsbigTE [fset x | x in r]%fset); last first.
+rewrite (fsbigTE [fset x | x in r]%fset).
   by move=> i; rewrite inE/= /patch mem_setE; case: ifP=> // + /fidx->.
 rewrite -big_mkcond; under [RHS]eq_bigl do rewrite mem_setE.
 by apply: perm_big; rewrite uniq_perm// => i; rewrite !inE.
@@ -193,7 +193,7 @@ Lemma fsbig_seq (R : Type) (idx : R) (op : Monoid.com_law idx)
   uniq r ->
   \big[op/idx]_(a <- r) F a = \big[op/idx]_(a \in [set` r]) F a.
 Proof.
-move=> ur; rewrite (fsbigE r)//=; last by move=> + ->.
+move=> ur; rewrite (fsbigE r)//=; first by move=> + ->.
 by rewrite mem_setE big_seq_cond big_mkcondr.
 Qed.
 
@@ -262,9 +262,9 @@ have fsbig_setI C : \big[op/idx]_(i <-
     \big[op/idx]_(i \in A `&` C) F i.
   apply: eq_fbigl => i /=; apply/idP/idP.
     rewrite !inE/= => /andP[+ Bi]; rewrite in_fset_set// inE => -[Ai Fi].
-    rewrite unlock in_fset_set ?inE// setIAC; first by rewrite inE in Bi.
+    rewrite unlock in_fset_set ?inE// setIAC; last by rewrite inE in Bi.
     exact/finite_setIl.
-  rewrite unlock in_fset_set; last by rewrite setIAC; exact/finite_setIl.
+  rewrite unlock in_fset_set; first by rewrite setIAC; exact/finite_setIl.
   by rewrite inE => -[[Ai Bi] Fi0]; rewrite !inE/= in_fset_set// !mem_set.
 rewrite (big_fsetID _ [pred i | i \in B])/= [locked_with _ _]unlock.
 rewrite fsbig_setI; congr (op _ _); rewrite -fsbig_setI.
@@ -289,7 +289,7 @@ Lemma fsbigU (R : Type) (idx : R) (op : Monoid.com_law idx)
   \big[op/idx]_(i \in A `|` B) F i =
      op (\big[op/idx]_(i \in A) F i) (\big[op/idx]_(i \in B) F i).
 Proof.
-move=> Afin Bfin AB0; rewrite (fsbigID A) ?finite_setU; last by split.
+move=> Afin Bfin AB0; rewrite (fsbigID A) ?finite_setU; first by split.
 rewrite setUK -setDE; congr (op _ _); rewrite setDE setIUl setICr set0U.
 by apply: fsbig_widen => //; rewrite -setDE setDD setIC.
 Qed.
@@ -320,13 +320,13 @@ move=> finF; elim/Peq : R => R in zero times plus a F finF *.
 have [->|a0] := eqVneq a zero.
   by rewrite Monoid.mul0m fsbig1//; move=> i _; rewrite Monoid.mul0m.
 #[warning="deprecated"] (* FIXME *)
-rewrite big_distrr [RHS](full_fsbigID (F @^-1` [set zero])); last first.
+rewrite big_distrr [RHS](full_fsbigID (F @^-1` [set zero])).
   apply: sub_finite_set finF => x /= [Px aFN0].
   by split=> //; apply: contra_not aFN0 => ->; rewrite Monoid.simpm.
 set b0 := bigop _ _ _.
 set b1 := bigop _ _ _.
 set b2 := bigop _ _ _.
-rewrite (_ : b1 = zero) ?Monoid.simpm; last first.
+rewrite (_ : b1 = zero) ?Monoid.simpm.
   by rewrite /b1 fsbig1// => i [_ ->]; rewrite Monoid.simpm.
 apply/esym/fsbig_fwiden => //.
   by move=> x [Px Fx0]; rewrite /= in_finite_support// inE.

classical/functions.v

@@ -130,7 +130,7 @@ Add Search Blacklist "_mixin_".
 (*                                                                            *)
 (******************************************************************************)
 
-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.
@@ -1148,7 +1148,7 @@ Context {f : {inv aT >-> aT}}.
 Lemma some_iter_inv n : olift (iter n f^-1) = 'oinv_(iter n f).
 Proof.
 elim: n => // n IH; rewrite iterfSr olift_comp IH ?oinv_iter -compA.
-rewrite (_ : Some \o f^-1 = 'oinv_f); first by rewrite iterfSr; congr (_ \o _).
+rewrite (_ : Some \o f^-1 = 'oinv_f); last by rewrite iterfSr; congr (_ \o _).
 by apply/funeqP => ? /=; rewrite some_inv.
 Qed.
 HB.instance Definition _ n := OInv_Inv.Build _ _ (iter n f) (some_iter_inv n).
@@ -1331,7 +1331,7 @@ set g := subfun _; set f := subfun _; apply/funext => x /=.
 apply: 'inj_(oapp f x) => //=.
 - by rewrite inE/=; eexists.
 - by rewrite inE/=; apply: 'oinvS_f; exists (g x) => //; apply/val_inj.
-rewrite oinvK ?inE//=; first exact/val_inj.
+rewrite oinvK ?inE//=; last exact/val_inj.
 by exists (g x) => //; apply/val_inj.
 Qed.
 (* Add a Inj_Can factory *)

classical/internal_Eqdep_dec.v

@@ -75,7 +75,7 @@ exact (fun Streicher_K p P x =>
 Qed.
 End Equivalences.
 
-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.
 
 Section EqdepDec.

classical/mathcomp_extra.v

@@ -15,7 +15,7 @@ From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
 (*                                                                            *)
 (******************************************************************************)
 
-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.

classical/set_interval.v

@@ -38,7 +38,7 @@ From mathcomp Require Import functions.
 (*                                                                            *)
 (******************************************************************************)
 
-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.
@@ -207,7 +207,7 @@ Lemma setUitv_set2 x y b1 b2 :
 Proof.
 rewrite le_eqVlt => /orP [/eqP->|xy].
   by case: b1; case: b2; rewrite !set_itvE !setUid // set0U.
-rewrite setUCA setUitv1; last by case: b1; rewrite bnd_simp// ltW.
+rewrite setUCA setUitv1; first by case: b1; rewrite bnd_simp// ltW.
 by rewrite setU1itv// bnd_simp ltW.
 Qed.