Lemmas on vectors, arrays, lists, ranges and numbers for the contracts

Lemmas that Lean core lacks, under their names in the namespaces of core, on vectors (the entries after Vector.set! and after a fold of it, of Vector.ofFn f and of the array of a vector), arrays (the entries after Array.set!, Array.push, Array.pop, Array.map, a concatenation and Array.eraseIdxIfInBounds, the cursor of a loop over an array, an array that extends another, the entries of an array whose list extends that of another), byte arrays (the size of a byte array made from an array, the bytes after ByteArray.set!), lists (filters and List.flatMap over ranges, a list read by its indices, tests by the entries, prefixes, the cursors of loops over two lists), ranges (the cursor of a loop over [a:m]), natural numbers and integers (residues and quotients, Barrett's estimate, the remainder and the quotient by a reciprocal, the steps of the binary algorithm for the gcd), Except and strings. The lemmas on 64-bit words are in Ratpoints.Proof.Bits.

Main definitions

• Array.Extends: an array extends another, position by position.

Implementation notes

The file uses Lean core and Std only, so that the grind calls of the proofs see only the lemmas of core, untouched by the updates of Mathlib.

Vectors

theorem Vector.getElem!_set! {α : Type u} [Inhabited α] {n : Nat} {xs : Vector α n} {i j : Nat} {x : α} (hj : j < n) : (xs.set! i x)[j]! = if i = j then x else xs[j]!

theorem Vector.getElem!_set!_self {α : Type u} [Inhabited α] {n i : Nat} {xs : Vector α n} {x : α} (hi : i < n) : (xs.set! i x)[i]! = x

theorem Vector.getElem!_set!_ne {α : Type u} [Inhabited α] {n i j : Nat} {xs : Vector α n} {x : α} (h : i ≠ j) : (xs.set! i x)[j]! = xs[j]!

theorem Vector.getElem!_fold_set! {α : Type u} [Inhabited α] {n : Nat} {xs : Vector α n} {base k : Nat} (g : Nat → α → α) {y : Nat} (hy : y < n) : (k.fold (fun (l : Nat) (x : l < k) (v : Vector α n) => v.set! (base + l) (g l v[base + l]!)) xs)[y]! = if base ≤ y ∧ y < base + k then g (y - base) xs[y]! else xs[y]!

Setting the entries base, …, base + k - 1 one after the other, entry base + l to g l of its value.

theorem Vector.getElem!_ofFn {α : Type u} [Inhabited α] {n : Nat} {f : Fin n → α} {i : Nat} (h : i < n) : (ofFn f)[i]! = f ⟨i, h⟩

theorem Vector.getElem!_set {α : Type u} [Inhabited α] {n : Nat} {xs : Vector α n} {i j : Nat} {x : α} (hi : i < n) (hj : j < n) : (xs.set i x hi)[j]! = if i = j then x else xs[j]!

theorem Vector.getElem!_toArray {α : Type u} [Inhabited α] {n : Nat} (xs : Vector α n) (i : Nat) : xs.toArray[i]! = xs[i]!

Arrays

theorem Array.getElem!_set! {α : Type u} [Inhabited α] {xs : Array α} {i j : Nat} {x : α} (hj : j < xs.size) : (xs.set! i x)[j]! = if i = j then x else xs[j]!

theorem Array.getElem!_toVector {α : Type u} [Inhabited α] {xs : Array α} (i : Nat) : xs.toVector[i]! = xs[i]!

theorem Array.getElem!_map_range {α : Type u} [Inhabited α] (f : Nat → α) {n j : Nat} (hj : j < n) : (map f (range n))[j]! = f j

theorem Array.drop_toList_eq_getElem!_cons {α : Type u} [Inhabited α] {xs : Array α} {n : Nat} (h : n < xs.size) : List.drop n xs.toList = xs[n]! :: List.drop (n + 1) xs.toList

The list of an array from a position n within it on: its entry n, then the rest.

theorem Array.getElem!_append {α : Type u} [Inhabited α] {xs ys : Array α} (i : Nat) : (xs ++ ys)[i]! = if i < xs.size then xs[i]! else ys[i - xs.size]!

theorem Array.size_fold_append {α : Type u} (w : Array α) (k : Nat) : (k.fold (fun (x : Nat) (x_1 : x < k) (s : Array α) => s ++ w) #[]).size = w.size * k

The array w written k times one after the other has k times its size.

theorem Array.getElem!_fold_append {α : Type u} [Inhabited α] (w : Array α) {k x : Nat} (hx : x < w.size * k) : (k.fold (fun (x : Nat) (x_1 : x < k) (s : Array α) => s ++ w) #[])[x]! = w[x % w.size]!

Entry x of the array w written k times one after the other is entry x mod w.size of w.

theorem Array.getElem!_mem {α : Type u} [Inhabited α] {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]! ∈ xs

theorem Array.size_pop_lt_of_back?_eq_some {α : Type u} {xs : Array α} {x : α} (h : xs.back? = some x) : xs.pop.size < xs.size

theorem Array.back!_eq_getElem! {α : Type u} [Inhabited α] {xs : Array α} : xs.back! = xs[xs.size - 1]!

theorem Array.back!_ne_of_back?_ne {α : Type u} [Inhabited α] {xs : Array α} {a : α} (hs : xs.size ≠ 0) (h : xs.back? ≠ some a) : xs.back! ≠ a

theorem Array.size_ne_zero_of_back!_ne {α : Type u} [Inhabited α] {xs : Array α} (h : xs.back! ≠ default) : xs.size ≠ 0

theorem Array.back!_map {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] {f : α → β} (hf : f default = default) (xs : Array α) : (map f xs).back! = f xs.back!

theorem Array.back!_map_range {α : Type u} [Inhabited α] (f : Nat → α) {n : Nat} (hn : n ≠ 0) : (map f (range n)).back! = f (n - 1)

theorem Array.getElem!_push_lt {α : Type u} [Inhabited α] {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) : (xs.push x)[i]! = xs[i]!

theorem Array.getElem!_push_eq {α : Type u} [Inhabited α] {xs : Array α} {x : α} : (xs.push x)[xs.size]! = x

theorem Array.getElem!_map {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] {f : α → β} (hf : f default = default) (xs : Array α) (i : Nat) : (map f xs)[i]! = f xs[i]!

theorem Array.getElem!_ofFn {α : Type u} [Inhabited α] {n : Nat} (f : Fin n → α) {i : Nat} (hi : i < n) : (ofFn f)[i]! = f ⟨i, hi⟩

theorem Array.getElem!_foldl_set!_eq_true {α : Type u} (f : α → Nat) (l : List α) {A : Array Bool} {i : Nat} (hi : i < A.size) (h : A[i]! = true ∨ ∃ (y : α), y ∈ l ∧ f y = i) : (List.foldl (fun (A : Array Bool) (y : α) => A.set! (f y) true) A l)[i]! = true

Setting the entries f y to true for the y of a list keeps the entries that are true and makes those entries true (within the size).

theorem Array.getElem!_pop {α : Type u} [Inhabited α] {xs : Array α} {i : Nat} : xs.pop[i]! = if i < xs.size - 1 then xs[i]! else default

theorem Array.getElem!_pop_of_back!_eq {α : Type u} [Inhabited α] {xs : Array α} (h : xs.back! = default) (i : Nat) : xs.pop[i]! = xs[i]!

theorem Array.getElem!_foldl_setIfInBounds {α : Type u} (l : List α) (f : α → Nat) {w : Array Bool} {t : Nat} (ht : t < w.size) : (List.foldl (fun (w : Array Bool) (i : α) => w.setIfInBounds (f i) true) w l)[t]! = (w[t]! || l.any fun (x : α) => f x == t)

The entries of an array of Booleans that a fold of setIfInBounds · true over the list l marks: entry t in range is set when it was set before or one of the positions f i is t.

theorem Array.forall_mem_toList_push {α : Type u} {xs : Array α} {x : α} {P : α → Prop} (h : ∀ (y : α), y ∈ xs.toList → P y) (hx : P x) (y : α) : y ∈ (xs.push x).toList → P y

A property of the members of the list of an array holds after a push of a member that has it: Array.forall_mem_push for the members of the list, as invariants of loops state them.

theorem Array.pairwise_map_toList_push {α : Type u} {β : Type v} {R : β → β → Prop} {f : α → β} {xs : Array α} {x : α} : List.Pairwise R (List.map f (xs.push x).toList) ↔ List.Pairwise R (List.map f xs.toList) ∧ ∀ (y : α), y ∈ xs.toList → R (f y) (f x)

The images under f of the members of the list of an array after a push of x are pairwise related by R exactly when those before are and each of them is related to the image of x, as invariants of loops state the order of the entries.

theorem Array.any_id_eq_true_of_getElem!_eq_true {xs : Array Bool} {i : Nat} (h : xs[i]! = true) : xs.any id = true

xs[i]! = true gives a true entry of xs, since xs[i]! is false out of range.

theorem Array.mem_of_forIn_toList_eq_append_cons {α : Type u} {xs : Array α} {pref suff : List α} {cur : α} (hl : ForIn.toList xs = pref ++ cur :: suff) : cur ∈ xs

The cursor of a loop over the array xs is an entry of xs.

theorem Array.getElem!_replicate_none {α : Type u} (n K : Nat) : (replicate n none)[K]! = none

theorem Array.getElem!_of_toList_eq_map {α : Type u} {β : Type v} [Inhabited β] {xs : Array β} {l : List α} {f : α → β} (h : xs.toList = List.map f l) {n : Nat} (hn : n < l.length) : xs[n]! = f l[n]

theorem Array.flatMap_range_size_getElem!_of_toList_eq_map {α : Type u} {β : Type v} [Inhabited α] {xs : Array α} {n : Nat} {f : Nat → α} (h : xs.toList = List.map f (List.range n)) (F : Nat → α → List β) : List.flatMap (fun (i : Nat) => F i xs[i]!) (List.range xs.size) = List.flatMap (fun (i : Nat) => F i (f i)) (List.range n)

A list over the positions of an array whose list is (List.range n).map f, read with [i]!, is that over the values of f.

theorem Array.getElem!_eq_of_toList_eq_append {α : Type u} [Inhabited α] {xs ys : Array α} {L : List α} (h : ys.toList = xs.toList ++ L) {j : Nat} (hj : j < xs.size) : ys[j]! = xs[j]!

The entries of an array whose list extends that of xs are those of xs at its positions.

theorem Array.getElem!_mem_of_toList_eq_append {α : Type u} [Inhabited α] {xs ys : Array α} {L : List α} (h : ys.toList = xs.toList ++ L) {j : Nat} (hj : xs.size ≤ j) (hj' : j < ys.size) : ys[j]! ∈ L

The entries of an array whose list is that of xs followed by L, beyond the positions of xs, are entries of L.

theorem Array.set!_set! {α : Type u} (xs : Array α) (i : Nat) (a b : α) : (xs.set! i a).set! i b = xs.set! i b

Setting an entry twice keeps the second value.

theorem Array.getElem!_set!_eq_or {α : Type u} [Inhabited α] (xs : Array α) (i j : Nat) (x : α) : (xs.set! i x)[j]! = x ∨ (xs.set! i x)[j]! = xs[j]!

theorem Array.getElem!_take_toList {α : Type u} [Inhabited α] {xs : Array α} {m j : Nat} (hj : j < m) (hm : m ≤ xs.size) : (List.take m xs.toList)[j]! = xs[j]!

theorem Array.getElem_take_toList {α : Type u} [Inhabited α] {xs : Array α} {m j : Nat} (hj : j < (List.take m xs.toList).length) : (List.take m xs.toList)[j] = xs[j]!

theorem Array.mem_take_toList_of_lt {α : Type u} [Inhabited α] {xs : Array α} {m j : Nat} (hj : j < m) (hm : m ≤ xs.size) : xs[j]! ∈ List.take m xs.toList

theorem Array.exists_eq_of_mem_take_toList {α : Type u} [Inhabited α] {xs : Array α} {m : Nat} {p : α} (hp : p ∈ List.take m xs.toList) : ∃ (j : Nat), j < m ∧ j < xs.size ∧ p = xs[j]!

theorem Array.any_push_id_eq_false_iff {t : Array Bool} {a : Bool} : (t.push a).any id = false ↔ List.count true t.toList = 0 ∧ a = false

A table with an entry pushed at its end has no true entry exactly when the table counts no true entry and the entry pushed is false.

theorem Array.getElem!_of_getElem? {α : Type u} [Inhabited α] {xs : Array α} {i : Nat} {x : α} (h : xs[i]? = some x) : xs[i]! = x

def Array.Extends {α : Type u} (a b : Array α) : Prop

The array b extends the array a: each entry of a is at its index in b. This is a.toList <+: b.toList (List.prefix_iff_getElem?), stated entry by entry, so that an entry of a is read off b in one step.

Equations

• a.Extends b = ∀ (i : Nat) (x : α), a[i]? = some x → b[i]? = some x

theorem Array.Extends.refl {α : Type u} (a : Array α) : a.Extends a

theorem Array.Extends.trans {α : Type u} {a b c : Array α} (hab : a.Extends b) (hbc : b.Extends c) : a.Extends c

theorem Array.extends_push {α : Type u} (a : Array α) (x : α) : a.Extends (a.push x)

theorem Array.extends_ite_push {α : Type u} (b : Bool) (a : Array α) (x : α) : a.Extends (if b = true then a.push x else a)

theorem Array.size_eraseIdxIfInBounds_of_lt {α : Type u} {xs : Array α} {n : Nat} (h : n < xs.size) : (xs.eraseIdxIfInBounds n).size = xs.size - 1

theorem Array.getElem_eraseIdxIfInBounds_of_lt {α : Type u} {xs : Array α} {n i : Nat} (hn : n < xs.size) (hi : i < n) (h : i < (xs.eraseIdxIfInBounds n).size) : (xs.eraseIdxIfInBounds n)[i] = xs[i]

Byte arrays

@[simp]

theorem ByteArray.size_mk (d : Array UInt8) : { data := d }.size = d.size

@[simp]

theorem ByteArray.size_emptyWithCapacity (c : Nat) : (emptyWithCapacity c).size = 0

theorem ByteArray.getElem!_mk_replicate_zero (n b : Nat) : { data := Array.replicate n 0 }[b]! = 0

theorem ByteArray.getElem!_set!_of_getElem!_eq {a : ByteArray} {i j : Nat} {v : UInt8} (hj : j < a.size) (h : a[j]! = v) : (a.set! i v)[j]! = v

Lists

theorem List.getElem!_set {α : Type u} [Inhabited α] {l : List α} {i j : Nat} (h : j < l.length) (x : α) : (l.set i x)[j]! = if i = j then x else l[j]!

theorem List.getElem!_mem {α : Type u} [Inhabited α] {l : List α} {i : Nat} (h : i < l.length) : l[i]! ∈ l

theorem List.range_prefix_range {k m : Nat} (h : k ≤ m) : range k <+: range m

The numbers below k ≤ m come first among those below m.

theorem List.filter_range_eq_of_le {p : Nat → Bool} {k n : Nat} (hk : k ≤ n) (hz : ∀ (j : Nat), j ≥ k → j < n → p j = false) : filter p (range n) = filter p (range k)

theorem List.filter_range_succ_eq_append {p : Nat → Bool} {k c : Nat} (hk : k ≤ c) (hc : p c = true) (hz : ∀ (j : Nat), j ≥ k → j < c → p j = false) : filter p (range (c + 1)) = filter p (range k) ++ [c]

theorem List.filter_map_range_eq_map_range (s : Int) (k₁ k₂ m : Nat) : filter (fun (a : Int) => decide (s + ↑k₁ ≤ a ∧ a + ↑k₂ < s + ↑m)) (map (fun (k : Nat) => s + ↑k) (range m)) = map (fun (k : Nat) => s + ↑k₁ + ↑k) (range (m - k₁ - k₂))

Of the integers s, …, s + m - 1, those from s + k₁ to s + m - 1 - k₂: the m - k₁ - k₂ integers from s + k₁ on; for m ≤ k₁ + k₂ there are none, and the truncated subtraction gives 0.

theorem List.filter_map_range_eq_map_range' (s lo hi : Int) (m : Nat) : filter (fun (a : Int) => decide (lo ≤ a ∧ a ≤ hi)) (map (fun (k : Nat) => s + ↑k) (range m)) = map (fun (k : Nat) => s + ↑(lo - s).toNat + ↑k) (range (m - (lo - s).toNat - (s + ↑m - 1 - hi).toNat))

Of the integers s, …, s + m - 1, those from lo to hi: the integers from s + (lo - s).toNat, the larger of s and lo, on, as many as m less the truncated differences (lo - s).toNat and (s + m - 1 - hi).toNat.

theorem List.filter_map_range_eq_map_range_of_le {s lo hi : Int} {m : Nat} (h1 : s ≤ lo) (h2 : hi < s + ↑m) : filter (fun (a : Int) => decide (lo ≤ a ∧ a ≤ hi)) (map (fun (k : Nat) => s + ↑k) (range m)) = map (fun (k : Nat) => lo + ↑k) (range (hi + 1 - lo).toNat)

Of the integers s, …, s + m - 1, for s ≤ lo and hi < s + m, those from lo to hi.

theorem List.flatMap_range_map_filter {g : Nat → Nat → Bool} {a : Int} {p : Int → Bool} {m : Nat} (hg : ∀ (y : Nat), y < m → ∀ (t : Nat), g y t = (decide (t < 64) && p (a + 64 * ↑y + ↑t))) : flatMap (fun (y : Nat) => map (fun (t : Nat) => a + 64 * ↑y + ↑t) (filter (g y) (range 64))) (range m) = filter p (map (fun (k : Nat) => a + ↑k) (range (64 * m)))

The positions t of the blocks y < m that pass the test g y, read as the integers a + 64 y + t, in increasing order, are the integers a, …, a + 64 m - 1 that pass p, when g y t is t < 64 and p (a + 64 y + t): for g y the bits of a word y, the numerators of the set bits of m words.

theorem List.flatMap_range'_map_filter {g : Nat → Nat → Bool} {p : Nat → Bool} {w0 n : Nat} (hg : ∀ (w : Nat), w0 ≤ w → w < w0 + n → ∀ (t : Nat), t < 64 → g w t = p (64 * w + t)) : flatMap (fun (w : Nat) => map (fun (x : Nat) => 64 * w + x) (filter (g w) (range 64))) (range' w0 n) = filter p (range' (64 * w0) (64 * n))

The positions t < 64 of the blocks w = w0, …, w0 + n - 1 that pass the test g w, read as the numbers 64 w + t, in increasing order, are the numbers 64 w0, …, 64 (w0 + n) - 1 that pass p, when g w t is p (64 w + t): for g w the bits of a word w, the numbers of the set bits of n words; List.flatMap_range_map_filter for natural numbers and blocks from w0 on.

theorem List.filter_range'_le_and_le {a n lo hi : Nat} (ha : a ≤ lo) (hn : hi < a + n) : filter (fun (b : Nat) => decide (lo ≤ b) && decide (b ≤ hi)) (range' a n) = range' lo (hi + 1 - lo)

Of the numbers a, …, a + n - 1, which cover lo, …, hi, those from lo to hi are the numbers lo, …, hi.

theorem List.range'_eq_filter_range' {bLow : Nat} (hbLow : 1 ≤ bLow) (bHigh : Nat) : range' bLow (bHigh + 1 - bLow) = filter (fun (x : Nat) => decide (bLow ≤ x)) (range' 1 bHigh)

The numbers bLow, …, bHigh are those of 1, …, bHigh from bLow ≥ 1 on.

theorem List.flatMap_filter {α : Type u} {β : Type v} {l : List α} {p : α → Bool} {f : α → List β} : flatMap f (filter p l) = flatMap (fun (a : α) => if p a = true then f a else []) l

theorem List.flatMap_filter_flatMap_filter {α : Type u} {β : Type v} {γ : Type w} (l : List α) (q : α → Bool) (xs : List β) (T : α → β → Bool) (g : α → β → List γ) : flatMap (fun (b : α) => flatMap (g b) (filter (T b) xs)) (filter q l) = flatMap (fun (b : α) => flatMap (g b) (filter (fun (a : β) => q b && T b a) xs)) l

The filter of the outer list of a double List.flatMap moved into the filter of the inner one.

theorem List.foldl_gcd_natAbs_dvd (l : List Int) (g : Nat) : foldl (fun (g : Nat) (a : Int) => g.gcd a.natAbs) g l ∣ g

theorem List.foldl_gcd_natAbs_one (l : List Int) : foldl (fun (g : Nat) (a : Int) => g.gcd a.natAbs) 1 l = 1

theorem List.foldl_gcd_natAbs_dvd_natAbs {l : List Int} (g : Nat) {x : Int} (hx : x ∈ l) : foldl (fun (g : Nat) (a : Int) => g.gcd a.natAbs) g l ∣ x.natAbs

theorem List.next?_drop_map {α : Type u} {β : Type v} {f : α → β} {l pref suff : List α} {a : α} (hl : l = pref ++ a :: suff) {b : β} {rest : List β} (h : Std.Stream.next? (drop pref.length (map f l)) = some (b, rest)) : b = f a ∧ rest = drop (pref.length + 1) (map f l)

The cursor of the second list of a loop for x in l, y in l.map f, after the entries pref of l, at the entry a: the next value is f a, and the rest of the list follows.

theorem List.next?_drop_map_ne_none {α : Type u} {β : Type v} (f : α → β) {l pref suff : List α} {a : α} (hl : l = pref ++ a :: suff) : Std.Stream.next? (drop pref.length (map f l)) ≠ none

The second list of a loop for x in l, y in l.map f does not run out before the first.

theorem List.map_range_length_getElem! {α : Type u} [Inhabited α] (l : List α) : map (fun (i : Nat) => l[i]!) (range l.length) = l

The entries of a list read by their indices are the list.

theorem List.all_range_length_getElem! {α : Type u} [Inhabited α] (l : List α) (P : α → Bool) : ((range l.length).all fun (i : Nat) => P l[i]!) = l.all P

A test of the entries of a list by their indices is the test of the list.

theorem List.flatMap_range_length_getElem! {α : Type u} {β : Type v} [Inhabited α] (l : List α) (g : α → List β) : flatMap (fun (i : Nat) => g l[i]!) (range l.length) = flatMap g l

A list over the positions of a list, read by their indices, is that over its entries.

theorem List.all_and_left {α : Type u} {l : List α} (hl : l ≠ []) (c : Bool) (P : α → Bool) : (l.all fun (a : α) => c && P a) = (c && l.all P)

A test of the entries of a nonempty list that and-s a fixed Boolean with a test is the Boolean and-ed with the test of the list.

theorem List.all_congr_left {α : Type u} {l : List α} {P Q : α → Bool} (h : ∀ (a : α), a ∈ l → P a = Q a) : l.all P = l.all Q

theorem List.filter_append_filter_of_pairwise {α : Type u} {R : α → α → Prop} [Std.Asymm R] {l : List α} (hl : Pairwise R l) {p q : α → Bool} (h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → p a = true → q b = true → R a b) : filter p l ++ filter q l = filter (fun (a : α) => p a || q a) l

The elements of a list that pass p followed by those that pass q are those that pass one of the two, for a list whose elements are pairwise in an asymmetric relation R that holds from every element that passes p to every element that passes q: none passes both, and those that pass p come first.

theorem List.flatMap_filter_eq_filter_any {l : List Int} (hl : Pairwise (fun (x1 x2 : Int) => x1 < x2) l) {rs : List (Int × Int)} (hrs : Pairwise (fun (r s : Int × Int) => r.snd < s.fst) rs) (q : Int → Bool) : flatMap (fun (r : Int × Int) => filter (fun (a : Int) => decide (r.fst ≤ a ∧ a ≤ r.snd) && q a) l) rs = filter (fun (a : Int) => (rs.any fun (r : Int × Int) => decide (r.fst ≤ a ∧ a ≤ r.snd)) && q a) l

Over ranges lo, …, hi of integers that are increasing and strictly apart, the elements of an increasing list l that lie in each range and pass q, range after range, are the elements of l that lie in one of the ranges and pass q: the loop of Ratpoints.Sieve.sift over the search intervals.

theorem List.map_some_filterMap_of_forall_isSome {α : Type u} {β : Type v} {f : α → Option β} {l : List α} (h : ∀ (a : α), a ∈ l → (f a).isSome = true) : map some (filterMap f l) = map f l

When f is some on every element of l, l.filterMap f holds one value for each element, in their order.

theorem List.take_append_take_drop {α : Type u} (l : List α) {m n : Nat} (h : m ≤ n) : take m l ++ take (n - m) (drop m l) = take n l

List.take_add for the lengths m and n - m, for m ≤ n.

theorem List.forall_mem_drop_of_forall_getElem! {α : Type u} [Inhabited α] {P : α → Prop} {l : List α} {m n : Nat} (hn : ∀ (e : α), e ∈ drop n l → P e) (hmn : ∀ (k : Nat), m ≤ k → k < n → P l[k]!) (e : α) : e ∈ drop m l → P e

A property of the elements of l.drop n and of the entries l[k]! for m ≤ k < n holds for the elements of l.drop m.

theorem List.filter_flatMap_range'_sub_add_one {α : Type u} {g : Nat → List α} {keep : α → Bool} {a b : Nat} (hab : a ≤ b) : filter keep (flatMap g (range' a (b - a + 1))) = filter keep (flatMap g (range' a (b - a))) ++ filter keep (g b)

For a ≤ b, the elements of the lists g a, …, g b that pass keep are those of g a, …, g (b - 1) followed by those of g b.

theorem List.mem_filter_range'_of_le {keep : Nat → Bool} {a b e : Nat} (hab : a ≤ b) (hbe : b ≤ e) (hk : keep b = true) : b ∈ filter keep (range' a (e + 1 - a))

A number b from a to e that passes keep is among the numbers a, …, e that pass it.

theorem List.mem_filter_map_range'_of_toList_eq_append_cons {α : Type u} {f : Nat → α} {keep : α → Bool} {a e cur : Nat} {pref suff : List Nat} (hl : ForIn.toList [a:e + 1] = pref ++ cur :: suff) (hk : keep (f cur) = true) : f cur ∈ filter keep (map f (range' a (e + 1 - a)))

