nonterminal simp then rfl

Stream: mathlib4

[Bolton Bailey]

I am writing a linter to catch nonterminal simps. I am noticing that most of these nonterminal simps are followed by rfl is that considered ok / should the linter ignore this?

[Bolton Bailey]

As I recall the rationale is that we don't want changes to the simp set to potentially break untouched files. Is it possible for a nonterminal simp like this which is immediately closed by rfl to do so?

[Scott Morrison]

Yes, it's certainly possible that changes to the simp set could make the rfl unnecessary.

[Scott Morrison]

However it may be best to be pragmatic for now and let this pattern past the linter.

[Patrick Massot]

This is really an edge case, I don't think we have a policy about it.

[Ruben Van de Velde]

I think most of those may have worked without the refl in lean 3. I'm not sure if anyone investigated what changed

[Ruben Van de Velde]

I'm not too worried about simp solving the goal making the rfl redundant, but I've seen simp change goals that were syntactically different but definitionally equal into goals that were no longer definitionally equal

[Ruben Van de Velde]

Though I agree that letting this slide in the initial version of the linter makes sense; we can always tighten later

[Joël Riou]

In mathlib3, we sometimes had to switch simp and simpa in one way or another in order to make some refactors work. It seems the new simpadoes not try rfl, so that we have to switch between simp and simp; rfl instead. I think the linter should not consider this is an issue.

[Eric Rodriguez]

I think the fact that simpa tried rfl was a bug in lean3 and I remember people being unhappy about it.

[Bolton Bailey]

Ok, the PR is #7497

[Damiano Testa]

I do not know if this is in scope, but looking at the output of

git ls-files 'Mathlib*.lean' | xargs awk '
  FNR == 1 { within=0 }
  within == 1 && !/^ *rfl$/ {
    within=0
    line=line "\n" $0
    gsub(/[^ ].*/, "")
    if ($0 == indent) { printf("%s\n", line)
  } indent="" }
  (/^  *simp[ \[]/ && !/simp .*only/) { line=FILENAME ":" FNR ":\n" $0; gsub(/[^ ].*/, "")
  within=1
  indent=$0 }'

there are a few more non-terminal simps. Here is a sample output:

Mathlib/SetTheory/Ordinal/Notation.lean:625:
      simp [h₂.zero_of_zero e0, xe, -Nat.cast_succ]
      rw [nat_cast_succ x, add_mul_succ _ ao, mul_assoc]
Mathlib/SetTheory/Ordinal/Notation.lean:629:
      simp [IH, Mul.mul, mul, e0, repr_add, opow_add, mul_add]
      rw [← mul_assoc]
Mathlib/SetTheory/Ordinal/Notation.lean:719:
      simp [split_eq_scale_split' h', split, split']
      have : 1 + (e - 1) = e := by
Mathlib/SetTheory/Ordinal/Notation.lean:744:
      simp [IH₂, split']
      intros
Mathlib/SetTheory/Ordinal/Notation.lean:764:
    simp [(· * ·)]; simp [mul, scale]
    haveI := h.snd
Mathlib/SetTheory/Ordinal/Notation.lean:788:
  simp [repr_scale, s₂.symm]
  infer_instance
Mathlib/SetTheory/Ordinal/Notation.lean:981:
        simp [HPow.hPow]
        simp [Pow.pow, opow, Ordinal.succ_ne_zero]

[Damiano Testa]

I really do not know python very much, but it seems that here

        if (not is_comment) and re.search(r"^\s*simp$", line):

you are matching simp followed by nothing else (this is implicitly confirmed by the shape of the squeezed simps in the PR). However, there are a few uses of simp [something] that are not terminal.

[Bolton Bailey]

Ok thanks for that comment @Damiano Testa , I have made a change to the PR to also match calls to simp that provide lemmas. This has resulted in even more things to fix, which I have put in #7580. I'd appreciate if some maintainer could look at it before it goes stale again.