Why is it necessary to run `simp_all` twice?

Stream: lean4

[Asei Inoue]

import Std.Tactic.Do
import Batteries

open Std

variable {α : Type} (A : Array α)
variable [LT α] [DecidableLT α]

@[grind =]
def ICan'tBelieveItCanSort := Id.run do
  let N := A.size
  let mut A := A.toVector
  for hi : i in [:N] do
    for hj : j in [:N] do
      if A[i] < A[j] then
        A := A.swap i j
  return A.toArray

open Std.Do

set_option mvcgen.warning false

theorem ICan'tBelieveItCanSort_perm (arr : Array α) : Array.Perm (ICan'tBelieveItCanSort arr) arr := by
  generalize h : ICan'tBelieveItCanSort arr = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨_cursor, vec⟩ => ⌜Array.Perm arr vec.toArray⌝
  · ⇓⟨_cursor, vec⟩ => ⌜Array.Perm arr vec.toArray⌝
  with grind [Array.Perm.trans, Array.Perm.symm, Array.swap_perm]

@[simp, grind =]
theorem Vector.toArray_extract_size {α : Type} {n : Nat} (v : Vector α n) :
    v.toArray.extract 0 n = v.toArray := by
  grind

variable [LE α] [IsLinearOrder α] [LawfulOrderLT α]

@[grind! =>]
theorem cursor_pos_le_length (n : Nat) (xs : [0:n].toList.Cursor) : xs.pos ≤ n := by
  have : xs.prefix.length + xs.suffix.length = n := by
    simp [← List.length_append, xs.property]
  grind only

@[simp]
theorem lemm (n cur : Nat) (pref suff : List Nat) (h : [:n].toList = pref ++ cur :: suff) :
    pref.length = cur := by
  grind

theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by
  generalize h : ICan'tBelieveItCanSort A = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · ⇓⟨xs, A'⟩ => ⌜A'.take xs.pos |>.toArray.Pairwise (· ≤ ·)⌝
  · ⇓⟨xs, A'⟩ => by
    expose_names
    exact ⌜(A'.take cur |>.toArray.Pairwise (· ≤ ·)) ∧ ∀ i (_ : i < xs.pos), A'[i]'(by grind) ≤ A'[cur]'(by grind)⌝

  case vc1.step.isTrue =>
    expose_names
    simp_all [Array.pairwise_iff_getElem]
    grind
  case vc2 =>
    grind
  case vc3 =>
    expose_names
    simp_all
    simp_all -- why twice `simp_all` is needed here?

    -- why simp lemma `pref.length = cur` is not applied?
    guard_hyp h_2 : Array.Pairwise (fun x1 x2 => x1 ≤ x2) (b.toArray.extract 0 pref.length)

    grind
  case vc4.step.post.success =>
    simp_all [Array.pairwise_iff_getElem]
    grind
  case vc5 =>
    grind
  case vc6 =>
    grind

[Asei Inoue]

I have two question:

• in case vc3, why does the result change when I run simp_all twice? I thought simp_all was a tactic that simplifies “until nothing more can be simplified,” but is that not the case?
• in case vc3, why simp lemma pref.length = cur is not applied?

[Aaron Liu]

Could be an instance of lean4#8300

[Asei Inoue]

I figured out why lemm isn’t being used by simp. It seems that simp is failing to automatically supply the argument h.

[Kenny Lau]

well, it isn't supposed to