Clean up

coq-community · Oct 13, 2023 · 11a05cc · 11a05cc
1 parent 96329e9
commit 11a05cc
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 21 deletions.
diff --git a/theories/binomialz.v b/theories/binomialz.v
@@ -125,12 +125,10 @@ wlog: m n / n <= 0.
   case: m => m; last by rewrite !binz_neg // mulr0.
   rewrite binz_nat_nat -addrA -opprB opprK.
   case: (ltnP n m) => hnm hwlog.
-  - rewrite bin_small // subzn // binz_nat_nat bin_small ?mulr0 //.
-    by rewrite add1n subnSK // leq_subLR leq_addl.
-  - have {}hnm : (Posz m) - (Posz n.+1) <= 0.
-      by rewrite subr_le0; apply/leqW/hnm.
-    rewrite [in RHS]hwlog // opprD opprK addrA subrr add0r addrAC subrr add0r.
-    by rewrite binz_nat_nat mulrA /exprz /= -exprMn mulrNN mul1r expr1n mul1r.
+    by rewrite bin_small // subzn // binz_nat_nat bin_small ?mulr0; lia.
+  have {}hnm : Posz m - Posz n.+1 <= 0 by rewrite subr_le0; apply/leqW/hnm.
+  rewrite [in RHS]hwlog // subKr addrAC subrr add0r.
+  by rewrite binz_nat_nat mulrA /exprz /= -exprMn mulrNN mul1r expr1n mul1r.
 case: m => m; last by rewrite !binz_neg // mulr0.
 case: n => [n | n _].
   case: n => [_ | //]; case:m => [ | m]; first by rewrite !binz0.
@@ -139,8 +137,7 @@ rewrite [in RHS]NegzE opprK -addrA subzSS subr0.
 move: {2}(m + n)%N (leqnn (m + n)) => k; elim: k n m => [n m|k ihk n m hnm].
   by rewrite leqn0 addn_eq0; case/andP => /eqP -> /eqP ->; rewrite !binz0.
 case: m hnm => [ | m] hnm //; case: n hnm => [ | n] hnm.
-  rewrite bin_1N_posz {}ihk // !addr0 !binz_on_diag /= !mulr1.
-  by rewrite exprSz mulN1r.
+  by rewrite bin_1N_posz {}ihk // !addr0 !binz_on_diag /= !mulr1 exprSz mulN1r.
 rewrite bin_negz_posz ihk; last by move: hnm; rewrite addnS.
 rewrite ihk; last by move: hnm; rewrite addSn.
 rewrite exprSzr -!mulrA !mulN1r -mulrBr; congr (_ * _); rewrite -opprD.
@@ -156,8 +153,8 @@ Lemma binzSS_weak (F : numFieldType) (n k : int) : 0 <= n -> k + 1 != 0 ->
 Proof.
 case: n k => [] // n [k|[|k]] // _ _; last by rewrite !binz_neg // mulr0.
 rewrite -!PoszD !addn1 !binz_nat_nat mulrAC.
-apply: (canRL (mulfK _)); rewrite ?intr_eq0 //.
-by rewrite -!rmorphM -!PoszM /= mul_bin_diag mulnC.
+apply: canRL (mulfK _) _; rewrite ?intr_eq0 //.
+by rewrite -!intrM -!PoszM mul_bin_diag mulnC.
 Qed.
 
 Lemma binzS_weak (F : numFieldType) (n k : int) : n >= 0 -> k + 1 != 0 ->

diff --git a/theories/hanson.v b/theories/hanson.v
@@ -318,34 +318,31 @@ have -> : w_seq 4 = a' 0 * a' 1 * a' 2 * a' 3.
 have a'0_ubP : a' 0 <= a'0_ub%:C.
   have ge0a'0 : 0 <= a'0_ub%:C by rewrite ler0q divr_ge0.
   rewrite root_le_x // a0 -rmorphXn ler_rat exprMn exprVn.
-  rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl.
-  by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z.
+  by rewrite lter_pdivlMr; ring_lia.
 have a'1_ubP : a' 1 <= a'1_ub%:C.
   have ge0a'1 : 0 <= a'1_ub%:C by rewrite ler0q divr_ge0.
   rewrite root_le_x // a1 -rmorphXn ler_rat exprMn exprVn.
-  rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl.
-  by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z.
+  by rewrite lter_pdivlMr; ring_lia.
 have a'2_ubP : a' 2 <= a'2_ub%:C.
   have ge0a'2 : 0 <= a'2_ub%:C by rewrite ler0q divr_ge0.
   have ge0a2 : 0 <= (a 2)%:Q%:C by rewrite ler0q.
   rewrite root_le_x // a2 -rmorphXn ler_rat exprMn exprVn.
-  rewrite lter_pdivlMr ?exprn_gt0 // -subr_ge0 mulrzl.
-  by rewrite -!rmorphXn -rmorphMz -rmorphB /= rat_of_ZEdef ler0z.
+  by rewrite lter_pdivlMr; ring_lia.
 have a'3_ubP : a' 3 <= a'3_ub%:C.
   have ge0a'3 : 0 <= a'3_ub%:C by rewrite ler0q divr_ge0.
   have ge0a3 : 0 <= (a 3)%:Q%:C by rewrite ler0q.
   rewrite root_le_x // a3 -rmorphXn ler_rat exprMn exprVn.
-  rewrite lter_pdivlMr; last exact: exprn_gt0.
-  rewrite -subr_ge0 mulrzl -!rmorphXn -rmorphMz -rmorphB /=.
-  by rewrite rat_of_ZEdef ler0z.
+  by rewrite lter_pdivlMr; ring_lia.
 have a'4_ubP : a' 4 <= a'4_ub%:C.
   have ge0a'1 : 0 <= a'4_ub%:C by rewrite ler0q divr_ge0.
   have ge0a4 : 0 <= (a 4)%:Q%:C by rewrite ler0q ler0z.
   rewrite root_le_x //.
   pose t : rat := (rat_of_Z 200)^-1.
   have -> : a'4_ub = 1 + t by rewrite /a'4_ub /t; field.
   rewrite -rmorphXn ler_rat a4 exprDn.
-  have -> : (1808 = 8 + 1800)%N by [].
+  (* FIXME: *)
+  (* have -> : (1808 = 8 + 1800)%N by []. *)
+  change 1808%N with (8 + 1800)%N.
   rewrite big_split_ord /=; apply: ler_wpDr.
     apply: sumr_ge0 => i.
     by rewrite expr1n mul1r mulrn_wge0 ?exprn_ge0 ?invr_ge0.
@@ -500,7 +497,7 @@ have -> : forall k1, exp_quo n%:Q (n * (a k1.+1).-2) (a k1.+1).-1
   - by rewrite muln_gt0 /= muln_gt0; apply/andP.
   - by rewrite muln_gt0 andbT muln_gt0; apply/andP.
   lia.
-rewrite /w_seq /t10n_to rmorphXn -subn1 -prod_is_exp_sum.
+rewrite /w_seq /t10n_to [in RHS]rmorphXn -subn1 -prod_is_exp_sum.
 rewrite -3!mulrA ![_ * (_%:C * _)]mulrCA; congr (_ * _).
 rewrite -prodrXl -!prodfV -!big_split /=; apply: eq_bigr => i _.
 rewrite -exprM mul1n [_^-1 / _ in RHS]mulrC [RHS]mulrA [RHS]mulrACA.