feat: Array.contains_def

Std/Data/Array/Basic.lean

@@ -15,18 +15,10 @@ proofs about these definitions, those are contained in other files in `Std.Data.
 
 namespace Array
 
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) #[]
-
 /-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
 def reduceOption (l : Array (Option α)) : Array α :=
   l.filterMap id
 
-/-- Turns `#[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` into `#[a₁, a₂, ⋯, b₁, b₂, ⋯]` -/
-def flatten (arr : Array (Array α)) : Array α :=
-  arr.foldl (init := #[]) fun acc a => acc.append a
-
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
 def zipWithIndex (arr : Array α) : Array (α × Nat) :=
   arr.mapIdx fun i a => (a, i)

Std/Data/Array/Init/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Std.Tactic.NoMatch
-import Std.Data.List.Init.Lemmas
 
 /-!
 ## Bootstrapping definitions about arrays
@@ -28,3 +26,11 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
 termination_by _ => n - i
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) #[]
+
+/-- Turns `#[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` into `#[a₁, a₂, ⋯, b₁, b₂, ⋯]` -/
+def flatten (arr : Array (Array α)) : Array α :=
+  arr.foldl (init := #[]) fun acc a => acc.append a

Std/Data/Array/Init/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Std.Tactic.NoMatch
 import Std.Tactic.HaveI
 import Std.Classes.LawfulMonad
+import Std.Data.Nat.Init.Lemmas
 import Std.Data.List.Init.Lemmas
 import Std.Data.Array.Init.Basic
 
@@ -227,3 +228,82 @@ theorem foldl_data_eq_map (l : List α) (acc : Array β) (G : α → β) :
   induction l generalizing acc <;> simp [*]
 
 theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by simp
+
+theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
+    anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
+  simp only [anyM, Nat.min_def]; split <;> rfl
+
+theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start stop)
+    (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
+  rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt_of_le h)]
+
+theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) (start stop)
+    (hstart : start ≤ min stop as.size) (tru : Prop) (fal : Nat → Prop) (h0 : fal start)
+    (hp : ∀ i : Fin as.size, i.1 < stop → fal i.1 →
+      SatisfiesM (bif · then tru else fal (i + 1)) (p as[i])) :
+    SatisfiesM
+      (fun res => bif res then tru else fal (min stop as.size))
+      (anyM p as start stop) := by
+  let rec go {stop j} (hj' : j ≤ stop) (hstop : stop ≤ as.size) (h0 : fal j)
+    (hp : ∀ i : Fin as.size, i.1 < stop → fal i.1 →
+      SatisfiesM (bif · then tru else fal (i + 1)) (p as[i])) :
+    SatisfiesM
+      (fun res => bif res then tru else fal stop)
+      (anyM.loop p as stop hstop j) := by
+    unfold anyM.loop; split
+    · next hj =>
+      exact (hp ⟨j, Nat.lt_of_lt_of_le hj hstop⟩ hj h0).bind fun
+        | true, h => .pure h
+        | false, h => go hj hstop h hp
+    · next hj => exact .pure <| Nat.le_antisymm hj' (Nat.ge_of_not_lt hj) ▸ h0
+  simp only [Array.anyM_eq_anyM_loop]
+  exact go hstart _ h0 fun i hi => hp i <| Nat.lt_of_lt_of_le hi <| Nat.min_le_left ..
+termination_by go => stop - j
+
+theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
+    (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)
+    (hp : ∀ i : Fin as.size, start ≤ i.1 → i.1 < stop → SatisfiesM (· = true ↔ q i) (p as[i])) :
+    SatisfiesM
+      (fun res => res = true ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i)
+      (anyM p as start stop) := by
+  cases Nat.le_total start (min stop as.size) with
+  | inl hstart =>
+    refine (SatisfiesM_anyM _ _ _ _ hstart
+      (fal := fun j => start ≤ j ∧ ¬ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < j ∧ q i)
+      (tru := ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ q i) ?_ ?_).imp ?_
+    · exact ⟨Nat.le_refl _, fun ⟨i, h₁, h₂, _⟩ => (Nat.not_le_of_gt h₂ h₁).elim⟩
+    · refine fun i h₂ ⟨h₁, h₃⟩ => (hp _ h₁ h₂).imp fun hq => ?_
+      unfold cond; split <;> simp at hq
+      · exact ⟨_, h₁, h₂, hq⟩
+      · refine ⟨Nat.le_succ_of_le h₁, h₃.imp fun ⟨j, h₃, h₄, h₅⟩ => ⟨j, h₃, ?_, h₅⟩⟩
+        refine Nat.lt_of_le_of_ne (Nat.le_of_lt_succ h₄) fun e => hq (Fin.eq_of_val_eq e ▸ h₅)
+    · intro
+      | true, h => simp only [true_iff]; exact h
+      | false, h =>
+        simp only [false_iff]
+        exact h.2.imp fun ⟨j, h₁, h₂, hq⟩ => ⟨j, h₁, Nat.lt_min.2 ⟨h₂, j.2⟩, hq⟩
+  | inr hstart =>
+    rw [anyM_stop_le_start (h := hstart)]
+    refine .pure ?_; simp; intro j h₁ h₂
+    cases Nat.not_lt_of_le (Nat.le_trans hstart h₁) (Nat.lt_min.2 ⟨h₂, j.2⟩)
+
+theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) :
+    any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+  have := SatisfiesM_anyM_iff_exists (m := Id) p as start stop (p as[·]) (by simp)
+  rwa [SatisfiesM_Id_eq] at this
+
+theorem any_eq_true (p : α → Bool) (as : Array α) :
+    any as p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+
+theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
+  ⟨fun | .mk h => h, Array.Mem.mk⟩
+
+theorem any_def {p : α → Bool} (as : Array α) : as.any p = as.data.any p := by
+  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
+  exact ⟨fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩, fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩⟩
+
+theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
+  rw [mem_def, contains, any_def, List.any_eq_true]; simp [and_comm]
+
+instance [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
+  decidable_of_iff _ contains_def

Std/Data/Array/Merge.lean

@@ -110,7 +110,7 @@ where
   go (xs ys : Array α) :=
     let xsSize := xs.size
     ys.foldl (init := xs) fun xs y =>
-      if xs[:xsSize].contains y then xs else xs.push y
+      if xs.any (y == ·) (stop := xsSize) then xs else xs.push y
 
 /--
 Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with

Std/Data/List/Init/Lemmas.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
 import Std.Data.Fin.Init.Lemmas
+import Std.Classes.SetNotation
+import Std.Logic
 
 namespace List
 
@@ -50,6 +52,14 @@ theorem ne_nil_of_length_eq_succ (_ : length l = succ n) : l ≠ [] := fun _ =>
 theorem length_eq_zero : length l = 0 ↔ l = [] :=
   ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
 
+/-! ### mem -/
+
+@[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := fun.
+
+@[simp] theorem mem_cons : a ∈ (b :: l) ↔ a = b ∨ a ∈ l :=
+  ⟨fun h => by cases h <;> simp [Membership.mem, *],
+   fun | Or.inl rfl => by constructor | Or.inr h => by constructor; assumption⟩
+
 /-! ### append -/
 
 @[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl
@@ -133,6 +143,19 @@ theorem reverseAux_eq (as bs : List α) : reverseAux as bs = reverse as ++ bs :=
 theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.reverse.map f := by
   induction l <;> simp [*]
 
+/-! ### nth element -/
+
+theorem get_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ n, get l n = a
+  | _, _ :: _, .head .. => ⟨⟨0, Nat.succ_pos _⟩, rfl⟩
+  | _, _ :: _, .tail _ m => let ⟨⟨n, h⟩, e⟩ := get_of_mem m; ⟨⟨n+1, Nat.succ_lt_succ h⟩, e⟩
+
+theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
+  | _ :: _, 0, _ => .head ..
+  | _ :: l, _+1, _ => .tail _ (get_mem l ..)
+
+theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
+  ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
+
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -354,6 +377,12 @@ theorem lookup_cons [BEq α] {k : α} :
 @[simp] theorem unzip_cons {h : α × β} :
     (h :: t).unzip = match unzip t with | (al, bl) => (h.1::al, h.2::bl) := rfl
 
+/-! ### all / any -/
+
+@[simp] theorem all_eq_true {l : List α} : l.all p ↔ ∀ x ∈ l, p x := by induction l <;> simp [*]
+
+@[simp] theorem any_eq_true {l : List α} : l.any p ↔ ∃ x ∈ l, p x := by induction l <;> simp [*]
+
 /-! ### enumFrom -/
 
 @[simp] theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl

Std/Data/List/Lemmas.lean

@@ -56,14 +56,8 @@ theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
 
 /-! ### mem -/
 
-@[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := fun.
-
 theorem mem_nil_iff (a : α) : a ∈ ([] : List α) ↔ False := by simp
 
-@[simp] theorem mem_cons : a ∈ (b :: l) ↔ a = b ∨ a ∈ l :=
-  ⟨fun h => by cases h <;> simp [Membership.mem, *],
-   fun | Or.inl rfl => by constructor | Or.inr h => by constructor; assumption⟩
-
 theorem mem_cons_self (a : α) (l : List α) : a ∈ a :: l := .head ..
 
 theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
@@ -601,10 +595,6 @@ theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
 
 @[simp] theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl
 
-theorem get_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ n, get l n = a
-  | _, _ :: _, .head .. => ⟨⟨0, Nat.succ_pos _⟩, rfl⟩
-  | _, _ :: _, .tail _ m => let ⟨⟨n, h⟩, e⟩ := get_of_mem m; ⟨⟨n+1, Nat.succ_lt_succ h⟩, e⟩
-
 theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
   | _ :: _, 0, _ => rfl
   | _ :: l, _+1, _ => get?_eq_get (l := l) _
@@ -636,16 +626,9 @@ theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
-theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
-  | _ :: _, 0, _ => .head ..
-  | _ :: l, _+1, _ => .tail _ (get_mem l ..)
-
 theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
   let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem ..
 
-theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
-  ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
-
 -- TODO(Mario): move somewhere else
 theorem Fin.exists_iff (p : Fin n → Prop) : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=
   ⟨fun ⟨i, h⟩ => ⟨i.1, i.2, h⟩, fun ⟨i, hi, h⟩ => ⟨⟨i, hi⟩, h⟩⟩
@@ -1010,10 +993,6 @@ theorem length_removeNth : ∀ {l i}, i < length l → length (@removeNth α l i
 
 /-! ### all / any -/
 
-@[simp] theorem all_eq_true {l : List α} : l.all p ↔ ∀ x ∈ l, p x := by induction l <;> simp [*]
-
-@[simp] theorem any_eq_true {l : List α} : l.any p ↔ ∃ x ∈ l, p x := by induction l <;> simp [*]
-
 @[simp] theorem contains_nil [BEq α] : ([] : List α).contains a = false := rfl
 
 @[simp] theorem contains_cons [BEq α] :

Std/Data/Nat/Init/Lemmas.lean

@@ -37,6 +37,11 @@ protected theorem min_le_right (a b : Nat) : min a b ≤ b := by rw [Nat.min_def
 
 protected theorem min_le_left (a b : Nat) : min a b ≤ a := Nat.min_comm .. ▸ Nat.min_le_right ..
 
+protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
+
+protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b := by
+  rw [Nat.min_comm]; exact Nat.min_eq_left h
+
 protected theorem max_comm (a b : Nat) : max a b = max b a := by
   simp only [Nat.max_def]
   by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
@@ -48,3 +53,18 @@ protected theorem le_max_left (a b : Nat) : a ≤ max a b := by rw [Nat.max_def]
 protected theorem le_max_right (a b : Nat) : b ≤ max a b := Nat.max_comm .. ▸ Nat.le_max_left ..
 
 protected theorem pow_two_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+
+protected theorem not_lt_of_le {n m : Nat} (h₁ : m ≤ n) : ¬ n < m := (Nat.not_le_of_gt · h₁)
+
+protected theorem le_of_not_le {a b : Nat} : ¬ a ≤ b → b ≤ a := (Nat.le_total a b).resolve_left
+
+protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
+  intros; cases Nat.le_total b c with
+  | inl h => rw [Nat.min_eq_left h]; assumption
+  | inr h => rw [Nat.min_eq_right h]; assumption
+
+protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
+  ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
+   fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩
+
+protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min

Std/Data/Nat/Lemmas.lean

@@ -136,8 +136,6 @@ theorem recDiagOn_succ_succ {motive : Nat → Nat → Sort _} (zero_zero : motiv
 
 theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm
 
-protected theorem le_of_not_le {a b : Nat} : ¬ a ≤ b → b ≤ a := (Nat.le_total a b).resolve_left
-
 protected theorem lt_iff_le_not_le {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m :=
   ⟨fun h => ⟨Nat.le_of_lt h, Nat.not_le_of_gt h⟩, fun h => Nat.gt_of_not_le h.2⟩
 
@@ -181,8 +179,6 @@ protected theorem lt_trichotomy (a b : Nat) : a < b ∨ a = b ∨ b < a :=
 protected theorem eq_or_lt_of_not_lt {a b : Nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
   (Nat.lt_trichotomy a b).resolve_left hnlt
 
-protected theorem not_lt_of_le {n m : Nat} (h₁ : m ≤ n) : ¬ n < m := (Nat.not_le_of_gt · h₁)
-
 protected theorem not_le_of_lt {n m : Nat} : m < n → ¬ n ≤ m := Nat.not_le_of_gt
 
 protected theorem lt_of_not_le {a b : Nat} : ¬ a ≤ b → b < a := (Nat.lt_or_ge b a).resolve_right
@@ -454,22 +450,6 @@ protected theorem sub_add_lt_sub {n m k : Nat} (h₁ : m + k ≤ n) (h₂ : 0 <
 
 /-! ## min/max -/
 
-protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
-
-protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b := by
-  rw [Nat.min_comm]; exact Nat.min_eq_left h
-
-protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
-  intros; cases Nat.le_total b c with
-  | inl h => rw [Nat.min_eq_left h]; assumption
-  | inr h => rw [Nat.min_eq_right h]; assumption
-
-protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
-  ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
-   fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩
-
-protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min
-
 theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by
   cases Nat.le_total x y with
   | inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]

Std/Tactic/Lint/Misc.lean

@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Robert Y. Lewis, Arthur Paulino, Gabriel Ebner
 import Lean.Util.CollectLevelParams
 import Lean.Meta.ForEachExpr
 import Std.Tactic.Lint.Basic
-import Std.Data.Array.Basic
+import Std.Data.Array.Init.Basic
 
 open Lean Meta