feat: More grind annotations for List.range' (#9766)

This PR moves `List.range'_elim` to `List.eq_of_range'_eq_append_cons` and adds a couple of `grind` annotations for `List.range'`. This will make it more convenient to work with proof obligations produced by `mvcgen`.
2025-08-13 11:27:48 +02:00 · 2025-08-13 11:27:48 +02:00 · 55f9dfad7d
commit 55f9dfad7d
parent b9a8dd8f0d
6 changed files with 141 additions and 151 deletions
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@ -2108,6 +2108,11 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
  | _, 0, _ => []
  | s, n+1, step => s :: range' (s+step) n step

+@[simp, grind =] theorem range'_zero : range' s 0 step = [] := rfl
+@[simp, grind =] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
+-- The following theorem is intentionally not a simp lemma.
+theorem range'_succ : range' s (n + 1) step = s :: range' (s + step) n step := rfl
+
 /-! ### zipIdx -/

 /--
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@ -70,7 +70,7 @@ See also

 Further results, which first require developing further automation around `Nat`, appear in
 * `Init.Data.List.Nat.Basic`: miscellaneous lemmas
-* `Init.Data.List.Nat.Range`: `List.range` and `List.enum`
+* `Init.Data.List.Nat.Range`: `List.range`, `List.range'` and `List.enum`
 * `Init.Data.List.Nat.TakeDrop`: `List.take` and `List.drop`

 Also
@ -1851,6 +1851,10 @@ theorem append_eq_map_iff {f : α → β} :
 theorem sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
  induction l₁ generalizing l₂ <;> simp_all [Nat.add_assoc]

+@[simp, grind =]
+theorem sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum := by
+  induction xs <;> simp_all [Nat.add_comm]
+
 /-! ### concat

 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@ -90,28 +90,27 @@ theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
  rintro rfl
  omega

-theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k) := by
+theorem range'_eq_append_iff : range' s n step = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k step ∧ ys = range' (s + k * step) (n - k) step := by
  induction n generalizing s xs ys with
  | zero => simp
  | succ n ih =>
    simp only [range'_succ]
    rw [cons_eq_append_iff]
+    have add_mul' (k n m : Nat) : (n + m) * k = m * k + n * k := by rw [Nat.add_mul]; omega
    constructor
    · rintro (⟨rfl, rfl⟩ | ⟨_, rfl, h⟩)
      · exact ⟨0, by simp [range'_succ]⟩
      · simp only [ih] at h
        obtain ⟨k, h, rfl, rfl⟩ := h
        refine ⟨k + 1, ?_⟩
-        simp_all [range'_succ]
-        omega
+        simp_all [range'_succ, Nat.add_assoc]
    · rintro ⟨k, h, rfl, rfl⟩
      cases k with
      | zero => simp [range'_succ]
      | succ k =>
-        simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]
+        simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, exists_eq_left', false_or]
        refine ⟨k, ?_⟩
-        simp_all
-        omega
+        simp_all [Nat.add_assoc]

@[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
    (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
@ -178,6 +177,46 @@ theorem count_range_1' {a s n} :
    specialize h (a - s)
    omega

+@[simp, grind =]
+theorem sum_range' : (range' start n step).sum = n * start + n * (n - 1) * step / 2 := by
+  induction n generalizing start with
+  | zero => simp
+  | succ n ih =>
+    simp_all only [List.range'_succ, List.sum_cons, Nat.mul_add, ← Nat.add_assoc,
+      Nat.add_mul, Nat.one_mul, Nat.add_one_sub_one]
+    have : n * step + n * (n - 1) * step / 2 = (n * n * step + n * step) / 2 := by
+      apply Nat.eq_div_of_mul_eq_left (by omega)
+      rw [Nat.add_mul, Nat.div_mul_cancel]
+      · calc  n * step * 2 + n * (n - 1) * step
+          _ = n * step * 2 + n * step * (n - 1) := by simp [Nat.mul_comm, Nat.mul_assoc]
+          _ = n * step + n * step * n := by cases n <;> simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
+          _ = n * n * step + n * step := by simp [Nat.mul_comm, Nat.add_comm, Nat.mul_left_comm]
+      · have : 2 ∣ n ∨ 2 ∣ (n - 1) := by omega
+        apply Nat.dvd_mul_right_of_dvd
+        apply Nat.dvd_mul.mpr
+        cases this with
+        | inl h => exists 2, 1; omega
+        | inr h => exists 1, 2; omega
+    omega
+
+@[simp, grind =]
+theorem drop_range' : (List.range' start n step).drop k = List.range' (start + k * step) (n - k) step := by
+  induction k generalizing start n with
+  | zero => simp
+  | succ => cases n <;> simp [*, List.range'_succ, Nat.add_mul, ← Nat.add_assoc, Nat.add_right_comm]
+
+@[simp, grind =]
+theorem take_range'_of_length_le (h : n ≤ k) : (List.range' start n step).take k = List.range' start n step := by
+  induction n generalizing start k with
+  | zero => simp
+  | succ n ih => cases k <;> simp_all [List.range'_succ]
+
+@[simp, grind =]
+theorem take_range'_of_length_ge (h : n ≥ k) : (List.range' start n step).take k = List.range' start k step := by
+  induction k generalizing start n with
+  | zero => simp
+  | succ k ih => cases n <;> simp_all [List.range'_succ]
+
 /-! ### range -/

 theorem reverse_range' : ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1 - ·) (range n)
@ -355,9 +394,7 @@ theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
    simp only [length_range'] at h
    obtain rfl := h
    refine ⟨ws, xs, rfl, ?_⟩
-    simp only [zipIdx_eq_zip_range', length_append, true_and]
-    congr
-    omega
+    simp [zipIdx_eq_zip_range', length_append]
  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
    simp only [zipIdx_eq_zip_range']
    refine ⟨l₁', l₂', range' k l₁'.length, range' (k + l₁'.length) l₂'.length, ?_⟩
--- a/src/Init/Data/List/Range.lean
+++ b/src/Init/Data/List/Range.lean
@ -29,30 +29,31 @@ open Nat

 /-! ### range' -/

-theorem range'_succ {s n step} : range' s (n + 1) step = s :: range' (s + step) n step := by
-  simp [range']
-
-@[simp] theorem length_range' {s step} : ∀ {n : Nat}, length (range' s n step) = n
+@[simp, grind =] theorem length_range' {s step} : ∀ {n : Nat}, length (range' s n step) = n
  | 0 => rfl
  | _ + 1 => congrArg succ length_range'

-@[simp] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
+@[simp, grind =] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
  rw [← length_eq_zero_iff, length_range']

 theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0 := by
  cases n <;> simp

-@[simp] theorem range'_zero : range' s 0 step = [] := by
-  simp
+theorem range'_eq_cons_iff : range' s n step = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + step) (n - 1) step := by
+  induction n generalizing s with
+  | zero => simp
+  | succ n ih =>
+    simp only [range'_succ]
+    simp only [cons.injEq, and_congr_right_iff]
+    rintro rfl
+    simp [eq_comm]

-@[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
-
-@[simp] theorem tail_range' : (range' s n step).tail = range' (s + step) (n - 1) step := by
+@[simp, grind =] theorem tail_range' : (range' s n step).tail = range' (s + step) (n - 1) step := by
  cases n with
  | zero => simp
  | succ n => simp [range'_succ]

-@[simp] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
+@[simp, grind =] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
  constructor
  · intro h
    have h' := congrArg List.length h
@ -81,14 +82,14 @@ theorem getElem?_range' {s step} :
    exact (getElem?_range' (s := s + step) (by exact succ_lt_succ_iff.mp h)).trans <| by
      simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]

-@[simp] theorem getElem_range' {n m step} {i} (H : i < (range' n m step).length) :
+@[simp, grind =] theorem getElem_range' {n m step} {i} (H : i < (range' n m step).length) :
    (range' n m step)[i] = n + step * i :=
  (getElem?_eq_some_iff.1 <| getElem?_range' (by simpa using H)).2

 theorem head?_range' : (range' s n).head? = if n = 0 then none else some s := by
  induction n <;> simp_all [range'_succ]

-@[simp] theorem head_range' (h) : (range' s n).head h = s := by
+@[simp, grind =] theorem head_range' (h) : (range' s n).head h = s := by
  repeat simp_all [head?_range', head_eq_iff_head?_eq_some]

 theorem map_add_range' {a} : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
@ -107,7 +108,7 @@ theorem range'_append : ∀ {s m n step : Nat},
    simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
      using range'_append (s := s + step)

-@[simp] theorem range'_append_1 {s m n : Nat} :
+@[simp, grind =] theorem range'_append_1 {s m n : Nat} :
    range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)

 theorem range'_sublist_right {s m n : Nat} : range' s m step <+ range' s n step ↔ m ≤ n :=
@ -129,15 +130,6 @@ theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ [
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ [s + n] := by
  simp [range'_concat]

-theorem range'_eq_cons_iff : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1) := by
-  induction n generalizing s with
-  | zero => simp
-  | succ n ih =>
-    simp only [range'_succ]
-    simp only [cons.injEq, and_congr_right_iff]
-    rintro rfl
-    simp [eq_comm]
-
 /-! ### range -/

@[simp, grind =] theorem range_one : range 1 = [0] := rfl
@ -152,7 +144,7 @@ theorem range_eq_range' {n : Nat} : range n = range' 0 n :=
 theorem getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i := by
  simp [range_eq_range', getElem?_range' h]

-@[simp] theorem getElem_range (h : j < (range n).length) : (range n)[j] = j := by
+@[simp, grind =] theorem getElem_range (h : j < (range n).length) : (range n)[j] = j := by
  simp [range_eq_range']

 theorem range_succ_eq_map {n : Nat} : range (n + 1) = 0 :: map succ (range n) := by
@ -162,23 +154,23 @@ theorem range_succ_eq_map {n : Nat} : range (n + 1) = 0 :: map succ (range n) :=
 theorem range'_eq_map_range {s n : Nat} : range' s n = map (s + ·) (range n) := by
  rw [range_eq_range', map_add_range']; rfl

-@[simp] theorem length_range {n : Nat} : (range n).length = n := by
+@[simp, grind =] theorem length_range {n : Nat} : (range n).length = n := by
  simp only [range_eq_range', length_range']

-@[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
+@[simp, grind =] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
  rw [← length_eq_zero_iff, length_range]

 theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by
  cases n <;> simp

-@[simp] theorem tail_range : (range n).tail = range' 1 (n - 1) := by
+@[simp, grind =] theorem tail_range : (range n).tail = range' 1 (n - 1) := by
  rw [range_eq_range', tail_range']

-@[simp]
+@[simp, grind =]
 theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
  simp only [range_eq_range', range'_sublist_right]

-@[simp]
+@[simp, grind =]
 theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
  simp only [range_eq_range', range'_subset_right, lt_succ_self]

@ -196,7 +188,7 @@ theorem head?_range {n : Nat} : (range n).head? = if n = 0 then none else some 0
    simp only [range_succ, head?_append, ih]
    split <;> simp_all

-@[simp] theorem head_range {n : Nat} (h) : (range n).head h = 0 := by
+@[simp, grind =] theorem head_range {n : Nat} (h) : (range n).head h = 0 := by
  cases n with
  | zero => simp at h
  | succ n => simp [head?_range, head_eq_iff_head?_eq_some]
@ -208,7 +200,7 @@ theorem getLast?_range {n : Nat} : (range n).getLast? = if n = 0 then none else
    simp only [range_succ, getLast?_append, ih]
    split <;> simp_all

-@[simp] theorem getLast_range {n : Nat} (h) : (range n).getLast h = n - 1 := by
+@[simp, grind =] theorem getLast_range {n : Nat} (h) : (range n).getLast h = n - 1 := by
  cases n with
  | zero => simp at h
  | succ n => simp [getLast?_range, getLast_eq_iff_getLast?_eq_some]
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@ -29,6 +29,48 @@ theorem toList_range' (r : Std.Range) (h : r.step = 1) :

 end Std.Range

+namespace List
+
+@[grind →]
+theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
+    cur = s + step * xs.length := by
+  rw [range'_eq_append_iff] at h
+  obtain ⟨k, hk, hxs, hcur⟩ := h
+  have h := (range'_eq_cons_iff.mp hcur.symm).1.symm
+  have hk : k = xs.length := by simp_all [length_range']
+  simp only [h, hk, Nat.add_left_cancel_iff]
+  apply Nat.mul_comm
+
+@[grind →]
+theorem length_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
+    n = xs.length + ys.length + 1 := by
+  have : n = (range' s n step).length := by simp
+  simpa [h] using this
+
+@[grind →]
+theorem mem_of_range'_eq_append_cons (h : range' s n step = xs ++ i :: ys) :
+    i ∈ range' s n step := by simp [h]
+
+@[grind →]
+theorem gt_of_range'_eq_append_cons (h : range' s n step = xs ++ i :: ys) (hstep : 0 < step) (hj : j ∈ xs) :
+    j < i := by
+  obtain ⟨nxs, _, rfl, htail⟩ := range'_eq_append_iff.mp h
+  obtain ⟨rfl, _⟩ := range'_eq_cons_iff.mp htail.symm
+  simp only [mem_range'] at hj
+  obtain ⟨i, _, rfl⟩ := hj
+  apply Nat.add_lt_add_left
+  simp [Nat.mul_comm, *]
+
+@[grind →]
+theorem lt_of_range'_eq_append_cons (h : range' s n step = xs ++ i :: ys) (hstep : 0 < step) (hj : j ∈ ys) :
+    i < j := by
+  obtain ⟨k, hk, rfl, htail⟩ := range'_eq_append_iff.mp h
+  obtain ⟨rfl, _, _, _⟩ := range'_eq_cons_iff.mp htail.symm
+  simp only [mem_range'] at hj
+  omega
+
+end List
+
 namespace Std.List

@[ext]
@ -45,17 +87,6 @@ abbrev Zipper.end (l : List α) : Zipper l := ⟨l.reverse,[],by simp⟩
 abbrev Zipper.tail (s : Zipper l) (h : s.suff = hd::tl) : Zipper l :=
  { rpref := hd::s.rpref, suff := tl, property := by simp [s.property, ←h] }

-@[grind →]
-theorem range_elim : List.range' s n = xs ++ i :: ys → i = s + xs.length := by
-  intro h
-  induction xs generalizing s n
-  case nil => cases n <;> simp_all[List.range']
-  case cons head tail ih =>
-    cases n <;> simp[List.range'] at h
-    have := ih h.2
-    simp[ih h.2]
-    omega
-
 end Std.List

 namespace Std.Do
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@ -180,9 +180,7 @@ theorem beaking_loop_spec :
  mspec
  case inv => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
  all_goals simp_all
-  case post =>
-    conv in (List.sum _) => whnf
-    grind
+  case post => grind
  case step =>
    intros
    mintro _
@ -205,12 +203,10 @@ theorem returning_loop_spec :
    · mspec
      mspec
      intro _ h
-      conv at h in (List.sum _) => whnf
      simp at h
      grind
    · mspec
      intro _ h
-      conv at h in (List.sum _) => whnf
      simp at h ⊢
      grind
  case step =>
@ -472,7 +468,7 @@ theorem sum_loop_spec :
  mintro -
  mvcgen [sum_loop]
  case inv1 => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
-  all_goals simp_all +decide; try grind
+  all_goals simp_all; try grind

 theorem throwing_loop_spec :
  ⦃fun s => ⌜s = 4⌝⦄
@ -482,11 +478,7 @@ theorem throwing_loop_spec :
  mvcgen [throwing_loop]
  case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suff.sum > 4⌝,
                         fun e s => ⌜e = 42 ∧ s = 4⌝⟩
-  case vc1 => intro _; simp_all
-  case vc2 => intro _; simp_all only [SPred.down_pure]; grind
-  case vc3 => simp_all only [SPred.down_pure]; decide
-  case vc4 => simp_all only [SPred.down_pure]; grind
-  case vc5 => simp_all
+  all_goals mleave; try (subst_vars; grind)

 theorem test_loop_break :
  ⦃fun s => ⌜s = 42⌝⦄
@ -494,15 +486,7 @@ theorem test_loop_break :
  ⦃⇓ r s => ⌜r > 4 ∧ s = 1⌝⦄ := by
  mvcgen [breaking_loop]
  case inv1 => exact (⇓ (xs, r) s => ⌜(r ≤ 4 ∧ r = xs.rpref.sum ∨ r > 4) ∧ s = 42⌝)
-  case vc1 => intro _; mleave; grind
-  case vc2 => intro _; simp_all only [SPred.down_pure]; grind
-  case vc3 => simp_all
-  case vc4 =>
-    simp_all
-    rename_i h
-    conv at h in (List.sum _) => whnf
-    simp at h
-    grind
+  all_goals mleave; try grind

 theorem test_loop_early_return :
  ⦃fun s => ⌜s = 4⌝⦄
@ -510,16 +494,7 @@ theorem test_loop_early_return :
  ⦃⇓ r s => ⌜r = 42 ∧ s = 4⌝⦄ := by
  mvcgen [returning_loop]
  case inv1 => exact (⇓ (xs, r) s => ⌜(r.1 = none ∧ r.2 = xs.rpref.sum ∧ r.2 ≤ 4 ∨ r.1 = some 42 ∧ r.2 > 4) ∧ s = 4⌝)
-  case vc1 => intro _; mleave; grind
-  case vc2 => intro _; mleave; grind
-  case vc3 => simp_all
-  case vc4 =>
-    simp_all
-    rename_i h
-    conv at h in (List.sum _) => whnf
-    simp at h
-    grind
-  case vc5 => simp_all
+  all_goals simp_all; try grind

 theorem unfold_to_expose_match_spec :
  ⦃fun s => ⌜s = 4⌝⦄
@ -547,9 +522,7 @@ theorem test_sum :
  ⦃⇓r => ⌜r < 30⌝⦄ := by
  mvcgen
  case inv1 => exact (⇓ (xs, r) => ⌜(∀ x, x ∈ xs.suff → x ≤ 5) ∧ r + xs.suff.length * 5 ≤ 25⌝)
-  case vc1 => simp_all; omega
-  case vc3 => simp_all; omega
-  simp_all +decide
+  all_goals simp_all; try grind

 /--
  The main point about this test is that `mSpec` should return all unassigned MVars it creates.
@ -574,39 +547,16 @@ def check_all (p : Nat → Prop) [DecidablePred p] (n : Nat) : Bool := Id.run do
      return false
  return true

-@[simp]
-theorem Std.Range.mem_toList {x} {r : Std.Range} :
-    x ∈ r.toList ↔ x ∈ r := sorry
-
-@[simp]
-theorem Nat.mod_one {n : Nat} : n % 1 = 0 := by omega
-
-/--
-VC generation is normally not useful to massage hypotheses such as `ht`, but in this example
-we manage to prove a contradiction `hf` using the VC generator.
-/
 example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
    (∀ i, i < n → p i) ↔ check_all p n := by
-  constructor
-  · intro h
-    apply Id.by_wp (P := (· = true)) rfl
-    mvcgen
-    case inv1 => exact (⇓ (xs, r) => ⌜r.1 = none ∧ ∀ x, x ∈ xs.suff → p x⌝)
-    case vc3 => simp; intro a ha; apply h a ha.upper
-    all_goals simp_all
-  · intro ht i hin
-    apply Classical.byContradiction
-    intro h'
-    have hf : check_all p n = false := by
-      have hin : i ∈ [0:n] := by simp [Std.instMembershipNatRange, hin]
-      apply Id.by_wp (P := (· = false)) rfl
-      mvcgen
-      case inv1 => exact (⇓ (xs, r) =>
-        match r.1 with
-        | none => ⌜i ∈ xs.suff⌝
-        | some b => ⌜b = false ∧ xs.suff = []⌝)
-      all_goals simp_all [SPred.pure_nil]; try grind
-    simp [ht] at hf
+  generalize h : check_all p n = x
+  apply Id.by_wp h
+  mvcgen
+  case inv1 =>
+    exact Invariant.withEarlyReturn
+      (onReturn := fun ret _ => ⌜ret = false ∧ ¬ ∀ i < n, p i⌝)
+      (onContinue := fun xs _ => ⌜∀ i, i ∈ xs.pref → p i⌝)
+  all_goals simp_all [-Classical.not_forall]; try grind

 end Automated

@ -962,42 +912,13 @@ theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.pref) ∧ traversalState.pref.Nodup⌝)
  all_goals mleave; grind

-@[simp, grind]
-theorem Std.HashSet.Nodup_toList [Hashable α] [BEq α] [LawfulHashable α] [EquivBEq α] [LawfulBEq α] (m : Std.HashSet α) :
-    m.toList.Nodup := by
-  simp only [Std.HashSet.toList]
-  simpa using Std.HashMap.distinct_keys (m := m.inner)
-
-@[simp, grind]
-theorem Std.HashSet.Nodup_append_toList_insert [Hashable α] [BEq α] [LawfulHashable α] [EquivBEq α] [LawfulBEq α] (m : Std.HashSet α) (x : α) (h : x ∉ m) :
-    ((m.insert x).toList ++ tl).Nodup ↔ (m.toList ++ x :: tl).Nodup := by
-  grind
-
 theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
-  simp [nodup]
-  suffices h :
-      ∀ seen,
-        match MProd.fst (Id.run (forIn (β := MProd (Option Bool) (Std.HashSet Int)) l ⟨none, seen⟩ (fun x ⟨_, seen⟩ =>
-          if x ∈ seen then pure (ForInStep.done (α := MProd (Option Bool) (Std.HashSet Int)) ⟨some false, seen⟩)
-          else pure (ForInStep.yield (α := MProd (Option Bool) (Std.HashSet Int)) ⟨none, seen.insert x⟩)))) with
-        | some true => False
-        | some false => ¬(seen.toList ++ l).Nodup
-        | none => (seen.toList ++ l).Nodup by
-    replace h := h ∅
-    split
-    · simp_all only [Id.run_pure]; grind
-    · cases ‹Bool› <;> simp_all only [Id.run_pure]; grind
-  induction l with
-  | nil => simp_all
-  | cons hd tl ih =>
-    intro seen
-    simp_all
-    if hif : hd ∈ seen
-    then simp_all only [↓reduceIte, Id.run_pure]; grind
-    else
-      replace ih := ih (seen.insert hd)
-      simp only [hif, ↓reduceIte, Id.run_pure]
-      split <;> simp_all
+  rw [nodup]
+  generalize hseen : (∅ : Std.HashSet Int) = seen
+  change ?lhs ↔ l.Nodup
+  suffices h : ?lhs ↔ l.Nodup ∧ ∀ x ∈ l, x ∉ seen by grind
+  clear hseen
+  induction l generalizing seen with grind [Id.run_pure, Id.run_bind]

 end Nodup