The image f cur of the cursor cur of a loop over [a:e + 1] is among the images of a, …, e that pass keep, when it passes keep.

theorem List.filter_map_append_singleton_of_pos {α : Type u} {β : Type v} {f : α → β} {keep : β → Bool} {pref : List α} {cur : α} (hk : keep (f cur) = true) : filter keep (map f (pref ++ [cur])) = filter keep (map f pref) ++ [f cur]

The images under f of pref ++ [cur] that pass keep are those of pref followed by f cur, when f cur passes it.

theorem List.takeWhile_eq_self_of_forall {α : Type u} {p : α → Bool} {l : List α} (h : ∀ (a : α), a ∈ l → p a = true) : takeWhile p l = l

A list whose elements all pass p is its own longest prefix that passes p: the direction from right to left of Mathlib's List.takeWhile_eq_self_iff, restated for the files without Mathlib.

Ranges

theorem Std.Legacy.Range.length_toList (a b : Nat) : (ForIn.toList [a:b]).length = b - a

theorem Std.Legacy.Range.add_length_eq_of_toList_eq_append_cons {a m cur : Nat} {pref suff : List Nat} (h : ForIn.toList [a:m] = pref ++ cur :: suff) : a + pref.length = cur

The form of List.eq_of_range'_eq_append_cons for the list ForIn.toList [a:m] of a loop over [a:m], in which the verification conditions state the cursor: the cursor is a plus the length of the list before it.

