advice on fixing "simp at ..." is a flexible tactic modifyin

Stream: general

[TongKe Xue]

At https://github.com/tkxue/func_algo/blob/main/FuncAlgo/C01_Sort.lean I have a port of https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.html

It's a Lean4 translation of (1) defining insertion sort, (2) two defs of what "sorted" means, and (3) proving InsertSort satisfies both defs of "sorted", (4) both defs of sorted are equal.

I am mostly okay with the proof, except for this warning:

cat build.log | grep simp | grep "is a flexible" | wc -l
19

cat build.log | grep simp | grep "is a flexible"
warning: FuncAlgo/C01_Sort.lean:100:20: 'simp at h_iv h_jv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:100:20: 'simp at h_iv h_jv' is a flexible tactic modifying 'h_jv'…
warning: FuncAlgo/C01_Sort.lean:121:9: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:122:11: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:133:16: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:133:50: 'simp at h3' is a flexible tactic modifying 'h3'…
warning: FuncAlgo/C01_Sort.lean:134:18: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:138:13: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:138:46: 'simp at h3' is a flexible tactic modifying 'h3'…
warning: FuncAlgo/C01_Sort.lean:139:46: 'simp at h3' is a flexible tactic modifying 'h3'…
warning: FuncAlgo/C01_Sort.lean:139:13: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:140:15: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:140:52: 'simp at h3' is a flexible tactic modifying 'h3'…
warning: FuncAlgo/C01_Sort.lean:165:14: 'simp at h_iv h_jv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:165:14: 'simp at h_iv h_jv' is a flexible tactic modifying 'h_jv'…
warning: FuncAlgo/C01_Sort.lean:167:6: 'simp at h_iv h_jv' is a flexible tactic modifying 'h_jv'…
warning: FuncAlgo/C01_Sort.lean:167:6: 'simp at h_iv h_jv' is a flexible tactic modifying 'h_iv'…
warning: FuncAlgo/C01_Sort.lean:214:9: 'simp at hi' is a flexible tactic modifying 'hi'…
warning: FuncAlgo/C01_Sort.lean:261:12: 'simp at h_iv' is a flexible tactic modifying 'h_iv'…

There's three questions here:

1. Why am I using simp in the first place ?
2. Why is this bad ?
3. How do we fix this ?

Why am I using simp in the first place ?

The reason I'm using simp is that in "walking through the code/spec symbolically of InsertSort", we often get things like:

lst[idx]? = some t

then we do do some cases, and this becomes

(x0 :: x1 :; xs) [ 0, 1, i+2] ? = some t

and we need simp to get one of x0 = t, x1 = t, or xs[i] = t

Why is this bad ?

I have no idea. My suspicion is that maybe simp has its code changed over time, and this might cause simp to do different things, or simplify in different ways, which then causes the proof to break? [Not sure].

How do we fix this ?

I have no clue. I'm asking for advice here. It is not obvious to me at all how to fix all the sim at h#'s.

Thanks!

[Kim Morrison]

@Damiano Testa, @Johan Commelin, could we make fixing this a high priority (possibly removing it from the standard linter set right now?) It's really unkind to users to give them non-actionable warnings like this.

[Kim Morrison]

@TongKe Xue, in the meantime, try replacing each such simp with simp?, and then using the "Try this:" suggestion that appears in the InfoView.

[Johan Commelin]

Kim Morrison said:

Damiano Testa, Johan Commelin, could we make fixing this a high priority (possibly removing it from the standard linter set right now?) It's really unkind to users to give them non-actionable warnings like this.

Yes, let's revert enabling the linter until we have better warnings.

[Michael Rothgang]

Do we want to revert the linter in mathlib or enabling the linter in other projects? I do think we want it in mathlib, for instance.

[Johan Commelin]

Disabled the linter in #32420

[TongKe Xue]

@Kim Morrison

1. Thank you for the simp -> simp? -> info view "apply fix" advice. Very cool feature. It explicitly lists out the rules simp uses for simplifying.

2. I have a followup issue. Captured screencast: https://www.youtube.com/watch?v=MIbHfvDxorM

   

3. In text: I'm running into a followup issue regarding readability (perhaps this is due to poor structuring of the proof). The issue is as follows -- I'm not sure getting rid of the linter error makes the proof more readable

