feat: introduce List.Cursor.pos as an abbreviation for prefix.length (leanprover#10642)

This PR introduces `List.Cursor.pos` as an abbreviation for
`prefix.length`.

Author: sgraf812

src/Std/Do/Triple/SpecLemmas.lean

@@ -59,6 +59,20 @@ def Cursor.tail (s : Cursor l) (h : 0 < s.suffix.length := by get_elem_tactic) :
     (Cursor.at l n).tail (by simpa using Nat.sub_lt_sub_right (Nat.le_refl n) h) = Cursor.at l (n + 1) := by
   simp [Cursor.tail, Cursor.at, Cursor.current]
 
+/--
+The position of the cursor in the list.
+It's a shortcut for the number of elements in the prefix.
+-/
+abbrev Cursor.pos (c : Cursor l) : Nat := c.prefix.length
+
+@[simp, grind =]
+theorem Cursor.pos_at {l : List α} {n : Nat} (h : n < l.length) :
+    (Cursor.at l n).pos = n := by simp only [pos, «at», length_take]; omega
+
+@[simp]
+theorem Cursor.pos_mk {l pre suff : List α} (h : pre ++ suff = l) :
+    (Cursor.mk pre suff h).pos = pre.length := rfl
+
 @[grind →]
 theorem eq_of_range'_eq_append_cons (h : range' s n step = xs ++ cur :: ys) :
     cur = s + step * xs.length := by

tests/lean/run/bhaviksSampler.lean

@@ -152,7 +152,7 @@ theorem sampler_correct {m : Type → Type u} {k h} [Monad m] [WPMonad m ps] :
   sampler (m:=m) n k h
   ⦃⇓ xs => ⌜xs.toList.Nodup⌝⦄ := by
   mvcgen -leave [sampler]
-  case inv1 => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.prefix.length⌝)
+  case inv1 => exact (⇓ (xs, midway) => ⌜Midway.valid midway xs.pos⌝)
   case vc1 pref cur _ _ _ _ _ _ r _ _ _ =>
     dsimp
     mframe

tests/lean/run/doLogicTests.lean

@@ -235,7 +235,7 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
   if h : n = 0 then simp [h] else
   simp only [h, reduceIte]
   mspec -- Spec.pure
-  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝) ?step
+  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.pos ∧ b = fib_spec (xs.pos + 1)⌝) ?step
   case step => intros; mintro _; simp_all
   simp_all [Nat.sub_one_add_one]
 
@@ -246,7 +246,7 @@ theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_sp
   mintro -
   simp only [fib_impl, h, reduceIte]
   mspec
-  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝) ?step
+  mspec Spec.forIn_range (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.pos ∧ b = fib_spec (xs.pos + 1)⌝) ?step
   case step => intros; mintro _; mspec; mspec; simp_all
   simp_all [Nat.sub_one_add_one]
 
@@ -279,7 +279,7 @@ theorem fib_impl_vcs
 
 theorem fib_triple_vcs : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
   apply fib_impl_vcs
-  case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝)
+  case I => intro n hn; exact (⇓ ⟨xs, a, b⟩ => ⌜a = fib_spec xs.pos ∧ b = fib_spec (xs.pos + 1)⌝)
   case ret => mpure_intro; rfl
   case loop_pre => intros; mpure_intro; trivial
   case loop_post => simp_all [Nat.sub_one_add_one]
@@ -365,14 +365,14 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
   unfold fib_impl
   mvcgen
   case inv1 => exact ⇓ (xs, ⟨a, b⟩) =>
-    ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝
+    ⌜a = fib_spec xs.pos ∧ b = fib_spec (xs.pos + 1)⌝
   all_goals simp_all +zetaDelta [Nat.sub_one_add_one]
 
 theorem fib_triple_step : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
   unfold fib_impl
   mvcgen (stepLimit := some 14) -- 13 still has a wp⟦·⟧
   case inv1 => exact ⇓ ⟨xs, a, b⟩ =>
-    ⌜a = fib_spec xs.prefix.length ∧ b = fib_spec (xs.prefix.length + 1)⌝
+    ⌜a = fib_spec xs.pos ∧ b = fib_spec (xs.pos + 1)⌝
   all_goals simp_all +zetaDelta [Nat.sub_one_add_one]
 
 attribute [local spec] fib_triple in
@@ -674,7 +674,7 @@ def max_and_sum (xs : Array Nat) : Id (Nat × Nat) := do
 theorem max_and_sum_spec (xs : Array Nat) :
     ⦃⌜∀ i, (h : i < xs.size) → xs[i] ≥ 0⌝⦄ max_and_sum xs ⦃⇓ (m, s) => ⌜s ≤ m * xs.size⌝⦄ := by
   mvcgen [max_and_sum]
-  case inv1 => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.prefix.length⌝)
+  case inv1 => exact (⇓ ⟨xs, m, s⟩ => ⌜s ≤ m * xs.pos⌝)
   all_goals simp_all
   · rw [Nat.left_distrib]
     simp +zetaDelta only [Nat.mul_one, Nat.add_le_add_iff_right]
@@ -821,14 +821,14 @@ theorem naive_expo_correct (x n : Nat) : naive_expo x n = x^n := by
   generalize h : naive_expo x n = r
   apply Id.of_wp_run_eq h
   mvcgen
-  case inv1 => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.prefix.length⌝
+  case inv1 => exact ⇓⟨xs, r⟩ => ⌜r = x^xs.pos⌝
   all_goals simp_all [Nat.pow_add_one]
 
 theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
   generalize h : fast_expo x n = r
   apply Id.of_wp_run_eq h
   mvcgen
-  case inv1 => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.prefix.length⌝
+  case inv1 => exact ⇓⟨xs, e, x', y⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.pos⌝
   all_goals simp_all
   case vc1 b _ _ _ _ _ _ ih =>
     obtain ⟨e, y, x'⟩ := b