theorem Std.Legacy.Range.length_eq_of_toList_eq_append_cons {m cur : Nat} {pref suff : List Nat} (h : ForIn.toList [:m] = pref ++ cur :: suff) : pref.length = cur

The form of List.eq_of_range'_eq_append_cons for the list ForIn.toList [0:m] of a loop over [0:m], in which the verification conditions state the cursor: the cursor is the length of the list before it.

theorem Std.Legacy.Range.lt_of_toList_eq_append_cons {a m cur : Nat} {pref suff : List Nat} (h : ForIn.toList [a:m] = pref ++ cur :: suff) : cur < m

The form of List.mem_of_range'_eq_append_cons for the list ForIn.toList [a:m] of a loop over [a:m]: the cursor is below m.

theorem Std.Legacy.Range.mem_toList_of_lt {x m : Nat} (h : x < m) : x ∈ ForIn.toList [:m]

A number below m is in the list of a loop over [0:m].

theorem Std.Legacy.Range.length_add_length_add_one_of_toList_eq_append_cons {a m cur : Nat} {pref suff : List Nat} (h : ForIn.toList [a:m] = pref ++ cur :: suff) : pref.length + suff.length + 1 = m - a

The form of List.length_of_range'_eq_append_cons for the list ForIn.toList [a:m] of a loop over [a:m]: the lists before and after the cursor have m - a - 1 entries together.

