Merge remote-tracking branch 'origin/master' into indexVariables3

src/Init/Data/Array/DecidableEq.lean

@@ -12,9 +12,9 @@ import Init.ByCases
 namespace Array
 
 private theorem rel_of_isEqvAux
-    {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
-    (heqv : Array.isEqvAux a b hsz r i hi)
-    {j : Nat} (hj : j < i) : r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
+    {r : α → α → Bool} {xs ys : Array α} (hsz : xs.size = ys.size) {i : Nat} (hi : i ≤ xs.size)
+    (heqv : Array.isEqvAux xs ys hsz r i hi)
+    {j : Nat} (hj : j < i) : r (xs[j]'(Nat.lt_of_lt_of_le hj hi)) (ys[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi))) := by
   induction i with
   | zero => contradiction
   | succ i ih =>
@@ -27,8 +27,8 @@ private theorem rel_of_isEqvAux
       subst hj'
       exact heqv.left
 
-private theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
-    (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
+private theorem isEqvAux_of_rel {r : α → α → Bool} {xs ys : Array α} (hsz : xs.size = ys.size) {i : Nat} (hi : i ≤ xs.size)
+    (w : ∀ j, (hj : j < i) → r (xs[j]'(Nat.lt_of_lt_of_le hj hi)) (ys[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux xs ys hsz r i hi := by
   induction i with
   | zero => simp [Array.isEqvAux]
   | succ i ih =>
@@ -36,23 +36,23 @@ private theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz :
     exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
 
 -- This is private as the forward direction of `isEqv_iff_rel` may be used.
-private theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
-    Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
+private theorem rel_of_isEqv {r : α → α → Bool} {xs ys : Array α} :
+    Array.isEqv xs ys r → ∃ h : xs.size = ys.size, ∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h')) := by
   simp only [isEqv]
   split <;> rename_i h
   · exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩
   · intro; contradiction
 
-theorem isEqv_iff_rel {a b : Array α} {r} :
-    Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
+theorem isEqv_iff_rel {xs ys : Array α} {r} :
+    Array.isEqv xs ys r ↔ ∃ h : xs.size = ys.size, ∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h')) :=
   ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
     simp only [isEqv, ← h, ↓reduceDIte]
     exact isEqvAux_of_rel h (by simp [h]) w⟩
 
-theorem isEqv_eq_decide (a b : Array α) (r) :
-    Array.isEqv a b r =
-      if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))) else false := by
-  by_cases h : Array.isEqv a b r
+theorem isEqv_eq_decide (xs ys : Array α) (r) :
+    Array.isEqv xs ys r =
+      if h : xs.size = ys.size then decide (∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h'))) else false := by
+  by_cases h : Array.isEqv xs ys r
   · simp only [h, Bool.true_eq]
     simp only [isEqv_iff_rel] at h
     obtain ⟨h, w⟩ := h
@@ -63,24 +63,24 @@ theorem isEqv_eq_decide (a b : Array α) (r) :
       Bool.not_eq_true]
     simpa [isEqv_iff_rel] using h'
 
-@[simp] theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r) := by
+@[simp] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
   simp [isEqv_eq_decide, List.isEqv_eq_decide]
 
-theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
+theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
   have ⟨h, h'⟩ := rel_of_isEqv h
   exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
 
-private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (a : Array α) (i : Nat) (h : i ≤ a.size) :
-    Array.isEqvAux a a rfl r i h = true := by
+private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (xs : Array α) (i : Nat) (h : i ≤ xs.size) :
+    Array.isEqvAux xs xs rfl r i h = true := by
   induction i with
   | zero => simp [Array.isEqvAux]
   | succ i ih =>
     simp_all only [isEqvAux, Bool.and_self]
 
-theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Array α) : Array.isEqv a a (· == ·) = true := by
+theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by
   simp [isEqv, isEqvAux_self]
 
-theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (· = ·) = true := by
+theorem isEqv_self [DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true := by
   simp [isEqv, isEqvAux_self]
 
 instance [DecidableEq α] : DecidableEq (Array α) :=
@@ -89,22 +89,22 @@ instance [DecidableEq α] : DecidableEq (Array α) :=
     | true  => isTrue (eq_of_isEqv a b h)
     | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
 
-theorem beq_eq_decide [BEq α] (a b : Array α) :
-    (a == b) = if h : a.size = b.size then
-      decide (∀ (i : Nat) (h' : i < a.size), a[i] == b[i]'(h ▸ h')) else false := by
+theorem beq_eq_decide [BEq α] (xs ys : Array α) :
+    (xs == ys) = if h : xs.size = ys.size then
+      decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by
   simp [BEq.beq, isEqv_eq_decide]
 
-@[simp] theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b) := by
+@[simp] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
   simp [beq_eq_decide, List.beq_eq_decide]
 
 end Array
 
 namespace List
 
-@[simp] theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
+@[simp] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
   simp [isEqv_eq_decide, Array.isEqv_eq_decide]
 
-@[simp] theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b) := by
+@[simp] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
   simp [beq_eq_decide, Array.beq_eq_decide]
 
 end List
@@ -114,7 +114,7 @@ namespace Array
 instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
   rfl := by simp [BEq.beq, isEqv_self_beq]
   eq_of_beq := by
-    rintro ⟨a⟩ ⟨b⟩ h
+    rintro ⟨_⟩ ⟨_⟩ h
     simpa using h
 
 end Array

src/Lean/Linter/List.lean

@@ -26,32 +26,67 @@ register_builtin_option linter.indexVariables : Bool := {
   descr := "Validate that variables appearing as an index (e.g. in `xs[i]` or `xs.take i`) are only `i`, `j`, or `k`."
 }
 
+/--
+`set_option linter.listName true` enables a strict linter that
+validates that all `List` variables are named `l`, `xs`, `ys`, `zs`, `as`, or `bs` (optionally with a `'`, `₁`, or `₂` suffix).
+-/
+register_builtin_option linter.listName : Bool := {
+  defValue := false
+  descr := "Validate that all `List`/`Array`/`Vector` variables use allowed names."
+}
+
 open Lean Elab Command
 
 /--
 Return the syntax for all expressions in which an `fvarId` appears as a "numerical index", along with the user name of that `fvarId`.
 -/
-partial def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
-  t.deepestNodes fun _ info _ => do
+def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
+  (t.deepestNodes fun _ info _ => do
     let stx := info.stx
     if let .ofTermInfo info := info then
-      let idx? := match_expr info.expr with
-      | GetElem.getElem _ _ _ _ _ _ i _ => some i
-      | GetElem?.getElem? _ _ _ _ _ _ i => some i
-      | List.take _ i _ => some i
-      | List.drop _ i _ => some i
-      | List.set _ _ i _ => some i
-      | List.insertIdx _ i _ _ => some i
-      | List.eraseIdx _ _ i _ => some i
-      | _ => none
-      match idx? with
-      | some (.fvar i) =>
-        match info.lctx.find? i with
-        | some ldecl => some (stx, ldecl.userName)
-        | none => none
-      | _ => none
+      let idxs := match_expr info.expr with
+      | GetElem.getElem _ _ _ _ _ _ i _ => [i]
+      | GetElem?.getElem? _ _ _ _ _ _ i => [i]
+      | List.take _ i _ => [i]
+      | List.drop _ i _ => [i]
+      | List.set _ _ i _ => [i]
+      | List.insertIdx _ i _ _ => [i]
+      | List.eraseIdx _ _ i _ => [i]
+      | _ => []
+      match idxs with
+      | [] => none
+      | _ => idxs.filterMap fun i =>
+        match i with
+        | .fvar i =>
+          match info.lctx.find? i with
+          | some ldecl => some (stx, ldecl.userName)
+          | none => none
+        | _ => none
     else
-      none
+      none).flatten
+
+/-- Find all binders appearing in the given info tree. -/
+def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Syntax × Name × Expr)) :=
+  t.collectTermInfoM fun ctx ti => do
+    if ti.isBinder then do
+      -- Something is wrong here: sometimes `inferType` fails with an unknown fvar error,
+      -- despite passing the local context here.
+      -- We fail quietly by returning a `Unit` type.
+      let ty ← ctx.runMetaM ti.lctx do (Meta.inferType ti.expr) <|> pure (.const `Unit [])
+      if p ty then
+        if let .fvar i := ti.expr then
+          match ti.lctx.find? i with
+          | some ldecl => return some (ti.stx, ldecl.userName, ty)
+          | none => return none
+        else
+          return none
+      else
+        return none
+    else
+      return none
+
+/-- Allowed names for index variables. -/
+def allowedIndices : List String := ["i", "j", "k"]
 
 /--
 A linter which validates that the only variables used as "indices" (e.g. in `xs[i]` or `xs.take i`)
@@ -66,10 +101,56 @@ def indexLinter : Linter
     for t in ← getInfoTrees do
       if let .context _ _ := t then -- Only consider info trees with top-level context
       for (idxStx, n) in numericalIndices t do
-        if n != `i && n != `j && n != `k then
-          Linter.logLint linter.indexVariables idxStx
-            m!"Forbidden variable appearing as an index: use `i`, `j`, or `k`: {n}"
+        if let .str _ n := n then
+          if !allowedIndices.contains n then
+            Linter.logLint linter.indexVariables idxStx
+              m!"Forbidden variable appearing as an index: use `i`, `j`, or `k`: {n}"
 
 builtin_initialize addLinter indexLinter
 
+/-- Strip optional suffixes from a binder name. -/
+def stripBinderName (s : String) : String :=
+  s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂"
+
+/-- Allowed names for `List` variables. -/
+def allowedListNames : List String := ["l", "xs", "ys", "zs", "as", "bs"]
+
+/-- Allowed names for `Array` variables. -/
+def allowedArrayNames : List String := ["xs", "ys", "zs", "as", "bs"]
+
+/-- Allowed names for `Vector` variables. -/
+def allowedVectorNames : List String := ["xs", "ys", "zs", "as", "bs"]
+
+/--
+A linter which validates that all `List`/`Array`/`Vector` variables use allowed names.
+-/
+def listNameLinter : Linter
+  where run := withSetOptionIn fun stx => do
+    unless (← getOptions).get linter.listName.name false do return
+    if (← get).messages.hasErrors then return
+    if ! (← getInfoState).enabled then return
+    for t in ← getInfoTrees do
+      if let .context _ _ := t then -- Only consider info trees with top-level context
+        let binders ← binders t
+        for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `List do
+          if let .str _ n := n then
+          let n := stripBinderName n
+          if !allowedListNames.contains n then
+            Linter.logLint linter.listName stx
+              m!"Forbidden variable appearing as a `List` name: use `l` instead of {n}"
+        for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
+          if let .str _ n := n then
+          let n := stripBinderName n
+          if !allowedArrayNames.contains n then
+            Linter.logLint linter.listName stx
+              m!"Forbidden variable appearing as a `Array` name: use `l` instead of {n}"
+        for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
+          if let .str _ n := n then
+          let n := stripBinderName n
+          if !allowedVectorNames.contains n then
+            Linter.logLint linter.listName stx
+              m!"Forbidden variable appearing as a `Vector` name: use `l` instead of {n}"
+
+builtin_initialize addLinter listNameLinter
+
 end Lean.Linter.List

src/Lean/Server/InfoUtils.lean

@@ -69,23 +69,35 @@ def InfoTree.visitM' [Monad m]
     (ctx? : Option ContextInfo := none) (t : InfoTree) : m Unit :=
   t.visitM preNode (fun ci i cs _ => postNode ci i cs) ctx? |> discard
 
+/--
+  Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
+def InfoTree.collectNodesBottomUpM [Monad m] (p : ContextInfo → Info → PersistentArray InfoTree → List α → m (List α)) (i : InfoTree) : m (List α) :=
+  (·.getD []) <$> i.visitM (m := m) (postNode := fun ci i cs as => do p ci i cs (as.filterMap id).flatten)
+
 /--
   Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/
 def InfoTree.collectNodesBottomUp (p : ContextInfo → Info → PersistentArray InfoTree → List α → List α) (i : InfoTree) : List α :=
-  i.visitM (m := Id) (postNode := fun ci i cs as => p ci i cs (as.filterMap id).flatten) |>.getD []
+  i.collectNodesBottomUpM (m := Id) p
+
+/--
+  For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns
+  `some _`  and return the union of all such nodes. The visitor `p` is given a node together with
+  its innermost surrounding `ContextInfo`. -/
+partial def InfoTree.deepestNodesM [Monad m] (p : ContextInfo → Info → PersistentArray InfoTree → m (Option α)) (infoTree : InfoTree) : m (List α) :=
+  infoTree.collectNodesBottomUpM fun ctx i cs rs => do
+    if rs.isEmpty then
+      match ← p ctx i cs with
+      | some r => return [r]
+      | none   => return []
+    else
+      return rs
 
 /--
   For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns
   `some _`  and return the union of all such nodes. The visitor `p` is given a node together with
   its innermost surrounding `ContextInfo`. -/
 partial def InfoTree.deepestNodes (p : ContextInfo → Info → PersistentArray InfoTree → Option α) (infoTree : InfoTree) : List α :=
-  infoTree.collectNodesBottomUp fun ctx i cs rs =>
-    if rs.isEmpty then
-      match p ctx i cs with
-      | some r => [r]
-      | none   => []
-    else
-      rs
+  infoTree.deepestNodesM (m := Id) p
 
 partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α :=
   go none init
@@ -98,6 +110,17 @@ where go ctx? a
     ts.foldl (init := a) (go <| i.updateContext? ctx?)
   | hole _ => a
 
+partial def InfoTree.foldInfoM [Monad m] (f : ContextInfo → Info → α → m α) (init : α) : InfoTree → m α :=
+  go none init
+where go ctx? a
+  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
+  | node i ts => do
+    let a ← match ctx? with
+      | none => pure a
+      | some ctx => f ctx i a
+    ts.foldlM (init := a) (go <| i.updateContext? ctx?)
+  | hole _ => pure a
+
 /--
 Fold an info tree as follows, while ensuring that the correct `ContextInfo` is supplied at each stage:
 
@@ -119,6 +142,15 @@ where
     ts.foldl (init := a) (go <| i.updateContext? ctx?)
   | hole _ => a
 
+def InfoTree.collectTermInfoM [Monad m] (t : InfoTree) (f : ContextInfo → TermInfo → m (Option α)) : m (List α) :=
+  t.foldInfoM (init := []) fun ctx info result =>
+    match info with
+    | Info.ofTermInfo ti => do
+      match ← f ctx ti with
+      | some a => return a :: result
+      | none => return result
+    | _ => return result
+
 def Info.isTerm : Info → Bool
   | ofTermInfo _ => true
   | _ => false

tests/lean/run/list_name_linter.lean

@@ -0,0 +1,46 @@
+set_option linter.listName true
+
+#guard_msgs in
+example (l : List Nat) : l = l := rfl
+
+#guard_msgs in
+example (l' : List Nat) : l' = l' := rfl
+
+#guard_msgs in
+example (l₁ : List Nat) : l₁ = l₁ := rfl
+
+#guard_msgs in
+example (l₂ : List Nat) : l₂ = l₂ := rfl
+
+/--
+warning: Forbidden variable appearing as a `List` name: use `l` instead of l₃
+note: this linter can be disabled with `set_option linter.listName false`
+---
+warning: Forbidden variable appearing as a `List` name: use `l` instead of l₃
+note: this linter can be disabled with `set_option linter.listName false`
+-/
+#guard_msgs in
+example (l₃ : List Nat) : l₃ = l₃ := rfl
+
+#guard_msgs in
+example (xs : List Nat) : xs = xs := rfl
+
+/--
+warning: Forbidden variable appearing as a `List` name: use `l` instead of ps
+note: this linter can be disabled with `set_option linter.listName false`
+---
+warning: Forbidden variable appearing as a `List` name: use `l` instead of ps
+note: this linter can be disabled with `set_option linter.listName false`
+-/
+#guard_msgs in
+example (ps : List Nat) : ps = ps := rfl
+
+/--
+warning: Forbidden variable appearing as a `Array` name: use `l` instead of l
+note: this linter can be disabled with `set_option linter.listName false`
+---
+warning: Forbidden variable appearing as a `Array` name: use `l` instead of l
+note: this linter can be disabled with `set_option linter.listName false`
+-/
+#guard_msgs in
+example (l : Array Nat) : l = l := rfl