Revise use of numerical occurrence selectors

Numerical occurrence selectors such as {1 3}, {-2} or {7}, which convenient during proof development, can be fragile. Context patterns (possibly in combination with the set and rewrite / tactics) provide a more declarative and robust alternative. Thus, as a rule, numerical selectors should not appear in library scripts, except perhaps in the rewrite {1}rule efficiency workaround, or if the context pattern alternative is much too verbose. It would be advisable to review all uses of numerical selectors in mathcomp; this has already been done successfully for all negative selectors ({-n}) as part of #434.

@ggonthier should this be done before the upcoming release or can it wait for the next one?

@amahboubi this can definitely wait for a future version, but is something we should eventually do - hence the issue.

Agreed, thanks.

Side question: while writing #434 did you perceive the need of more shapes of contextual patterns than what currently available? Similarly variants of set? (personally I'm not a big fan of set A :=B; rewrite [somewhere]/A but I have no great ideas).

I was mostly getting rid of negative selectors, and in a few cases having some form of negative pattern would have made it easier to avoid the set; rewrite [..]/.. idiom, which by the way seems to fail mysteriously when the pattern selects exactly the variable to rewrite, i.e., set n := m; rewrite [n in 2 + n]/n fails on a goal 2 + m = m.+2, although set n := m; rewrite [in n in 2 + n]/n does work. Likewise, some way to specify multiple patterns would have saved some extra rewrite -[..]/...

I wish to write patterns before -> and <- in intro patterns (e.g., move=> [in RHS]<-). This enhancement would be useful to address this issue without lengthening proof scripts too much. For example: https://github.com/math-comp/math-comp/blob/bd308dab655e37275afc3fd33ed80cb73647a9ae/mathcomp/ssreflect/ssrnat.v#L573-L574

Enrico's remark: move=> [in RHS]<- is syntactically ambiguous with that destruct the top element of stack into in and RHS then perform <-.

We could parse {occ[pat]}-> or ever {occ}[pat]->. The best is probably to force the curly braces even if no occurrence has to be specified as {}[pat]-> that is long, but not semantically too bizarre, since {}E means rewrite and clear, pretty much like -> (or more explicitly {}->).

PR #504 partially fixes this issue.

There are other directories to process.

In order to process the other directories as a collective effort, could you share the small tools (sed, perl scripts, patterns to be grepped, etc.) or ideas you used to process the ssreflect directory?

We'll advertise them on Zulip so that efforts can be shared.

For example, what about this short guide for future contributors to this issue:

--

The main job (w.r.t. the goal of issue #436) is the following one:

• replace numerical occurrence selectors as {1} or {3}[x] with contextual patterns such [LHS], [in LHS], [x in RHS], [_.+1 in LHS], [x %% _], [n in _ * n.+1], etc.
  • it is not a big problem if lines get longer and even if sometimes they need to be split (it looks like it seldom happens)
• remove numerical occurrence selectors when possible
• numerical occurrence selectors can be tolerated in intro patterns (it looks like it seldom happens)

The fact is that, by doing this job, you run into other things you may want to improve:

• removals (when possible):
  • spurious /=, eqxx, =>
  • symmetry tactic
  • useless unfolds
• shortenings:
  • apply/A/B instead of apply: A; apply: B
  • use lemmas that have been recently introduced when possible (contra lemmas, news lemmas in ssrnat)
• replacements:
  • fst / snd instead of (fun p => p.1) / (fun p => p.2)
  • explicit tactics such as exact of apply instead of auto
  • exact/A instead of by rewrite B (at the beginning of a line of course)

But the most important improvements of all in terms of style is maybe case analysis (and the usage of views):

• favor /andP[] of /eqP (in an intro pattern) over case/andP or move/eqP
• favor have [|] := lemmaP over case: lemmaP => [|]
  • examples of lemmaPs: leqP, ifP, posnP, ltngtP, notations =P, ==
  • in particular, avoid simulating lemmas such as
    • ltngtP with leq_eqVlt / predU1P
    • leqP with leq_total / orP
• favor the use of eqVneq (with or without explicit parameters)
  • instead of =P or x == y
  • instead of playing with eq_sym, if_neg, ifP

In order to process the other directories as a collective effort, could you share the small tools (sed, perl scripts, patterns to be grepped, etc.) or ideas you used to process the ssreflect directory?

In my experience, grepping in Emacs with the pattern {[0-9 -]*[0-9 ]} was useful.