Natural numbers

theorem Nat.mul_sub_one_div_div_mul_le (u N p : Nat) : u * ((N - 1) / p) / N * p ≤ u

Barrett's estimate ⌊u ⌊(N - 1) / p⌋ / N⌋ of the quotient ⌊u / p⌋ is at most it: its product with p is at most u.

theorem Nat.lt_mul_sub_one_div_div_add_two_mul {u N p : Nat} (hp : 0 < p) (hu : u < N) : u < (u * ((N - 1) / p) / N + 2) * p

Barrett's estimate q = ⌊u ⌊(N - 1) / p⌋ / N⌋ of the quotient ⌊u / p⌋ for u < N is at least it less one: u < (q + 2) p.

theorem Nat.mul_add_lt_mul_of_lt {s a c P p : Nat} (hs : s < P) (ha : a ≤ p) (hc : c < p) : s * a + c < P * p

One step of Horner's rule with an argument at most p and a coefficient below p multiplies a bound on the accumulator by p.

theorem Nat.add_le_of_lt_of_dvd_of_mod_eq_zero {x m q : Nat} (hxm : x < m) (hq : q ∣ m) (hx : x % q = 0) : x + q ≤ m

After a multiple x < m of a divisor q of m, the next multiple x + q is at most m.

theorem Nat.mul_add_lt_mul_of_lt_of_lt' {k c j κ : Nat} (hj : j < c) (hκ : κ < k) : k * j + κ < c * k

