simp_all / grind self-replacement

Stream: mathlib4

[Alex Meiburg]

I realize that simp_all is a fragile tactic that goes all over the place in how it affects goal state. :slight_smile: But this seems somewhat unfortunate. Here I have a short argument that can be closed by just simp_all [...]; grind [...]. Unfortunately, when I want to squeeze the simp_all, the suggested simp_all only given by simp_all? breaks the proof!

I'm mentioning simp_all and grind in the subject line, because it seems not great on the part of the simp_all, but also maybe a bit of a sore spot on grind, that it's sensitive to the exact simplification that happened, in this way. (I'm having a hard time piecing together exactly where the simplification changes, so maybe it's not grind's fault at all, though, depending on what happened.)

import Mathlib

lemma extracted_issue [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MetricSpace P] [NormedAddTorsor V P] {O a b c A B C P_AB P_AC P_BC : P}
  (h_a_eq : a = O)
  (h_AB : (affineSpan ℝ {A, B} : Set P) ∩ affineSpan ℝ {a, b} = {P_AB})
  (h_AC : (affineSpan ℝ {A, C} : Set P) ∩ affineSpan ℝ {a, c} = {P_AC})
  (h_BC : (affineSpan ℝ {B, C} : Set P) ∩ affineSpan ℝ {b, c} = {P_BC})
  (hb₂ : b = O) (hc' : c = O) :
    Collinear ℝ {P_AB, P_AC, P_BC} := by
  simp_all? [Set.eq_singleton_iff_unique_mem]
  /- replacing with the suggested
  simp_all only [coe_affineSpan, Set.mem_singleton_iff, Set.insert_eq_of_mem, AffineSubspace.coe_affineSpan_singleton,
    Set.eq_singleton_iff_unique_mem, Set.mem_inter_iff, and_imp]
  causes grind to fail. -/
  grind [collinear_singleton]

[Alex Meiburg]

Oh dear, I just saw #mathlib4 > simp only + grind failure too. Possible duplicate.

[Kim Morrison]

It's not great that simp_all? doesn't always give a viable replacement. It's easier to recover if the simp lemmas are locally confluent. In this case, this means adding:

@[simp] theorem spanPoints_singleton
    [AddCommGroup V] [Module ℝ V] [AddTorsor V P] {O : P} : spanPoints ℝ {O} = {O} := sorry

(or rather, some generalization replacing \real)

Then simp_all? [Set.eq_singleton_iff_unique_mem] gives

simp_all only [coe_affineSpan, Set.mem_singleton_iff, Set.insert_eq_of_mem,  AffineSubspace.coe_affineSpan_singleton,
    Set.eq_singleton_iff_unique_mem, Set.mem_inter_iff, and_imp]

as before, but then a subsequent simp_all? gives simp_all only [spanPoints_singleton, Set.mem_singleton_iff, Set.insert_eq_of_mem], at which point grind [collinear_singleton] goes through.

[Joseph Myers]

coe_affineSpan should not be a simp lemma. spanPoints and all lemmas stated using it should be deprecated (this would require some reworking to avoid using spanPoints to define affineSpan and prove lemmas about it).

[Malvin Gattinger]

For the record: I am often running into situations where the simp only [...] suggestion breaks the proof but when I add exists_prop to the list it works again. The same with simp_all? and its suggestion. So maybe there is something about exists_prop that prevents it from getting picked up by the ? suggestion machinery?
I don't have an MWE, but it keeps popping up while I am trying to satisfy the flexible linter in my project where it was not enabled before.

[Johan Commelin]

Hmm, I remember simp? being unreliable in the Lean 3 days, but I don't remember any issues in the past > 8 months. (Maybe even the past 2 years. But I don't trust my memory.)

I would be interested in seeing a non-MWE if you encounter this again at some point.

[Malvin Gattinger]

Here is one, I tried to find something towards the root of my import tree so you should not have to compile too much. It does not break the proof in this case, but it does show an example where exists_prop is not caught: https://github.com/m4lvin/lean4-pdl/commit/6f9009d2561a5d7528f84992efbffb948820719c

[Jireh Loreaux]

Johan, I have a recent example of a failed squeeze for simp. Search "simp only and grind failure"

[Malvin Gattinger]

Semi-related: I often wrote cases bla <;> simp at * or similar where some cases finish with this, some don't and need follow-up proofs. The linter complains about this, and rightly so :see_no_evil: But with cases bla <;> simp? at * I get multiple suggestions, one for each of the cases. And accepting one can then break other cases, so I end up semi-manually writing the union of the suggestions. It would be very cool if simp? would be aware of such multi-goal situations and only make one suggestion.

[Bhavik Mehta]

https://github.com/leanprover/lean4/issues/4615 I think this might be the same exists_prop issue