From 0eca3bd55de7f29320e90b83ef2f43e9dff7546b Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 25 Nov 2024 05:19:23 -0800
Subject: [PATCH] feat: add a coercion from `List Nat` to
 `Lean.Meta.Occurrences` (#6206)

This PR makes it possible to write `rw (occs := [1,2]) ...` instead of
`rw (occs := .pos [1,2]) ...` by adding a coercion from `List.Nat` to
`Lean.Meta.Occurrences`.
---
 src/Init/Data/Array/Bootstrap.lean | 2 +-
 src/Init/Data/List/Sublist.lean    | 2 +-
 src/Init/Data/Nat/Dvd.lean         | 2 +-
 src/Init/Data/Nat/Lemmas.lean      | 4 ++--
 src/Init/MetaTypes.lean            | 6 ++++++
 5 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index 2cefb7db4d..004f4e2c48 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -23,7 +23,7 @@ theorem foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux f arr i (j+1) H]
-    rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
+    rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
index de54ffab05..638a824d86 100644
--- a/src/Init/Data/List/Sublist.lean
+++ b/src/Init/Data/List/Sublist.lean
@@ -835,7 +835,7 @@ theorem isPrefix_iff : l₁ <+: l₂ ↔ ∀ i (h : i < l₁.length), l₂[i]? =
       simpa using ⟨0, by simp⟩
     | cons b l₂ =>
       simp only [cons_append, cons_prefix_cons, ih]
-      rw (occs := .pos [2]) [← Nat.and_forall_add_one]
+      rw (occs := [2]) [← Nat.and_forall_add_one]
       simp [Nat.succ_lt_succ_iff, eq_comm]
 
 theorem isPrefix_iff_getElem {l₁ l₂ : List α} :
diff --git a/src/Init/Data/Nat/Dvd.lean b/src/Init/Data/Nat/Dvd.lean
index bba1d884da..5dc8619028 100644
--- a/src/Init/Data/Nat/Dvd.lean
+++ b/src/Init/Data/Nat/Dvd.lean
@@ -92,7 +92,7 @@ protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
   rw [Nat.mul_comm, Nat.mul_div_cancel' H]
 
 @[simp] theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c := by
-  rw (occs := .pos [2]) [← mod_add_div a b]
+  rw (occs := [2]) [← mod_add_div a b]
   have ⟨x, h⟩ := h
   subst h
   rw [Nat.mul_assoc, add_mul_mod_self_left]
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index cb60267c5d..b956ca8712 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -651,8 +651,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
   | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos)
 
 theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by
-  rw (occs := .pos [1]) [← mod_add_div a n]
-  rw (occs := .pos [1]) [← mod_add_div b n]
+  rw (occs := [1]) [← mod_add_div a n]
+  rw (occs := [1]) [← mod_add_div b n]
   rw [Nat.add_mul, Nat.mul_add, Nat.mul_add,
     Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left,
     Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]
diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index aa7ade2488..1221a37e4a 100644
--- a/src/Init/MetaTypes.lean
+++ b/src/Init/MetaTypes.lean
@@ -251,10 +251,16 @@ def neutralConfig : Simp.Config := {
 
 end Simp
 
+/-- Configuration for which occurrences that match an expression should be rewritten. -/
 inductive Occurrences where
+  /-- All occurrences should be rewritten. -/
   | all
+  /-- A list of indices for which occurrences should be rewritten. -/
   | pos (idxs : List Nat)
+  /-- A list of indices for which occurrences should not be rewritten. -/
   | neg (idxs : List Nat)
   deriving Inhabited, BEq
 
+instance : Coe (List Nat) Occurrences := ⟨.pos⟩
+
 end Lean.Meta