Word κ < k of block j < c of c blocks of k words is below c k: the statement of Batteries' Nat.mul_add_lt_mul_of_lt_of_lt, for the files that use Lean core only.

theorem Nat.mul_add_mod_mul_of_lt {k x κ p : Nat} (hκ : κ < k) : (k * x + κ) % (k * p) = k * (x % p) + κ

Word κ < k of block x is word κ of block x mod p in the words modulo k p.

theorem Nat.pow_lt_two_pow_of_lt {p b n N : Nat} (hp : p < 2 ^ b) (hn : b * n ≤ N) (hn0 : n ≠ 0) : p ^ n < 2 ^ N

theorem Nat.lt_add_one_mul_of_lt_mul {y n k : Nat} (h : y < n * k) : y < (n + 1) * k

theorem Nat.le_add_sub_one_mul (n : Nat) {c k : Nat} (hc : 0 < c) (hk : 0 < k) : n ≤ (n + c - 1) * k

The first n words of n + c - 1 blocks of k words, for c, k > 0, lie among them.

theorem Nat.mod_eq_ite_of_lt_two_mul {a q : Nat} (h : a < 2 * q) : a % q = if q ≤ a then a - q else a

A residue a < 2 q modulo q by one conditional subtraction.

theorem Nat.ite_eq_add_one_mod_add_one {a n : Nat} (h : a ≤ n) : (if a = n then 0 else a + 1) = (a + 1) % (n + 1)

