From 2cd9ffa62954d89a0153b372a0816210425f6446 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 19 Jun 2024 14:31:10 +0200 Subject: [PATCH] Adapt to Coq PR #18591: better refolding of addn induces "simpl never" now respected An equality "2%N = (1 + \rank V)%N" was previously leading to "1%N = (\rank V)%N" after injection but with the PR, it respects "simpl never" and only leads to "1%N = (0 + \rank V)%N". So, we add a rewrite of addSn and add0n to recover the previous behavior. This rewrite is additionally made optional so as to preserve the compatibility. Another simplification, in PFsection13.v, gives "1 + (c - 2)" which now needs an extra add1n. --- theories/BGsection2.v | 2 +- theories/PFsection13.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/BGsection2.v b/theories/BGsection2.v index f59dcd4..6c70d3a 100644 --- a/theories/BGsection2.v +++ b/theories/BGsection2.v @@ -897,7 +897,7 @@ have{sU1} [|V Vmod sumUV dxUV] := mx_Maschke _ _ Umod sU1. have [u defU]: exists u : 'rV_2, (u :=: U)%MS. by move: (row_base U) (eq_row_base U); rewrite Uscal => u; exists u. have{dxUV Uscal} [v defV]: exists v : 'rV_2, (v :=: V)%MS. - move/mxdirectP: dxUV; rewrite /= Uscal sumUV mxrank1 => [[Vscal]]. + move/mxdirectP: dxUV; rewrite /= Uscal sumUV mxrank1 ?addSn ?add0n => [[Vscal]]. by move: (row_base V) (eq_row_base V); rewrite -Vscal => v; exists v. pose B : 'M_(1 + 1) := col_mx u v; have{sumUV} uB: B \in unitmx. rewrite -row_full_unit /row_full eqn_leq rank_leq_row {1}addn1. diff --git a/theories/PFsection13.v b/theories/PFsection13.v index 592b56b..8321a44 100644 --- a/theories/PFsection13.v +++ b/theories/PFsection13.v @@ -1282,7 +1282,7 @@ have regCW1: semiregular C W1. have [[_ _ /Frobenius_reg_ker regUW1 _] _ _ _] := FTtypeP_facts maxS StypeP. by move=> _ y /regUW1 regUx; rewrite setIAC regUx setI1g. have{regCW1} dv_2q_c1: q.*2 %| c.-1. - rewrite -(subnKC c_gt1) -mul2n Gauss_dvd ?coprime2n ?dvdn2 ?mFT_odd //=. + rewrite -(subnKC c_gt1) -mul2n Gauss_dvd ?coprime2n ?dvdn2 ?mFT_odd //= ?add1n. rewrite oddB ?mFT_odd -?subSn // subn2 regular_norm_dvd_pred //. have /mulG_sub[_ sW1S] := sdprodW defS. apply: normsI; first by have [_ []] := StypeP.