before:

      -- | 0 => simp at h_iv; have h3 := h 1 iv; simp at h3; apply h3 h_iv
      -- | 1 => simp at h_iv; have h3 := h 0 iv; simp at h3; apply h3 h_iv
      -- | i+2 => simp at h_iv; have h3 := h (i+2) iv; simp at h3; apply h3 h_iv

after:

     match i with
      | 0 =>
          simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.ofNat_pos, or_true,
            getElem?_pos, List.getElem_cons_zero, Option.some.injEq] at h_iv; have h3 := h 1 iv;
          simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true,
            getElem?_pos, List.getElem_cons_succ, List.getElem_cons_zero, Option.some.injEq] at h3; apply h3 h_iv
      | 1 =>
          simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff, zero_lt_one, or_true,
            getElem?_pos, List.getElem_cons_succ, List.getElem_cons_zero, Option.some.injEq] at h_iv; have h3 := h 0 iv;
          simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.ofNat_pos, or_true,
            getElem?_pos, List.getElem_cons_zero, Option.some.injEq] at h3; apply h3 h_iv
      | i+2 =>
          simp only [List.getElem?_cons_succ] at h_iv; have h3 := h (i+2) iv;
          simp only [List.getElem?_cons_succ] at h3; apply h3 h_iv
```

So my "updated" problem is:

(a) = "simp at ..." = linter warning
(b) = "simp only [...] at ..." = imho the proof is less readable

I suspect I'm doing something else wrong (perhaps in the overall structure of the proof?)

Advice, however crazy, appreciated.

(Aside: Is this a good time to invest in https://leanprover-community.github.io/lean4-metaprogramming-book/ and try to roll my own mini tactics for handling these "verifying functional algorithm" program proofs? [feels a bit early for this; but not sure])

Thanks!

[Kim Morrison]

One trick you need to learn is the simpa tactic.

[TongKe Xue]

I was able to change

      -- | 0 => simp at h_iv; have h3 := h 1 iv; simp at h3; apply h3 h_iv
      -- | 1 => simp at h_iv; have h3 := h 0 iv; simp at h3; apply h3 h_iv
      -- | i+2 => simp at h_iv; have h3 := h (i+2) iv; simp at h3; apply h3 h_iv

to

      match i with
      | 0 => apply (h 1 iv); simpa using h_iv;
      | 1 => apply (h 0 iv); simpa using h_iv;
      | i+2 => apply h (i+2) iv; simpa using h_iv;

My understanding here is:

• simpa is simp + assumption; but requires we close goal; and does not trigger linter warning
• it's not clear if we can reduce this to 1 line; the goal state at the start is:

1 goal
l1 l2 : List ℕ
f : ℕ → Prop
x y : ℕ
lst : List ℕ
h : List_fa (y :: x :: lst) f
i iv : ℕ
h_iv : (x :: y :: lst)[0]? = some iv
⊢ f iv

[TongKe Xue]

https://github.com/tkxue/func_algo/commit/bf516c3c952bf49185d55c3e7ad686bd45132514

Using simpa (and rearranging some stuff) solved all the "simp ... flexible tactic" linter errors.

This was instructive. Thanks!

[TongKe Xue]

My $0.02, after having gone through the issue.

1. I think having the linter warning is great. It forced me to re-org the proof, which improved quality.
2. I would recommend appending to the linter warning msg something like:

Two common ways to fix this are:

1. change 'simp ..' to 'simp only [...] ...' by (1) changing simp to simp? and (2) using the 'apply fix' button in infoview
2. restructure the section using have, apply, suffices, so we can conclude the goal with a single simpa

[Chris Henson]

Johan Commelin said:

Disabled the linter in #32420

I appreciate you keeping it available for downstream projects, we find it very useful already in CSLib!

[Michael Rothgang]

My hope is that after #32421 lands, the linter can be re-enabled.

[Michael Rothgang]

#32577 re-enables the linter; the error messages now suggest one way to fix this.
(It is not always clear which fix is the best; this will require judgement on a case-by-case basis. If all possible fixes are truly worse than the other options, disabling the linter with a comment is also fine.)

[Kim Morrison]

The flexible linter comes at a +2.3% overall instruction penalty.

[Johan Commelin]

@Thomas Murrills mentioned the following idea, which hopefully can be implemented at some point. Linters like these would not run by default when working on Mathlib, but at some point you flip a switch and go into "PR preparation mode". Then several of these linters kick in, and help you improve your branch to get it PR-ready.

The linters would also still run in CI, of course. So the performance cost is still there for CI. But not during the authoring phase, where most people spend their time.