The position after a ≤ n in a ring of the positions 0, …, n, by a test for the last.

theorem Nat.ite_mod_add_one_eq_add_one_mod {w p : Nat} (hp : 0 < p) : (if w % p + 1 = p then 0 else w % p + 1) = (w + 1) % p

The position w mod p stepped on by one, back to 0 at p, is (w + 1) mod p.

theorem Nat.ite_add_lt_eq_add_mod {m i u : Nat} (hi : i < m) (hu : u < m) : (if i + u < m then i + u else i + u - m) = (i + u) % m

The sum of two residues modulo m by one conditional subtraction.

theorem Nat.and_eq_mod_two_pow_and {x k n : Nat} (hk : k < 2 ^ n) : x &&& k = x % 2 ^ n &&& k

The bits of x &&& k for k < 2 ^ n are those of the residue of x modulo 2 ^ n.

theorem Nat.and_two_ne_zero_iff {q : Nat} (hq : q % 2 = 1) : (q &&& 2 != 0) = true ↔ q % 4 = 3

Bit 1 of an odd number is set exactly when it is 3 (mod 4).

theorem Nat.and_and_two_ne_zero_iff {n m : Nat} (hn : n % 2 = 1) (hm : m % 2 = 1) : (n &&& m &&& 2 != 0) = true ↔ n % 4 = 3 ∧ m % 4 = 3

Bit 1 of two odd numbers is set in both exactly when both are 3 (mod 4).

theorem Nat.gcd_div_two_of_mod_two {x y : Nat} (hx : x % 2 = 0) (hy : y % 2 = 1) : (x / 2).gcd y = x.gcd y

Halving an even x keeps its gcd with an odd y.

theorem Nat.exists_mul_eq_add_mul_div {u p m N δ : Nat} (hp : 0 < p) (hm : m * p = N + δ) (hu : u * δ < N) : ∃ (L : Nat), L < N ∧ m * u = L + N * (u / p) ∧ L * p = u * δ + N * (u % p)

For m p = N + δ and u δ < N, the product m u is L + N ⌊u / p⌋ for some L < N with L p = u δ + N (u mod p): the product of u with a reciprocal m of p scaled by N, rounded up when δ ≥ 0 is small.

theorem Nat.mul_mod_mul_div_eq_mod_of_mul_eq_add {u p m N δ : Nat} (hp : 0 < p) (hm : m * p = N + δ) (hu : u * δ < N) : m * u % N * p / N = u % p

The remainder by a reciprocal: for m p = N + δ and u δ < N, the low part m u mod N of the product of u with m, times p, has the high part u mod p.

theorem Nat.mul_div_eq_div_of_mul_eq_add {u p m N δ : Nat} (hp : 0 < p) (hm : m * p = N + δ) (hu : u * δ < N) : m * u / N = u / p

The quotient by a reciprocal: for m p = N + δ and u δ < N, the high part of the product of u with m is ⌊u / p⌋.

theorem Nat.gcd_eq_of_two_pow_mul_eq {x y n t : Nat} (h : 2 ^ t * y = x) (hn : n % 2 = 1) : y.gcd n = x.gcd n

Removing the factors 2 of x = 2 ^ t y keeps its gcd with an odd n.

theorem Nat.gcd_min_eq_gcd_of_two_pow_mul_eq {m n y t : Nat} (hm : m % 2 = 1) (hn : n % 2 = 1) (h : 2 ^ t * y = if m < n then n - m else m - n) : y.gcd (min m n) = m.gcd n

