Tuning simplifications using Arguments simpl nomatch

7 files changed, 26 insertions, 0 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f2ba40b..4de594e 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -294,6 +294,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `path.v`, added `size_merge_sort_push`, which documents an
   invariant of `merge_sort_push`.
 
+- in `seq.v ` added lemma `mask0s`.
+
 ### Changed
 
 - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12
@@ -374,6 +376,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `order.v`, generalized `sort_le_id` for any `porderType`.
 
+- the following constants have been tuned to only reduce when they do
+  not expose a match: `subn_rec`, `decode_rec`, `nth` (thus avoiding a
+  notorious problem of ``p`_0`` expanding too eagerly), `set_nth`,
+  `take`, `drop`, `eqseq`, `incr_nth`, `elogn2`, `binomial_rec`,
+  `sumpT`.
+
+- in `seq.v`, `mask` will only expand if both arguments are
+  constructors, the case `mask [::] s` can be dealt with using
+  `mask0s` or explicit conversion.
+
 ### Renamed
 
 - `big_rmcond` -> `big_rmcond_in` (cf Changed section)
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 24b764b..4ee11f3 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -194,6 +194,7 @@ Proof. by move=> a n; elim: n a=> [a /= -> //|n ihn a ra]; apply: ihn. Qed.
 Fixpoint sumpT (p q : polyF) :=
   match p, q with a :: p, b :: q => (a + b)%T :: sumpT p q
                 | [::], q => q | p, [::] => p end.
+Arguments sumpT : simpl nomatch.
 
 Lemma eval_sumpT (p q : polyF) (e : seq F) :
   eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index cd3ec87..02d2e48 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -178,6 +178,7 @@ Fixpoint binomial_rec n m :=
   | _, 0 => 1
   | 0, _.+1 => 0
   end.
+Arguments binomial_rec : simpl nomatch.
 
 Definition binomial := nosimpl binomial_rec.
 
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index a68ec41..81b83dc 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -76,6 +76,7 @@ Fixpoint decode_rec (v q r : nat) {struct q} :=
   | q'.+1, 1     => [rec v.+1, q', q']
   | q'.+1, r'.+2 => [rec v, q', r']
   end where "[ 'rec' v , q , r ]" := (decode_rec v q r).
+Arguments decode_rec : simpl nomatch.
 
 Definition decode n := if n is 0 then [::] else [rec 0, n.-1, n.-1].
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index ab8edce..ee5b136 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -76,6 +76,7 @@ Fixpoint elogn2 e q r {struct q} :=
   | q'.+1, 1 => elogn2 e.+1 q' q'
   | q'.+1, r'.+2 => elogn2 e q' r'
   end.
+Arguments elogn2 : simpl nomatch.
 
 Variant elogn2_spec n : nat * nat -> Type :=
   Elogn2Spec e m of n = 2 ^ e * m.*2.+1 : elogn2_spec n (e, m).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 3d56831..347a671 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -909,6 +909,10 @@ Arguments seqn {T} n.
 Prenex Implicits cat take drop rot rotr catrev.
 Prenex Implicits find count nth all has filter.
 Arguments rev {T} s : simpl never.
+Arguments nth : simpl nomatch.
+Arguments set_nth : simpl nomatch.
+Arguments take : simpl nomatch.
+Arguments drop : simpl nomatch.
 
 Arguments nilP {T s}.
 Arguments all_filterP {T a s}.
@@ -1463,6 +1467,7 @@ Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) ->
 Proof. by move=> ?; rewrite eq_sym uniq_eqseq_pivotl//; case: eqVneq => /=. Qed.
 
 End EqSeq.
+Arguments eqseq : simpl nomatch.
 
 Section RotIndex.
 Variables (T : eqType).
@@ -1581,6 +1586,7 @@ End FindNth.
 Fixpoint incr_nth v i {struct i} :=
   if v is n :: v' then if i is i'.+1 then n :: incr_nth v' i' else n.+1 :: v'
   else ncons i 0 [:: 1].
+Arguments incr_nth : simpl nomatch.
 
 Lemma nth_incr_nth v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j.
 Proof.
@@ -1978,6 +1984,8 @@ Proof. by elim: s n => [|x s IHs] [|n] //= Hn; congr (_ :: _); apply: IHs. Qed.
 Lemma mask0 m : mask m [::] = [::].
 Proof. by case: m. Qed.
 
+Lemma mask0s s : mask [::] s = [::]. Proof. by []. Qed.
+
 Lemma mask1 b x : mask [:: b] [:: x] = nseq b x.
 Proof. by case: b. Qed.
 
@@ -2026,6 +2034,7 @@ by elim: s m => [|x s IHs] [|b m] //=; rewrite (mask_false, IHs).
 Qed.
 
 End Mask.
+Arguments mask _ !_ !_.
 
 Section EqMask.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index dcb518f..8dbfc73 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -260,6 +260,7 @@ Lemma add4n m : 4 + m = m.+4. Proof. by []. Qed.
 (* Further properties depend on ordering conditions.                  *)
 
 Definition subn_rec := minus.
+Arguments subn_rec : simpl nomatch.
 Notation "m - n" := (subn_rec m n) : nat_rec_scope.
 
 Definition subn := nosimpl subn_rec.