/-
Copyright (c) 2021 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
-/
import Std.Data.Array.Init.Basic
import Std.Data.Ord

/-!
## Definitions on Arrays

This file contains various definitions on `Array`. It does not contain
proofs about these definitions, those are contained in other files in `Std.Data.Array`.
-/

namespace Array

/-- The array `#[0, 1, ..., n - 1]`. -/
def range: Nat → Array Nat
range (n: Nat
n : Nat: Type
Nat) : Array: Type ?u.4 → Type ?u.4
Array Nat: Type
Nat :=
  n: Nat
n.fold: {α : Type ?u.7} → (Nat → α → α) → Nat → α → α
fold (flip: {α : Sort ?u.15} → {β : Sort ?u.14} → {φ : Sort ?u.13} → (α → β → φ) → β → α → φ
flip Array.push: {α : Type ?u.23} → Array α → α → Array α
Array.push) #[]: Array ?m.39
#[]

/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/
def reduceOption: {α : Type ?u.96} → Array (Option α) → Array α
reduceOption (l: Array (Option α)
l : Array: Type ?u.95 → Type ?u.95
Array (Option: Type ?u.96 → Type ?u.96
Option α: ?m.92
α)) : Array: Type ?u.99 → Type ?u.99
Array α: ?m.92
α :=
  l: Array (Option α)
l.filterMap: {α : Type ?u.104} →
  {β : Type ?u.103} → (α → Option β) → (as : Array α) → optParam Nat 0 → optParam Nat (size as) → Array β
filterMap id: {α : Sort ?u.114} → α → α
id

/-- Turns `#[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` into `#[a₁, a₂, ⋯, b₁, b₂, ⋯]` -/
def flatten: {α : Type ?u.667} → Array (Array α) → Array α
flatten (arr: Array (Array α)
arr : Array: Type ?u.666 → Type ?u.666
Array (Array: Type ?u.667 → Type ?u.667
Array α: ?m.663
α)) : Array: Type ?u.670 → Type ?u.670
Array α: ?m.663
α :=
  arr: Array (Array α)