The odd part y of the distance of two odd numbers m and n has with the smaller of the two the gcd of m and n: the step of the binary algorithm for the gcd.

theorem Nat.add_min_lt_add_of_two_pow_mul_eq {m n y t : Nat} (hm : 0 < m) (hn : 0 < n) (h : 2 ^ t * y = if m < n then n - m else m - n) : y + min m n < m + n

A part y of the distance of two positive numbers, together with the smaller of the two, is less than their sum: the measure of the binary algorithm for the gcd decreases.

theorem Nat.mul_mod_of_mod_eq_one (a : Nat) {b q : Nat} (h : b % q = 1) : a * b % q = a % q

theorem Nat.mul_mul_mod_mod_of_mul_mod_eq_one {p u v : Nat} (b : Nat) (h : v * u % p = 1) : u * (b * v % p) % p = b % p

u (b v mod p) ≡ b (mod p) for an inverse v of u modulo p.

theorem Nat.mul_mod_eq_mul_mod_of_mod_eq {a a' : Nat} (b : Nat) {q : Nat} (h : a % q = a' % q) : a * b % q = a' * b % q

theorem Nat.mul_mod_eq_zero_iff_of_mul_mod {q u v : Nat} (huv : v * u % q = 1 % q) (b : Nat) : u * b % q = 0 ↔ b % q = 0

Scaling b by u, with an inverse v modulo q, keeps it zero modulo q or not.

theorem Nat.mul_mod_mod_eq_zero_iff_of_mul_mod {p q u v : Nat} (hpq : p ∣ q) (huv : v * u % q = 1 % q) (b : Nat) : u * b % q % p = 0 ↔ b % q % p = 0

Scaling b by u, with an inverse v modulo q, keeps its residue modulo q zero modulo a divisor p of q or not.

theorem Nat.mul_mod_eq_mul_mod_of_mul_mod_eq_one {q u x x' r r' i i' : Nat} (hx : x' % q = u * x % q) (hr : r' % q = u * r % q) (hi : i * r % q = 1) (hi' : i' * r' % q = 1) : x' * i' % q = x * i % q

The residue x i mod q, for an inverse i of r modulo q, is unchanged when x and r are both scaled by u: x' i' ≡ x i for x' ≡ u x, r' ≡ u r, i r ≡ 1 and i' r' ≡ 1.

theorem Nat.le_and_sub_mod_eq_zero_iff {a s m : Nat} (hs : s < m) : s ≤ a ∧ (a - s) % m = 0 ↔ a % m = s

theorem Nat.sub_mod_div_eq_mod_iff {a a0 m P t n : Nat} (hm : m * P = n) (ha : a < n) (haa : a % m = a0) : (a - a0) % n / m = t % P ↔ a = (a0 + m * t) % n

For a residue a ≡ a₀ (mod m) below n and m P = n, the place (a - a₀) mod n / m of a is t mod P exactly when a is (a₀ + m t) mod n.

theorem Nat.le_mul_add_sub_one_div (R : Nat) {m : Nat} (hm : 0 < m) : R ≤ m * ((R + m - 1) / m)

The multiple m ⌈R / m⌉ = m ((R + m - 1) / m) of m > 0 is at least R.

theorem Nat.mul_add_sub_one_div_lt (R : Nat) {m : Nat} (hm : 0 < m) : m * ((R + m - 1) / m) < R + m

The multiple m ⌈R / m⌉ = m ((R + m - 1) / m) of m > 0 is below R + m.

theorem Nat.mul_mod_add_mul_mod_eq_mod {p a y c M : Nat} (hy : y * M % p = 1) (hc : c % p = 0) : (a * y % p + c) * M % p = a % p

The residue a y mod p plus a multiple c of p, times an inverse M of y modulo p, is a modulo p.

theorem Nat.add_sub_mod_eq_zero_iff {N m r : Nat} (hr : r < m) : (N + (m - r)) % m = 0 ↔ N % m = r

N + (m - r) is a multiple of m exactly when N is r modulo m, for r < m.

