def Chapter6.foldr1₀ {a : Type} (f : a → a → a) (xs : List a) (h : xs ≠ []) : a

Equations

• Chapter6.foldr1₀ f xs h = if h₁ : xs.length = 1 then xs.head ⋯ else match xs, h, h₁ with | b :: bs, h, h₁ => f b (Chapter6.foldr1₀ f bs ⋯)

def Chapter6.foldr1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a

Equations

• Chapter6.foldr1 f [] = default
• Chapter6.foldr1 f [x_1] = x_1
• Chapter6.foldr1 f (x_1 :: xs) = f x_1 (Chapter6.foldr1 f xs)

def Chapter6.foldl1 {a : Type} [Inhabited a] (f : a → a → a) : List a → a

Equations

• Chapter6.foldl1 f [] = default
• Chapter6.foldl1 f (x_1 :: xs) = List.foldl f x_1 xs

def Chapter6.minimum {a : Type} [Inhabited a] [Min a] : List a → a

Equations

• Chapter6.minimum = Chapter6.foldr1 min

def Chapter6.maximum {a : Type} [Inhabited a] [Max a] : List a → a

Equations

• Chapter6.maximum = Chapter6.foldr1 max

def Chapter6.minmax₀ {a : Type} [Inhabited a] [Max a] [Min a] : List a → a × a

Equations

• Chapter6.minmax₀ [] = default
• Chapter6.minmax₀ (x_1 :: xs) = List.foldr (fun (x : a) (q : a × a) => (x ⊓ q.1, x ⊔ q.2)) (x_1, x_1) xs

def Chapter6.minmax₁ {a : Type} [Inhabited a] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → a × a

Equations

• Chapter6.minmax₁ [] = default
• Chapter6.minmax₁ (x_1 :: xs) = List.foldr (fun (x : a) (q : a × a) => if x < q.1 then (x, q.2) else if x > q.2 then (q.1, x) else (q.1, q.2)) (x_1, x_1) xs

@[irreducible]

def Chapter6.minmax₂ {a : Type} [Inhabited a] [Max a] [Min a] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → a × a

Equations

• One or more equations did not get rendered due to their size.
• Chapter6.minmax₂ [] = default

def Chapter6.mkPairs {a : Type} [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] : List a → List (a × a)

Equations

• Chapter6.mkPairs [] = []
• Chapter6.mkPairs [x_1] = [(x_1, x_1)]
• Chapter6.mkPairs (x_1 :: y :: xs) = if x_1 ≤ y then (x_1, y) :: Chapter6.mkPairs xs else (y, x_1) :: Chapter6.mkPairs xs

def Chapter6.minmax {a : Type} [Inhabited a] [Max a] [Min a] [LE a] [DecidableRel fun (x1 x2 : a) => x1 ≤ x2] (xs : List a) : a × a

Equations

• One or more equations did not get rendered due to their size.

def Chapter6.select₀ {a : Type} [Inhabited a] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (k : ℕ) (xs : List a) : a

Equations

• Chapter6.select₀ k xs = (Chapter5.Quicksort.qsort₁ xs)[k - 1]!

def Chapter6.median {a : Type} [Inhabited a] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (xs : List a) : a

Equations

• Chapter6.median xs = Chapter6.select₀ ((xs.length + 1) / 2) xs

@[irreducible]

def Chapter6.group {a : Type} [DecidableRel fun (x1 x2 : a) => x1 = x2] (n : ℕ) (xs : List a) : List (List a)

Equations

• Chapter6.group n xs = if h₁ : n = 0 then [] else if h₂ : xs = [] then [] else have p := List.splitAt n xs; have this := ⋯; p.1 :: Chapter6.group n p.2

def Chapter6.medians {a : Type} [Inhabited a] [DecidableRel fun (x1 x2 : a) => x1 = x2] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

Equations

• Chapter6.medians = List.map ((fun (xs : List a) => xs[(xs.length + 1) / 2 - 1]!) ∘ Chapter5.Quicksort.qsort₁) ∘ Chapter6.group 5

def Chapter6.pivot {a : Type} [Inhabited a] [DecidableRel fun (x1 x2 : a) => x1 = x2] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → a

Equations

• Chapter6.pivot [x_1] = x_1
• Chapter6.pivot x✝ = (fun (xs : List a) => Chapter6.select₀ ((xs.length + 1) / 2) xs) (Chapter6.medians x✝)

partial def Chapter6.qsort {a : Type} [Inhabited a] [DecidableRel fun (x1 x2 : a) => x1 = x2] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] : List a → List a

partial def Chapter6.select {a : Type} [Inhabited a] [DecidableRel fun (x1 x2 : a) => x1 = x2] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (k : ℕ) (xs : List a) (ok : k ≤ xs.length) : a

theorem Chapter6.partition3_length {a : Type} [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] [DecidableRel fun (x1 x2 : a) => x1 = x2] (y : a) (xs : List a) : (Chapter4.BST2.partition3 y xs).2.2.length + (Chapter4.BST2.partition3 y xs).2.1.length + (Chapter4.BST2.partition3 y xs).1.length = xs.length

def Chapter6.select' {a : Type} [Inhabited a] [DecidableRel fun (x1 x2 : a) => x1 = x2] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (k : ℕ) (xs : List a) (q : k ≤ xs.length) : a

Equations

• Chapter6.select' k xs q = Chapter6.select'.help k xs k xs q xs.length

@[irreducible]

def Chapter6.select'.help {a : Type} [Inhabited a] [DecidableRel fun (x1 x2 : a) => x1 = x2] [LT a] [DecidableRel fun (x1 x2 : a) => x1 < x2] (k : ℕ) (xs : List a) (k✝ : ℕ) (xs✝ : List a) (q : k✝ ≤ xs✝.length) (fuel : ℕ) : a

Equations

• One or more equations did not get rendered due to their size.
• Chapter6.select'.help k✝ xs✝ k xs q 0 = panicWithPosWithDecl "Fad.Chapter6" "Chapter6.select'.help" 222 10 "Never here"