arr.foldl: {α : Type ?u.675} → {β : Type ?u.674} → (β → α → β) → β → (as : Array α) → optParam Nat 0 → optParam Nat (size as) → β
foldl (init := #[]: Array ?m.707
#[]) fun acc: ?m.691
acc a: ?m.694
a => acc: ?m.691
acc.append: {α : Type ?u.696} → Array α → Array α → Array α
append a: ?m.694
a

/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
def zipWithIndex: {α : Type ?u.922} → Array α → Array (α × Nat)
zipWithIndex (arr: Array α
arr : Array: Type ?u.922 → Type ?u.922
Array α: ?m.919
α) : Array: Type ?u.925 → Type ?u.925
Array (α: ?m.919
α × Nat: Type
Nat) :=
  arr: Array α
arr.mapIdx: {α : Type ?u.932} → {β : Type ?u.931} → (as : Array α) → (Fin (size as) → α → β) → Array β
mapIdx fun i: ?m.941
i a: ?m.944
a => (a: ?m.944
a, i: ?m.941
i)

/--
Check whether `xs` and `ys` are equal as sets, i.e. they contain the same
elements when disregarding order and duplicates. `O(n*m)`! If your element type
has an `Ord` instance, it is asymptotically more efficient to sort the two
arrays, remove duplicates and then compare them elementwise.
-/
def equalSet: {α : Type u_1} → [inst : BEq α] → Array α → Array α → Bool
equalSet [BEq: Type ?u.1333 → Type ?u.1333
BEq α: ?m.1330
α] (xs: Array α
xs ys: Array α
ys : Array: Type ?u.1336 → Type ?u.1336
Array α: ?m.1330
α) : Bool: Type
Bool :=
  xs: Array α
xs.all: {α : Type ?u.1347} → (as : Array α) → (α → Bool) → optParam Nat 0 → optParam Nat (size as) → Bool
all (ys: Array α
ys.contains: {α : Type ?u.1358} → [inst : BEq α] → Array α → α → Bool
contains ·) && ys: Array α
ys.all: {α : Type ?u.1370} → (as : Array α) → (α → Bool) → optParam Nat 0 → optParam Nat (size as) → Bool
all (xs: Array α
xs.contains: {α : Type ?u.1380} → [inst : BEq α] → Array α → α → Bool
contains ·)

set_option linter.unusedVariables.funArgs false in
/--
Sort an array using `compare` to compare elements.
-/
def qsortOrd: {α : Type ?u.1565} → [ord : Ord α] → Array α → Array α
qsortOrd [ord: Ord α
ord : Ord: Type ?u.1565 → Type ?u.1565
Ord α: ?m.1562
α] (xs: Array α
xs : Array: Type ?u.1568 → Type ?u.1568
Array α: ?m.1562
α) : Array: Type ?u.1571 → Type ?u.1571
Array α: ?m.1562
α :=
  xs: Array α
xs.qsort: {α : Type ?u.1576} → (as : Array α) → (α → α → Bool) → optParam Nat 0 → optParam Nat (size as - 1) → Array α
qsort λ x: ?m.1585
x y: ?m.1588
y => compare: {α : Type ?u.1590} → [self : Ord α] → α → α → Ordering
compare x: ?m.1585
x y: ?m.1588
y |>.isLT: Ordering → Bool
isLT

set_option linter.unusedVariables.funArgs false in
/--
Find the first minimal element of an array. If the array is empty, `d` is
returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
considered.
-/
@[inline]
protected def minD: {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam Nat 0 → optParam Nat (size xs) → α
minD [ord: Ord α
ord : Ord: Type ?u.1686 → Type ?u.1686
Ord α: ?m.1683
α]
    (xs: Array α
xs : Array: Type ?u.1689 → Type ?u.1689
Array α: ?m.1683
α) (d: α
d : α: ?m.1683
α) (start: optParam Nat 0
start := 0: ?m.1697
0) (stop: optParam ?m.1708 (size xs)
stop := xs: Array α
xs.size: {α : Type ?u.1709} → Array α → Nat
size) : α: ?m.1683
α :=
  xs: Array α
xs.foldl: {α : Type ?u.1733} → {β : Type ?u.1732} → (β → α → β) → β → (as : Array α) → optParam Nat 0 → optParam Nat (size as) → β
foldl (init := d: α
d) (start := start: optParam Nat 0
start) (stop := stop: optParam Nat (size xs)
stop) λ min: ?m.1749
min x: ?m.1752
x =>
    if compare: {α : Type ?u.1754} → [self : Ord α] → α → α → Ordering
compare x: ?m.1752
x min: ?m.1749
min |>.isLT: Ordering → Bool
isLT then x: ?m.1752
x else min: ?m.1749
min

set_option linter.unusedVariables.funArgs false in
/--
Find the first minimal element of an array. If the array is empty, `none` is
returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
considered.
-/
@[inline]
protected def min?: {α : Type ?u.1988} → [ord : Ord α] → (xs : Array α) → optParam Nat 0 → optParam Nat (size xs) → Option α
min? [ord: Ord α
ord : Ord: Type ?u.1988 → Type ?u.1988
Ord α: ?m.1985
α]
    (xs: Array α
xs : Array: Type ?u.1991 → Type ?u.1991
Array α: ?m.1985
α) (start: optParam Nat 0
start := 0: ?m.1997
0) (stop: optParam ?m.2008 (size xs)
stop := xs: Array α
xs.size: {α : Type ?u.2009} → Array α → Nat
size) : Option: Type ?u.2016 → Type ?u.2016
Option α: ?m.1985
α :=
  if h: ?m.2086
h : start: optParam Nat 0
start < xs: Array α
xs.size: {α : Type ?u.2033} → Array α → Nat
size then
    some: {α : Type ?u.2059} → α → Option α
some $ xs: Array α
xs.minD: {α : Type ?u.2062} → [ord : Ord α] → (xs : Array α) → α → optParam Nat 0 → optParam Nat (size xs) → α
minD (xs: Array α
xs.get: {α : Type ?u.2073} → (a : Array α) → Fin (size a) → α
get ⟨start: optParam Nat 0
start, h: ?m.2057
h⟩) start: optParam Nat 0
start stop: optParam Nat (size xs)
stop
  else
    none: {α : Type ?u.2088} → Option α
none

set_option linter.unusedVariables.funArgs false in
/--
Find the first minimal element of an array. If the array is empty, `default` is
returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
considered.
-/
@[inline]
protected def minI: {α : Type u_1} → [ord : Ord α] → [inst : Inhabited α] → (xs : Array α) → optParam Nat 0 → optParam Nat (size xs) → α
minI [ord: Ord α
ord : Ord: Type ?u.2187 → Type ?u.2187
Ord α: ?m.2184
α] [Inhabited: Sort ?u.2190 → Sort (max1?u.2190)
Inhabited α: ?m.2184
α]
    (xs: Array α
xs : Array: Type ?u.2193 → Type ?u.2193
Array α: ?m.2184
α) (start: optParam Nat 0
start := 0: ?m.2199
0) (stop: optParam Nat (size xs)
stop := xs: Array α
xs.size: {α : Type ?u.2211} → Array α → Nat
size) : α: ?m.2184
α :=
  xs: Array α
xs.minD: {α : Type ?u.2234} → [ord : Ord α] → (xs : Array α) → α → optParam Nat 0 → optParam Nat (size xs) → α
minD default: {α : Sort ?u.2245} → [self : Inhabited α] → α
default start: optParam Nat 0
start stop: optParam Nat (size xs)
stop

set_option linter.unusedVariables.funArgs false in
/--
Find the first maximal element of an array. If the array is empty, `d` is
returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
considered.
-/
@[inline]
protected def maxD: {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam Nat 0 → optParam Nat (size xs) → α
maxD [ord: Ord α
ord : Ord: Type ?u.2427 → Type ?u.2427
Ord α: ?m.2424
α]
    (xs: Array α
xs : Array: Type ?u.2430 → Type ?u.2430
Array α: ?m.2424
α) (d: α
d : α: ?m.2424
α) (start: optParam Nat 0
start := 0: ?m.2438
0) (stop: optParam Nat (size xs)
stop := xs: Array α
xs.size: {α : Type ?u.2450} → Array α → Nat
size) : α: ?m.2424
α :=
  xs: Array α
xs.minD: {α : Type ?u.2473} → [ord : Ord α] → (xs : Array α) → α → optParam Nat 0 → optParam Nat (size xs) → α
minD (ord := ord: Ord α
ord.opposite: {α : Type ?u.2481} → Ord α → Ord α
opposite) d: α
d start: optParam Nat 0
start stop: optParam Nat (size xs)
stop

set_option linter.unusedVariables.funArgs false in
/--
Find the first maximal element of an array. If the array is empty, `none` is
returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
considered.
-/
@[inline]
protected def max?: {α : Type ?u.2598} → [ord : Ord α] → (xs : Array α) → optParam Nat 0 → optParam Nat (size xs) → Option α
max? [ord: Ord α
ord : Ord: Type ?u.2598 → Type ?u.2598
Ord α: ?m.2595
α]
    (xs: Array α
xs : Array: Type ?u.2601 → Type ?u.2601
Array α: ?m.2595
α) (start: optParam Nat 0
start := 0: ?m.2607
0) (stop: optParam ?m.2618 (size xs)
stop := xs: Array α
xs.size: {α : Type ?u.2619} → Array α → Nat
size) : Option: Type ?u.2626 → Type ?u.2626
Option α: ?m.2595
α :=
  xs: Array α
xs.min?: {α : Type ?u.2642} → [ord : Ord α] → (xs : Array α) → optParam Nat 0 → optParam Nat (size xs) → Option α
min? (ord := ord: Ord α
ord.opposite: {α : Type ?u.2650} → Ord α → Ord α
opposite) start: optParam Nat 0
start stop: optParam Nat (size xs)
stop

set_option linter.unusedVariables.funArgs false in
/--
Find the first maximal element of an array. If the array is empty, `default` is
returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is
considered.
-/
@[inline]
protected def maxI: {α : Type u_1} → [ord : Ord α] → [inst : Inhabited α] → (xs : Array α) → optParam Nat 0 → optParam Nat (size xs) → α
maxI [ord: Ord α
ord : Ord: Type ?u.2738 → Type ?u.2738
Ord α: ?m.2735
α] [Inhabited: Sort ?u.2741 → Sort (max1?u.2741)
Inhabited α: ?m.2735
α]
    (xs: Array α
xs : Array: Type ?u.2744 → Type ?u.2744
Array α: ?m.2735
α) (start: optParam ?m.2748 0
start := 0: ?m.2750
0) (stop: optParam Nat (size xs)
stop := xs: Array α
xs.size: {α : Type ?u.2762} → Array α → Nat
size) : α: ?m.2735
α :=
  xs: Array α
xs.minI: {α : Type ?u.2785} → [ord : Ord α] → [inst : Inhabited α] → (xs : Array α) → optParam Nat 0 → optParam Nat (size xs) → α
minI (ord := ord: Ord α
ord.opposite: {α : Type ?u.2793} → Ord α → Ord α
opposite) start: optParam Nat 0
start stop: optParam Nat (size xs)
stop

end Array


namespace Subarray

/--
The empty subarray.
-/
protected def empty: {α : Type u_1} → Subarray α
empty : Subarray: Type ?u.2916 → Type ?u.2916
Subarray α: ?m.2913
α where
  as := #[]: Array ?m.2923
#[]
  start := 0: ?m.2929
0
  stop := 0: ?m.2938
0
  h₁ := Nat.le_refl: ∀ (n : Nat), n ≤ n
Nat.le_refl 0: ?m.2941
0
  h₂ := Nat.le_refl: ∀ (n : Nat), n ≤ n
Nat.le_refl 0: ?m.2944
0

instance: {α : Type u_1} → EmptyCollection (Subarray α)
instance : EmptyCollection: Type ?u.3052 → Type ?u.3052
EmptyCollection (Subarray: Type ?u.3053 → Type ?u.3053
Subarray α: ?m.3049
α) :=
  ⟨Subarray.empty: {α : Type ?u.3061} → Subarray α
Subarray.empty⟩

instance: {α : Type u_1} → Inhabited (Subarray α)
instance : Inhabited: Sort ?u.3118 → Sort (max1?u.3118)
Inhabited (Subarray: Type ?u.3119 → Type ?u.3119
Subarray α: ?m.3115
α) :=
  ⟨{}: ?m.3128
{}⟩

/--
Check whether a subarray is empty.
-/
@[inline]
def isEmpty: {α : Type ?u.3218} → Subarray α → Bool
isEmpty (as: Subarray α
as : Subarray: Type ?u.3218 → Type ?u.3218
Subarray α: ?m.3215
α) : Bool: Type
Bool :=
  as: Subarray α
as.start: {α : Type ?u.3225} → Subarray α → Nat
start == as: Subarray α
as.stop: {α : Type ?u.3228} → Subarray α → Nat
stop

/--
Check whether a subarray contains an element.
-/
@[inline]
def contains: {α : Type u_1} → [inst : BEq α] → Subarray α → α → Bool
contains [BEq: Type ?u.3299 → Type ?u.3299
BEq α: ?m.3296
α] (as: Subarray α
as : Subarray: Type ?u.3302 → Type ?u.3302
Subarray α: ?m.3296
α) (a: α
a : α: ?m.3296
α) : Bool: Type
Bool :=
  as: Subarray α
as.any: {α : Type ?u.3312} → (α → Bool) → Subarray α → Bool
any (· == a: α
a)

/--
Remove the first element of a subarray. Returns the element and the remaining
subarray, or `none` if the subarray is empty.
-/
def popHead?: {α : Type ?u.3393} → Subarray α → Option (α × Subarray α)
popHead? (as: Subarray α
as : Subarray: Type ?u.3393 → Type ?u.3393
Subarray α: ?m.3390
α) : Option: Type ?u.3396 → Type ?u.3396
Option (α: ?m.3390
α × Subarray: Type ?u.3399 → Type ?u.3399
Subarray α: ?m.3390
α) :=
  if h: ?m.3480
h : as: Subarray α
as.start: {α : Type ?u.3404} → Subarray α → Nat
start < as: Subarray α
as.stop: {α : Type ?u.3407} → Subarray α → Nat
stop
    then
      let head: ?m.3431
head := as: Subarray α
as.as: {α : Type ?u.3432} → Subarray α → Array α
as.get: {α : Type ?u.3434} → (a : Array α) → Fin (Array.size a) → α
get ⟨as: Subarray α
as.start: {α : Type ?u.3445} → Subarray α → Nat
start, Nat.lt_of_lt_of_le: ∀ {n m k : Nat}, n < m → m ≤ k → n < k
Nat.lt_of_lt_of_le h: ?m.3428
h as: Subarray α
as.h₂: ∀ {α : Type ?u.3454} (self : Subarray α), self.stop ≤ Array.size self.as
h₂⟩
      let tail: ?m.3458
tail :=
        { as: Subarray α
as with
          start := as: Subarray α
as.start: {α : Type ?u.3495} → Subarray α → Nat
start + 1: ?m.3498
1
          h₁ := Nat.le_of_lt_succ: ∀ {m n : Nat}, m < Nat.succ n → m ≤ n
Nat.le_of_lt_succ $ Nat.succ_lt_succ: ∀ {n m : Nat}, n < m → Nat.succ n < Nat.succ m
Nat.succ_lt_succ h: ?m.3428
h  }
      some: {α : Type ?u.3461} → α → Option α
some (head: ?m.3431
head, tail: ?m.3458
tail)
    else
      none: {α : Type ?u.3482} → Option α
none

end Subarray