theorem Nat.eq_of_mod_eq_zero_of_le_of_lt {p t t' : Nat} (ht : t % p = 0) (ht' : t' % p = 0) (hle : t ≤ t') (hlt : t' < t + p) : t' = t

A multiple t' of p from the multiple t of p on and below t + p is t.

theorem List.filter_range_mod_eq {m r : Nat} (hr : r < m) (N : Nat) : filter (fun (i : Nat) => i % m == r) (range N) = map (fun (j : Nat) => r + m * j) (range ((N + (m - 1 - r)) / m))

The numbers below N that are r modulo m, for r < m: r, r + m, r + 2 m, …, of which there are ⌈(N - r) / m⌉.

Integers

theorem Int.toNat_add_emod_of_lt {a : Int} {p j : Nat} (hp : 0 < p) (hj : j < (-a % ↑p).toNat) : ((a + ↑j) % ↑p).toNat = p - (-a % ↑p).toNat + j

Before the first multiple of p from a on: for r = (-a) mod p and j < r, the residue of a + j modulo p is p - r + j.

theorem Int.toNat_add_add_emod {a : Int} {p i k : Nat} (hi : i < p) : ((a + ↑((-a % ↑p).toNat + k * p + i)) % ↑p).toNat = i

From the first multiple of p from a on: for r = (-a) mod p and i < p, the residue of a + r + k p + i modulo p is i.

theorem Int.toNat_emod_lt (a : Int) {p : Nat} (hp : 0 < p) : (a % ↑p).toNat < p

@[simp]

theorem Int.toNat_natCast_emod (a b : Nat) : (↑a % ↑b).toNat = a % b

theorem Int.toNat_emod_add_mod (a : Int) (x : Nat) {p : Nat} (hp : 0 < p) : ((a % ↑p).toNat + x) % p = ((a + ↑x) % ↑p).toNat

theorem Int.toNat_mul_emod (u : Nat) (a : Int) {q : Nat} (hq : 0 < q) : (↑u * a % ↑q).toNat = u * (a % ↑q).toNat % q

theorem Int.toNat_emod_mod_of_dvd (a : Int) {m p : Nat} (hm : 0 < m) (hpm : p ∣ m) : (a % ↑m).toNat % p = (a % ↑p).toNat

theorem Int.ediv_mul_eq_ediv_mul_of_dvd {a b g : Int} (ha : g ∣ a) (hb : g ∣ b) : a / g * b = b / g * a

theorem Int.ediv_ne_zero_of_dvd {a b : Int} (hb : b ∣ a) (ha : a ≠ 0) : a / b ≠ 0

theorem Int.natAbs_sub_mul_of_mul_nonpos {a b : Int} (h : a * b ≤ 0) (q : Nat) : (a - ↑q * b).natAbs = a.natAbs + q * b.natAbs

For integers a and b of opposite signs, or one of them 0, and q ≥ 0, |a - q b| = |a| + q |b|: the step of the cofactors of the extended Euclidean algorithm.

theorem Int.dvd_natAbs_of_dvd_gcd {a : Int} {b f q : Nat} (h : ↑f % ↑b = a % ↑b) (hq : q ∣ f.gcd b) : q ∣ a.natAbs

A divisor of the gcd of f ≡ a (mod b) and b divides a.

theorem Int.toNat_emod_ne_zero_of_gcd_eq_one {p : Nat} (hp : 1 < p) {a : Int} {b : Nat} (hab : a.gcd ↑b = 1) (hb : b % p = 0) : (a % ↑p).toNat ≠ 0

A divisor p > 1 of b does not divide a numerator a prime to b.

theorem Int.ite_tmod_lt_zero_eq_emod (a : Int) {p : Int} (hp : 0 < p) : (if a.tmod p < 0 then a.tmod p + p else a.tmod p) = a % p

C's remainder a.tmod p, which truncates, plus p if it is negative, is the Euclidean remainder a % p, for p > 0.

theorem Int.toNat_emod_mul_emod (a : Int) {p : Nat} (b : Nat) (hp : 0 < p) : (a % ↑p * ↑b % ↑p).toNat = (a % ↑p).toNat * b % p

theorem Int.toNat_mul_add_natCast_mul_mod {a : Int} {p binv H : Nat} (hp : 0 < p) (h : 0 ≤ a * ↑binv + ↑(p * H)) : (a * ↑binv + ↑(p * H)).toNat % p = (a % ↑p).toNat * binv % p

The shift by the multiple p H of p keeps the residue modulo p of a binv.

theorem Int.natAbs_mul_add_le_mul {a : Int} {b p H : Nat} (ha : a.natAbs ≤ H) (hb : b < p) : (a * ↑b).natAbs + H ≤ p * H

theorem Int.natCast_sub_natCast_emod_eq_iff {i H a0 m : Nat} (ha : a0 < m) : (↑i - ↑H) % ↑m = ↑a0 ↔ i % m = (a0 + H) % m

theorem Int.neg_ediv_eq_sub_one_sub_ediv (x : Int) {m : Int} (hm : 0 < m) : -(x / m) = (m - 1 - x) / m

-⌊x / m⌋ = ⌊(m - 1 - x) / m⌋, the ceiling of -x / m, for m > 0.

theorem Int.ediv_add_emod_sub_add_sub_one_ediv (lo a0 : Int) {m : Int} (hm : 0 < m) : lo / m + (lo % m - a0 + (m - 1)) / m = -((a0 - lo) / m)

⌊lo / m⌋ + ⌈(lo mod m - a₀) / m⌉ = ⌈(lo - a₀) / m⌉ for m > 0: the first bit of the split form of numerators_to_bits (Ratpoints.Sieve.numeratorsToBits), from the multiple of m in lo and its rest.

theorem Int.ediv_add_emod_sub_ediv (hi a0 : Int) {m : Int} (hm : 0 < m) : hi / m + (hi % m - a0) / m = (hi - a0) / m

⌊hi / m⌋ + ⌊(hi mod m - a₀) / m⌋ = ⌊(hi - a₀) / m⌋ for m > 0: the last bit of the split form of numerators_to_bits (Ratpoints.Sieve.numeratorsToBits).

theorem Int.lt_ediv_of_neg {c z m : Int} (hc : c < 0) (hz : c < z) (hm : 0 < m) : c < z / m

theorem Int.emod_eq_ite_of_lt_two_mul {a m : Int} (h0 : 0 ≤ a) (h1 : a < 2 * m) : a % m = if m ≤ a then a - m else a

A residue 0 ≤ a < 2 m modulo m by one conditional subtraction.

theorem Int.neg_le_mul_ediv_of_dvd {d N lo : Int} (hd : 0 < d) (hdN : d ∣ N) (hlo : -N ≤ lo) : -N ≤ d * (lo / d)

The multiple d ⌊lo / d⌋ of d > 0 at or below lo is at least every multiple -N ≤ lo of d.

theorem Int.mul_ediv_add_one_le_of_dvd {d N hi : Int} (hd : 0 < d) (hdN : d ∣ N) (hhi : hi < N) : d * (hi / d + 1) ≤ N

The multiple d (⌊hi / d⌋ + 1) of d > 0 above hi is at most every multiple N > hi of d.

theorem Int.pow_mul_pow_sub (a : Int) {m n : Nat} (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n

Mathlib's pow_mul_pow_sub for integers, for the files without Mathlib.

Exceptions

theorem Except.bind_eq_ok {ε α β : Type u} {m : Except ε α} {f : α → Except ε β} {b : β} (h : m >>= f = ok b) : ∃ (a : α), m = ok a ∧ f a = ok b

A bind that succeeds succeeds at its first step.

Strings

theorem String.intercalate_cons_eq_append_join (s t : String) (l : List String) : s.intercalate (t :: l) = t ++ join (List.map (fun (x : String) => s ++ x) l)

The strings t :: l joined by the separator s are t followed by each string of l after s.