data.fin

# The finite type with n elements #

fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

## Main definitions #

### Induction principles #

• fin_zero_elim : Elimination principle for the empty set fin 0, generalizes fin.elim0.
• fin.succ_rec : Define C n i by induction on i : fin n interpreted as (0 : fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.
• fin.succ_rec_on : same as fin.succ_rec but i : fin n is the first argument;
• fin.induction : Define C i by induction on i : fin (n + 1), separating into the nat-like base cases of C 0 and C (i.succ).
• fin.induction_on : same as fin.induction but with i : fin (n + 1) as the first argument.

### Casts #

• cast_lt i h : embed i into a fin where h proves it belongs into;
• cast_le h : embed fin n into fin m, h : n ≤ m;
• cast eq : embed fin n into fin m, eq : n = m;
• cast_add m : embed fin n into fin (n+m);
• cast_succ : embed fin n into fin (n+1);
• succ_above p : embed fin n into fin (n + 1) with a hole around p;
• pred_above (p : fin n) i : embed i : fin (n+1) into fin n by subtracting one if p < i;
• cast_pred : embed fin (n + 2) into fin (n + 1) by mapping last (n + 1) to last n;
• sub_nat i h : subtract m from i ≥ m, generalizes fin.pred;
• add_nat m i : add m on i on the right, generalizes fin.succ;
• nat_add n i adds n on i on the left;
• clamp n m : min n m as an element of fin (m + 1);

### Operation on tuples #

We interpret maps Π i : fin n, α i as tuples (α 0, …, α (n-1)). If α i is a constant map, then tuples are isomorphic (but not definitionally equal) to vectors.

We define the following operations:

• tail : the tail of an n+1 tuple, i.e., its last n entries;
• cons : adding an element at the beginning of an n-tuple, to get an n+1-tuple;
• init : the beginning of an n+1 tuple, i.e., its first n entries;
• snoc : adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.
• insert_nth : insert an element to a tuple at a given position.
• find p : returns the first index n where p n is satisfied, and none if it is never satisfied.

### Misc definitions #

• fin.last n : The greatest value of fin (n+1).
def fin_zero_elim {α : fin 0Sort u} (x : fin 0) :
α x

Elimination principle for the empty set fin 0, dependent version.

Equations
@[instance]
theorem fact.succ.pos {n : } :
fact (0 < n.succ)
@[instance]
theorem fact.bit0.pos {n : } [h : fact (0 < n)] :
fact (0 < bit0 n)
@[instance]
theorem fact.bit1.pos {n : } :
fact (0 < bit1 n)
@[instance]
theorem fact.pow.pos {p n : } [h : fact (0 < p)] :
fact (0 < p ^ n)
@[protected, instance]
def fin.fin_to_nat (n : ) :
Equations

### coercions and constructions #

@[protected, simp]
theorem fin.eta {n : } (a : fin n) (h : a < n) :
a, h⟩ = a
@[ext]
theorem fin.ext {n : } {a b : fin n} (h : a = b) :
a = b
theorem fin.ext_iff {n : } (a b : fin n) :
a = b a = b
theorem fin.coe_injective {n : } :
theorem fin.eq_iff_veq {n : } (a b : fin n) :
a = b a.val = b.val
theorem fin.ne_iff_vne {n : } (a b : fin n) :
a b a.val b.val
@[simp]
theorem fin.mk_eq_subtype_mk {n : } (a : ) (h : a < n) :
h = a, h⟩
@[protected]
theorem fin.mk.inj_iff {n a b : } {ha : a < n} {hb : b < n} :
a, ha⟩ = b, hb⟩ a = b
theorem fin.mk_val {m n : } (h : m < n) :
m, h⟩.val = m
theorem fin.eq_mk_iff_coe_eq {n : } {a : fin n} {k : } {hk : k < n} :
a = k, hk⟩ a = k
@[simp, norm_cast]
theorem fin.coe_mk {m n : } (h : m < n) :
m, h⟩ = m
theorem fin.mk_coe {n : } (i : fin n) :
i, _⟩ = i
theorem fin.coe_eq_val {n : } (a : fin n) :
a = a.val
@[simp]
theorem fin.val_eq_coe {n : } (a : fin n) :
a.val = a
@[protected]
theorem fin.heq_fun_iff {α : Sort u_1} {k l : } (h : k = l) {f : fin k → α} {g : fin l → α} :
f == g ∀ (i : fin k), f i = g i, _⟩

Assume k = l. If two functions defined on fin k and fin l are equal on each element, then they coincide (in the heq sense).

@[protected]
theorem fin.heq_ext_iff {k l : } (h : k = l) {i : fin k} {j : fin l} :
i == j i = j
theorem fin.exists_iff {n : } {p : fin n → Prop} :
(∃ (i : fin n), p i) ∃ (i : ) (h : i < n), p i, h⟩
theorem fin.forall_iff {n : } {p : fin n → Prop} :
(∀ (i : fin n), p i) ∀ (i : ) (h : i < n), p i, h⟩

### order #

theorem fin.is_lt {n : } (i : fin n) :
i < n
theorem fin.is_le {n : } (i : fin (n + 1)) :
i n
theorem fin.lt_iff_coe_lt_coe {n : } {a b : fin n} :
a < b a < b
theorem fin.le_iff_coe_le_coe {n : } {a b : fin n} :
a b a b
theorem fin.mk_lt_of_lt_coe {n : } {b : fin n} {a : } (h : a < b) :
a, _⟩ < b
theorem fin.mk_le_of_le_coe {n : } {b : fin n} {a : } (h : a b) :
a, _⟩ b
@[simp, norm_cast]
theorem fin.coe_fin_lt {n : } {a b : fin n} :
a < b a < b

a < b as natural numbers if and only if a < b in fin n.

@[simp, norm_cast]
theorem fin.coe_fin_le {n : } {a b : fin n} :
a b a b

a ≤ b as natural numbers if and only if a ≤ b in fin n.

@[protected, instance]
Equations
def fin.coe_embedding (n : ) :

The inclusion map fin n → ℕ is a relation embedding.

Equations
@[protected, instance]

The ordering on fin n is a well order.

@[protected, instance]
def fin.has_well_founded {n : } :

Use the ordering on fin n for checking recursive definitions.

For example, the following definition is not accepted by the termination checker, unless we declare the has_well_founded instance:

def factorial {n : ℕ} : fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩

Equations
@[simp]
theorem fin.coe_zero {n : } :
0 = 0
@[simp]
theorem fin.val_zero' (n : ) :
0.val = 0
@[simp]
theorem fin.mk_zero {n : } :
0, _⟩ = 0
theorem fin.zero_le {n : } (a : fin (n + 1)) :
0 a
theorem fin.pos_iff_ne_zero {n : } (a : fin (n + 1)) :
0 < a a 0
def fin.last (n : ) :
fin (n + 1)

The greatest value of fin (n+1)

Equations
@[simp, norm_cast]
theorem fin.coe_last (n : ) :
theorem fin.last_val (n : ) :
(fin.last n).val = n
theorem fin.le_last {n : } (i : fin (n + 1)) :
i
@[protected, instance]
Equations
theorem fin.last_pos {n : } :
0 < fin.last (n + 1)
theorem fin.eq_last_of_not_lt {n : } {i : fin (n + 1)} (h : ¬i < n) :
i =
@[simp]
theorem fin.coe_order_iso_apply {n m : } (e : fin n ≃o fin m) (i : fin n) :
(e i) = i

If e is an order_iso between fin n and fin m, then n = m and e is the identity map. In this lemma we state that for each i : fin n we have (e i : ℕ) = (i : ℕ).

@[protected, instance]
def fin.order_iso_subsingleton {n : } {α : Type u_1} [preorder α] :
@[protected, instance]
def fin.order_iso_subsingleton' {n : } {α : Type u_1} [preorder α] :
@[protected, instance]
def fin.order_iso_unique {n : } :
Equations
theorem fin.strict_mono_unique {n : } {α : Type u_1} [preorder α] {f g : fin n → α} (hf : strict_mono f) (hg : strict_mono g) (h : = ) :
f = g

Two strictly monotone functions from fin n are equal provided that their ranges are equal.

theorem fin.order_embedding_eq {n : } {α : Type u_1} [preorder α] {f g : fin n ↪o α} (h : = ) :
f = g

Two order embeddings of fin n are equal provided that their ranges are equal.

theorem fin.strict_mono_iff_lt_succ {n : } {α : Type u_1} [preorder α] {f : fin n → α} :
∀ (i : ) (h : i + 1 < n), f i, _⟩ < f i + 1, h⟩

A function f on fin n is strictly monotone if and only if f i < f (i+1) for all i.

### addition, numerals, and coercion from nat #

def fin.of_nat' {n : } [h : fact (0 < n)] (i : ) :
fin n

convert a ℕ to fin n, provided n is positive

Equations
theorem fin.one_val {n : } :
1.val = 1 % (n + 1)
theorem fin.coe_one' {n : } :
1 = 1 % (n + 1)
@[simp]
theorem fin.val_one {n : } :
1.val = 1
@[simp]
theorem fin.coe_one {n : } :
1 = 1
@[simp]
theorem fin.mk_one {n : } :
1, _⟩ = 1
@[protected, instance]
def fin.nontrivial {n : } :
nontrivial (fin (n + 2))
@[protected, simp]
theorem fin.add_zero {n : } (k : fin (n + 1)) :
k + 0 = k
@[protected, simp]
theorem fin.zero_add {n : } (k : fin (n + 1)) :
0 + k = k
@[protected, instance]
Equations
theorem fin.val_add {n : } (a b : fin n) :
(a + b).val = (a.val + b.val) % n
theorem fin.coe_add {n : } (a b : fin n) :
(a + b) = (a + b) % n
theorem fin.coe_bit0 {n : } (k : fin n) :
(bit0 k) = % n
theorem fin.coe_bit1 {n : } (k : fin (n + 1)) :
(bit1 k) = % (n + 1)
theorem fin.coe_add_one_of_lt {n : } {i : fin n.succ} (h : i < ) :
(i + 1) = i + 1
@[simp]
theorem fin.last_add_one (n : ) :
+ 1 = 0
theorem fin.coe_add_one {n : } (i : fin (n + 1)) :
(i + 1) = ite (i = fin.last n) 0 (i + 1)
@[simp]
theorem fin.mk_bit0 {m n : } (h : bit0 m < n) :
bit0 m, h⟩ = bit0 m, _⟩
@[simp]
theorem fin.mk_bit1 {m n : } (h : bit1 m < n + 1) :
bit1 m, h⟩ = bit1 m, _⟩
@[simp]
theorem fin.val_two {n : } :
2.val = 2
@[simp]
theorem fin.coe_two {n : } :
2 = 2
@[simp]
theorem fin.of_nat_eq_coe (n a : ) :
= a
theorem fin.coe_val_of_lt {n a : } (h : a < n + 1) :
a.val = a

Converting an in-range number to fin (n + 1) produces a result whose value is the original number.

theorem fin.coe_val_eq_self {n : } (a : fin (n + 1)) :
(a.val) = a

Converting the value of a fin (n + 1) to fin (n + 1) results in the same value.

theorem fin.coe_coe_of_lt {n a : } (h : a < n + 1) :

Coercing an in-range number to fin (n + 1), and converting back to ℕ, results in that number.

@[simp]
theorem fin.coe_coe_eq_self {n : } (a : fin (n + 1)) :

Converting a fin (n + 1) to ℕ and back results in the same value.

theorem fin.coe_nat_eq_last (n : ) :
n =
theorem fin.le_coe_last {n : } (i : fin (n + 1)) :
i n
theorem fin.add_one_pos {n : } (i : fin (n + 1)) (h : i < ) :
0 < i + 1
theorem fin.one_pos {n : } :
0 < 1
theorem fin.zero_ne_one {n : } :
0 1
@[simp]
theorem fin.zero_eq_one_iff {n : } :
0 = 1 n = 0
@[simp]
theorem fin.one_eq_zero_iff {n : } :
1 = 0 n = 0

### succ and casts into larger fin types #

@[simp]
theorem fin.coe_succ {n : } (j : fin n) :
(j.succ) = j + 1
theorem fin.succ_pos {n : } (a : fin n) :
0 < a.succ
def fin.succ_embedding (n : ) :
fin n ↪o fin (n + 1)

fin.succ as an order_embedding

Equations
@[simp]
theorem fin.coe_succ_embedding {n : } :
@[simp]
theorem fin.succ_le_succ_iff {n : } {a b : fin n} :
a.succ b.succ a b
@[simp]
theorem fin.succ_lt_succ_iff {n : } {a b : fin n} :
a.succ < b.succ a < b
theorem fin.succ_injective (n : ) :
@[simp]
theorem fin.succ_inj {n : } {a b : fin n} :
a.succ = b.succ a = b
theorem fin.succ_ne_zero {n : } (k : fin n) :
k.succ 0
@[simp]
theorem fin.succ_zero_eq_one {n : } :
0.succ = 1
@[simp]
theorem fin.succ_one_eq_two {n : } :
1.succ = 2
@[simp]
theorem fin.succ_mk (n i : ) (h : i < n) :
fin.succ i, h⟩ = i + 1, _⟩
theorem fin.mk_succ_pos {n : } (i : ) (h : i < n) :
0 < i.succ, _⟩
theorem fin.one_lt_succ_succ {n : } (a : fin n) :
1 < a.succ.succ
theorem fin.succ_succ_ne_one {n : } (a : fin n) :
def fin.cast_lt {n m : } (i : fin m) (h : i.val < n) :
fin n

cast_lt i h embeds i into a fin where h proves it belongs into.

Equations
@[simp]
theorem fin.coe_cast_lt {n m : } (i : fin m) (h : i.val < n) :
@[simp]
theorem fin.cast_lt_mk (i n m : ) (hn : i < n) (hm : i < m) :
fin.cast_lt i, hn⟩ hm = i, hm⟩
def fin.cast_le {n m : } (h : n m) :

cast_le h i embeds i into a larger fin type.

Equations
@[simp]
theorem fin.coe_cast_le {n m : } (h : n m) (i : fin n) :
@[simp]
theorem fin.cast_le_mk (i n m : ) (hn : i < n) (h : n m) :
(fin.cast_le h) i, hn⟩ = i, _⟩
@[simp]
theorem fin.cast_le_zero {n m : } (h : n.succ m.succ) :
@[simp]
theorem fin.range_cast_le {n k : } (h : n k) :
= {i : fin k | i < n}
@[simp]
theorem fin.coe_of_injective_cast_le_symm {n k : } (h : n k) (i : fin k) (hi : i ) :
( _).symm) i, hi⟩) = i
def fin.cast {n m : } (eq : n = m) :

cast eq i embeds i into a equal fin type.

Equations
@[simp]
theorem fin.symm_cast {n m : } (h : n = m) :
theorem fin.coe_cast {n m : } (h : n = m) (i : fin n) :
@[simp]
theorem fin.cast_mk {n m : } (h : n = m) (i : ) (hn : i < n) :
(fin.cast h) i, hn⟩ = i, _⟩
@[simp]
theorem fin.cast_trans {n m k : } (h : n = m) (h' : m = k) {i : fin n} :
@[simp]
theorem fin.cast_refl {n : } (h : n = n := rfl) :
=
theorem fin.cast_to_equiv {n m : } (h : n = m) :

While in many cases fin.cast is better than equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

theorem fin.cast_eq_cast {n m : } (h : n = m) :

While in many cases fin.cast is better than equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

def fin.cast_add {n : } (m : ) :
fin n ↪o fin (n + m)

cast_add m i embeds i : fin n in fin (n+m).

Equations
@[simp]
theorem fin.coe_cast_add {n : } (m : ) (i : fin n) :
@[simp]
theorem fin.cast_add_mk {n : } (m i : ) (h : i < n) :
(fin.cast_add m) i, h⟩ = i, _⟩
def fin.cast_succ {n : } :
fin n ↪o fin (n + 1)

cast_succ i embeds i : fin n in fin (n+1).

Equations
@[simp]
theorem fin.coe_cast_succ {n : } (i : fin n) :
@[simp]
theorem fin.cast_succ_mk (n i : ) (h : i < n) :
fin.cast_succ i, h⟩ = i, _⟩
theorem fin.cast_succ_lt_succ {n : } (i : fin n) :
theorem fin.le_cast_succ_iff {n : } {i : fin (n + 1)} {j : fin n} :
i < j.succ
@[simp]
theorem fin.succ_last (n : ) :
@[simp]
theorem fin.succ_eq_last_succ {n : } (i : fin n.succ) :
i.succ = fin.last (n + 1) i =
@[simp]
theorem fin.cast_succ_cast_lt {n : } (i : fin (n + 1)) (h : i < n) :
@[simp]
theorem fin.cast_lt_cast_succ {n : } (a : fin n) (h : a < n) :
h = a
@[simp]
theorem fin.cast_succ_lt_cast_succ_iff {n : } {a b : fin n} :
a < b
theorem fin.cast_succ_inj {n : } {a b : fin n} :
a = b
theorem fin.cast_succ_lt_last {n : } (a : fin n) :
@[simp]
theorem fin.cast_succ_zero {n : } :
@[simp]
theorem fin.cast_succ_one {n : } :
theorem fin.cast_succ_pos {n : } {i : fin (n + 1)} (h : 0 < i) :

cast_succ i is positive when i is positive

theorem fin.cast_succ_fin_succ (n : ) (j : fin n) :
@[simp, norm_cast]
theorem fin.coe_eq_cast_succ {n : } {a : fin n} :
@[simp]
theorem fin.coe_succ_eq_succ {n : } {a : fin n} :
= a.succ
theorem fin.lt_succ {n : } {a : fin n} :
@[simp]
theorem fin.range_cast_succ {n : } :
= {i : fin (n + 1) | i < n}
@[simp]
theorem fin.coe_of_injective_cast_succ_symm {n : } (i : fin n.succ) (hi : i ) :
i, hi⟩) = i
def fin.add_nat {n : } (m : ) :
fin n ↪o fin (n + m)

add_nat m i adds m to i, generalizes fin.succ.

Equations
@[simp]
theorem fin.coe_add_nat {n : } (m : ) (i : fin n) :
def fin.nat_add (n : ) {m : } :
fin m ↪o fin (n + m)

nat_add n i adds n to i "on the left".

Equations
@[simp]
theorem fin.coe_nat_add (n : ) {m : } (i : fin m) :
theorem fin.nat_add_zero {n : } :

### recursion and induction principles #

def fin.succ_rec {C : Π (n : ), fin nSort u_1} (H0 : Π (n : ), C n.succ 0) (Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ) {n : } (i : fin n) :
C n i

Define C n i by induction on i : fin n interpreted as (0 : fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

Equations
def fin.succ_rec_on {n : } (i : fin n) {C : Π (n : ), fin nSort u_1} (H0 : Π (n : ), C n.succ 0) (Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ) :
C n i

Define C n i by induction on i : fin n interpreted as (0 : fin (n - i)).succ.succ…. This function has two arguments: H0 n defines 0-th element C (n+1) 0 of an (n+1)-tuple, and Hs n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

A version of fin.succ_rec taking i : fin n as the first argument.

Equations
@[simp]
theorem fin.succ_rec_on_zero {C : Π (n : ), fin nSort u_1} {H0 : Π (n : ), C n.succ 0} {Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ} (n : ) :
0.succ_rec_on H0 Hs = H0 n
@[simp]
theorem fin.succ_rec_on_succ {C : Π (n : ), fin nSort u_1} {H0 : Π (n : ), C n.succ 0} {Hs : Π (n : ) (i : fin n), C n iC n.succ i.succ} {n : } (i : fin n) :
i.succ.succ_rec_on H0 Hs = Hs n i (i.succ_rec_on H0 Hs)
def fin.induction {n : } {C : fin (n + 1)Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C C i.succ) (i : fin (n + 1)) :
C i

Define C i by induction on i : fin (n + 1) via induction on the underlying nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.cast_succ.

Equations
• hs = λ (i : fin (n + 1)), subtype.cases_on i (λ (i : ) (hi : i < n + 1), nat.rec (λ (hi : 0 < n + 1), _.mpr h0) (λ (i : ) (IH : Π (hi : i < n + 1), C i, hi⟩) (hi : i.succ < n + 1), hs i, _⟩ (IH _)) i hi)
def fin.induction_on {n : } (i : fin (n + 1)) {C : fin (n + 1)Sort u_1} (h0 : C 0) (hs : Π (i : fin n), C C i.succ) :
C i

Define C i by induction on i : fin (n + 1) via induction on the underlying nat value. This function has two arguments: h0 handles the base case on C 0, and hs defines the inductive step using C i.cast_succ.

A version of fin.induction taking i : fin (n + 1) as the first argument.

Equations
def fin.cases {n : } {C : fin n.succSort u_1} (H0 : C 0) (Hs : Π (i : fin n), C i.succ) (i : fin n.succ) :
C i

Define f : Π i : fin n.succ, C i by separately handling the cases i = 0 and i = j.succ, j : fin n.

Equations
@[simp]
theorem fin.cases_zero {n : } {C : fin n.succSort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} :
Hs 0 = H0
@[simp]
theorem fin.cases_succ {n : } {C : fin n.succSort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} (i : fin n) :
Hs i.succ = Hs i
@[simp]
theorem fin.cases_succ' {n : } {C : fin n.succSort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} {i : } (h : i + 1 < n + 1) :
Hs i.succ, h⟩ = Hs i, _⟩
theorem fin.forall_fin_succ {n : } {P : fin (n + 1) → Prop} :
(∀ (i : fin (n + 1)), P i) P 0 ∀ (i : fin n), P i.succ
theorem fin.exists_fin_succ {n : } {P : fin (n + 1) → Prop} :
(∃ (i : fin (n + 1)), P i) P 0 ∃ (i : fin n), P i.succ

### pred #

@[simp]
theorem fin.coe_pred {n : } (j : fin (n + 1)) (h : j 0) :
(j.pred h) = j - 1
@[simp]
theorem fin.succ_pred {n : } (i : fin (n + 1)) (h : i 0) :
(i.pred h).succ = i
@[simp]
theorem fin.pred_succ {n : } (i : fin n) {h : i.succ 0} :
i.succ.pred h = i
@[simp]
theorem fin.pred_mk_succ {n : } (i : ) (h : i < n + 1) :
fin.pred i + 1, _⟩ _ = i, h⟩
theorem fin.pred_mk {n : } (i : ) (h : i < n + 1) (w : i, h⟩ 0) :
fin.pred i, h⟩ w = i - 1, _⟩
@[simp]
theorem fin.pred_le_pred_iff {n : } {a b : fin n.succ} {ha : a 0} {hb : b 0} :
a.pred ha b.pred hb a b
@[simp]
theorem fin.pred_lt_pred_iff {n : } {a b : fin n.succ} {ha : a 0} {hb : b 0} :
a.pred ha < b.pred hb a < b
@[simp]
theorem fin.pred_inj {n : } {a b : fin (n + 1)} {ha : a 0} {hb : b 0} :
a.pred ha = b.pred hb a = b
@[simp]
theorem fin.pred_one {n : } :
1.pred _ = 0
theorem fin.pred_add_one {n : } (i : fin (n + 2)) (h : i < n + 1) :
(i + 1).pred _ = i.cast_lt h
def fin.sub_nat {n : } (m : ) (i : fin (n + m)) (h : m i) :
fin n

sub_nat i h subtracts m from i, generalizes fin.pred.

Equations
@[simp]
theorem fin.coe_sub_nat {n m : } (i : fin (n + m)) (h : m i) :
i h) = i - m
@[simp]
theorem fin.pred_cast_succ_succ {n : } (i : fin n) :
.pred _ =
@[protected, instance]
def fin.has_neg (n : ) :

Negation on fin n

Equations
@[protected, instance]
def fin.add_comm_group (n : ) :

Abelian group structure on fin (n+1).

Equations
@[protected]
theorem fin.coe_neg {n : } (a : fin n) :
-a = (n - a) % n
@[protected]
theorem fin.coe_sub {n : } (a b : fin n) :
(a - b) = (a + (n - b)) % n
theorem fin.succ_above_aux {n : } (p : fin (n + 1)) :
strict_mono (λ (i : fin n), ite < p) i.succ)
def fin.succ_above {n : } (p : fin (n + 1)) :
fin n ↪o fin (n + 1)

succ_above p i embeds fin n into fin (n + 1) with a hole around p.

Equations
theorem fin.succ_above_below {n : } (p : fin (n + 1)) (i : fin n) (h : < p) :

Embedding i : fin n into fin (n + 1) with a hole around p : fin (n + 1) embeds i by cast_succ when the resulting i.cast_succ < p.

@[simp]
theorem fin.succ_above_zero {n : } :

Embedding fin n into fin (n + 1) with a hole around zero embeds by succ.

@[simp]
theorem fin.succ_above_last {n : } :

Embedding fin n into fin (n + 1) with a hole around last n embeds by cast_succ.

theorem fin.succ_above_last_apply {n : } (i : fin n) :
theorem fin.succ_above_above {n : } (p : fin (n + 1)) (i : fin n) (h : p ) :

Embedding i : fin n into fin (n + 1) with a hole around p : fin (n + 1) embeds i by succ when the resulting p < i.succ.

theorem fin.succ_above_lt_ge {n : } (p : fin (n + 1)) (i : fin n) :

Embedding i : fin n into fin (n + 1) is always about some hole p.

theorem fin.succ_above_lt_gt {n : } (p : fin (n + 1)) (i : fin n) :
p < i.succ

Embedding i : fin n into fin (n + 1) is always about some hole p.

@[simp]
theorem fin.succ_above_lt_iff {n : } (p : fin (n + 1)) (i : fin n) :

Embedding i : fin n into fin (n + 1) using a pivot p that is greater results in a value that is less than p.

theorem fin.lt_succ_above_iff {n : } (p : fin (n + 1)) (i : fin n) :

Embedding i : fin n into fin (n + 1) using a pivot p that is lesser results in a value that is greater than p.

theorem fin.succ_above_ne {n : } (p : fin (n + 1)) (i : fin n) :

Embedding i : fin n into fin (n + 1) with a hole around p : fin (n + 1) never results in p itself

theorem fin.succ_above_pos {n : } (p : fin (n + 2)) (i : fin (n + 1)) (h : 0 < i) :

Embedding a positive fin n results in a positive fin (n + 1)

theorem fin.range_succ_above {n : } (p : fin (n + 1)) :
= {i : fin (n + 1) | i p}

The range of p.succ_above is everything except p.

theorem fin.succ_above_right_injective {n : } {x : fin (n + 1)} :

Given a fixed pivot x : fin (n + 1), x.succ_above is injective

theorem fin.succ_above_right_inj {n : } {a b : fin n} {x : fin (n + 1)} :

Given a fixed pivot x : fin (n + 1), x.succ_above is injective

succ_above is injective at the pivot

theorem fin.succ_above_left_inj {n : } {x y : fin (n + 1)} :
x = y

succ_above is injective at the pivot

@[simp]
theorem fin.zero_succ_above {n : } (i : fin n) :
@[simp]
theorem fin.succ_succ_above_zero {n : } (i : fin (n + 1)) :
@[simp]
theorem fin.succ_succ_above_succ {n : } (i : fin (n + 1)) (j : fin n) :
@[simp]
theorem fin.one_succ_above_zero {n : } :
@[simp]
theorem fin.succ_succ_above_one {n : } (i : fin (n + 2)) :

By moving succ to the outside of this expression, we create opportunities for further simplification using succ_above_zero or succ_succ_above_zero.

@[simp]
theorem fin.one_succ_above_succ {n : } (j : fin n) :
@[simp]
theorem fin.one_succ_above_one {n : } :
def fin.pred_above {n : } (p : fin n) (i : fin (n + 1)) :
fin n

pred_above p i embeds i : fin (n+1) into fin n by subtracting one if p < i.

Equations
theorem fin.pred_above_right_monotone {n : } (p : fin n) :
theorem fin.pred_above_left_monotone {n : } (i : fin (n + 1)) :
monotone (λ (p : fin n), p.pred_above i)
def fin.cast_pred {n : } (i : fin (n + 2)) :
fin (n + 1)

cast_pred embeds i : fin (n + 2) into fin (n + 1) by lowering just last (n + 1) to last n.

Equations
@[simp]
theorem fin.cast_pred_zero {n : } :
@[simp]
theorem fin.cast_pred_one {n : } :
@[simp]
theorem fin.pred_above_zero {n : } {i : fin (n + 2)} (hi : i 0) :
0.pred_above i = i.pred hi
@[simp]
theorem fin.cast_pred_last {n : } :
@[simp]
theorem fin.cast_pred_mk (n i : ) (h : i < n + 1) :
fin.cast_pred i, _⟩ = i, h⟩
theorem fin.pred_above_below {n : } (p : fin (n + 1)) (i : fin (n + 2)) (h : i ) :
@[simp]
theorem fin.pred_above_last {n : } :
theorem fin.pred_above_above {n : } (p : fin n) (i : fin (n + 1)) (h : < i) :
p.pred_above i = i.pred _
theorem fin.cast_pred_monotone {n : } :
@[simp]
theorem fin.succ_above_pred_above {n : } {p : fin n} {i : fin (n + 1)} (h : i ) :

Sending fin (n+1) to fin n by subtracting one from anything above p then back to fin (n+1) with a gap around p is the identity away from p.

@[simp]
theorem fin.pred_above_succ_above {n : } (p i : fin n) :

Sending fin n into fin (n + 1) with a gap at p then back to fin n by subtracting one from anything above p is the identity.

@[simp]
theorem fin.cast_pred_cast_succ {n : } (i : fin (n + 1)) :
= i
theorem fin.cast_succ_cast_pred {n : } {i : fin (n + 2)} (h : i < fin.last (n + 1)) :
theorem fin.coe_cast_pred_le_self {n : } (i : fin (n + 2)) :
theorem fin.coe_cast_pred_lt_iff {n : } {i : fin (n + 2)} :
theorem fin.lt_last_iff_coe_cast_pred {n : } {i : fin (n + 2)} :
theorem fin.forall_iff_succ_above {n : } {p : fin (n + 1) → Prop} (i : fin (n + 1)) :
(∀ (j : fin (n + 1)), p j) p i ∀ (j : fin n), p ((i.succ_above) j)
def fin.clamp (n m : ) :
fin (m + 1)

min n m as an element of fin (m + 1)

Equations
@[simp]
theorem fin.coe_clamp (n m : ) :
m) = min n m

### Tuples #

We can think of the type Π(i : fin n), α i as n-tuples of elements of possibly varying type α i. A particular case is fin n → α of elements with all the same type. Here are some relevant operations, first about adding or removing elements at the beginning of a tuple.

@[protected, instance]
def fin.tuple0_unique (α : fin 0Sort u) :
unique (Π (i : fin 0), α i)

There is exactly one tuple of size zero.

Equations
@[simp]
theorem fin.tuple0_le {α : fin 0Type u_1} [Π (i : fin 0), preorder (α i)] (f g : Π (i : fin 0), α i) :
f g
def fin.tail {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) :
α i.succ

The tail of an n+1 tuple, i.e., its last n entries.

Equations
theorem fin.tail_def {n : } {α : fin (n + 1)Type u_1} {q : Π (i : fin (n + 1)), α i} :
fin.tail (λ (k : fin (n + 1)), q k) = λ (k : fin n), q k.succ
def fin.cons {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin (n + 1)) :
α i

Adding an element at the beginning of an n-tuple, to get an n+1-tuple.

Equations
• p = λ (j : fin (n + 1)), p j
@[simp]
theorem fin.tail_cons {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) :
@[simp]
theorem fin.cons_succ {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin n) :
p i.succ = p i
@[simp]
theorem fin.cons_zero {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) :
p 0 = x
@[simp]
theorem fin.cons_update {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (i : fin n) (y : α i.succ) :
i y) = function.update (fin.cons x p) i.succ y

Updating a tuple and adding an element at the beginning commute.

theorem fin.update_cons_zero {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (i : fin n), α i.succ) (z : α 0) :

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

@[simp]
theorem fin.cons_self_tail {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) :
fin.cons (q 0) (fin.tail q) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

@[simp]
theorem fin.tail_update_zero {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (z : α 0) :
fin.tail 0 z) =

Updating the first element of a tuple does not change the tail.

@[simp]
theorem fin.tail_update_succ {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α i.succ) :
fin.tail i.succ y) = i y

Updating a nonzero element and taking the tail commute.

theorem fin.comp_cons {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (y : α) (q : fin n → α) :
g q = fin.cons (g y) (g q)
theorem fin.comp_tail {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :
g = fin.tail (g q)
theorem fin.le_cons {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {x : α 0} {q : Π (i : fin (n + 1)), α i} {p : Π (i : fin n), α i.succ} :
q p q 0 x p
theorem fin.cons_le {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {x : α 0} {q : Π (i : fin (n + 1)), α i} {p : Π (i : fin n), α i.succ} :
p q x q 0 p
@[simp]
theorem fin.range_cons {α : Type u_1} {n : } (x : α) (b : fin n → α) :
def fin.append {n m : } {α : Type u_1} {o : } (ho : o = m + n) (u : fin m → α) (v : fin n → α) :
fin o → α

fin.append ho u v appends two vectors of lengths m and n to produce one of length o = m + n. ho provides control of definitional equality for the vector length.

Equations
@[simp]
theorem fin.fin_append_apply_zero {n m : } {α : Type u_1} {o : } (ho : o + 1 = m + 1 + n) (u : fin (m + 1) → α) (v : fin n → α) :
u v 0 = u 0

In the previous section, we have discussed inserting or removing elements on the left of a tuple. In this section, we do the same on the right. A difference is that fin (n+1) is constructed inductively from fin n starting from the left, not from the right. This implies that Lean needs more help to realize that elements belong to the right types, i.e., we need to insert casts at several places.

def fin.init {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) :
α

The beginning of an n+1 tuple, i.e., its first n entries

Equations
• i = q
theorem fin.init_def {n : } {α : fin (n + 1)Type u_1} {q : Π (i : fin (n + 1)), α i} :
fin.init (λ (k : fin (n + 1)), q k) = λ (k : fin n), q
def fin.snoc {n : } {α : fin (n + 1)Type u} (p : Π (i : fin n), α ) (x : α (fin.last n)) (i : fin (n + 1)) :
α i

Adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.

Equations
@[simp]
theorem fin.init_snoc {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α ) :
@[simp]
theorem fin.snoc_cast_succ {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α ) (i : fin n) :
x = p i
@[simp]
theorem fin.snoc_last {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α ) :
x (fin.last n) = x
@[simp]
theorem fin.snoc_update {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α ) (i : fin n) (y : α ) :

Updating a tuple and adding an element at the end commute.

theorem fin.update_snoc_last {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (i : fin n), α ) (z : α (fin.last n)) :

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

@[simp]
theorem fin.snoc_init_self {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) :
fin.snoc (fin.init q) (q (fin.last n)) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

@[simp]
theorem fin.init_update_last {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (z : α (fin.last n)) :

Updating the last element of a tuple does not change the beginning.

@[simp]
theorem fin.init_update_cast_succ {n : } {α : fin (n + 1)Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α ) :
fin.init y) = i y

Updating an element and taking the beginning commute.

theorem fin.tail_init_eq_init_tail {n : } {β : Type u_1} (q : fin (n + 2) → β) :

tail and init commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

theorem fin.cons_snoc_eq_snoc_cons {n : } {β : Type u_1} (a : β) (q : fin n → β) (b : β) :
(fin.snoc q b) = fin.snoc (fin.cons a q) b

cons and snoc commute. We state this lemma in a non-dependent setting, as otherwise it would involve a cast to convince Lean that the two types are equal, making it harder to use.

theorem fin.comp_snoc {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n → α) (y : α) :
g y = fin.snoc (g q) (g y)
theorem fin.comp_init {n : } {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :
g = fin.init (g q)
def fin.insert_nth' {n : } {α : fin (n + 2)Type u} (i : fin (n + 2)) (x : α i) (p : Π (j : fin (n + 1)), α ((i.succ_above) j)) (j : fin (n + 2)) :
α j

Insert an element into a tuple at a given position, auxiliary definition. For the general definition, see insert_nth.

Equations
def fin.insert_nth {n : } {α : fin (n + 1)Type u} (i : fin (n + 1)) (x : α i) (p : Π (j : fin n), α ((i.succ_above) j)) (j : fin (n + 1)) :
α j

Insert an element into a tuple at a given position. For i = 0 see fin.cons, for i = fin.last n see fin.snoc.

Equations
@[simp]
theorem fin.insert_nth_apply_same {n : } {α : fin (n + 1)Type u} (i : fin (n + 1)) (x : α i) (p : Π (j : fin n), α ((i.succ_above) j)) :
i.insert_nth x p i = x
@[simp]
theorem fin.insert_nth_apply_succ_above {n : } {α : fin (n + 1)Type u} (i : fin (n + 1)) (x : α i) (p : Π (j : fin n), α ((i.succ_above) j)) (j : fin n) :
i.insert_nth x p ((i.succ_above) j) = p j
@[simp]
theorem fin.insert_nth_comp_succ_above {n : } {β : Type v} (i : fin (n + 1)) (x : β) (p : fin n → β) :
theorem fin.insert_nth_eq_iff {n : } {α : fin (n + 1)Type u} {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α ((i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
i.insert_nth x p = q q i = x p = λ (j : fin n), q ((i.succ_above) j)
theorem fin.eq_insert_nth_iff {n : } {α : fin (n + 1)Type u} {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α ((i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
q = i.insert_nth x p q i = x p = λ (j : fin n), q ((i.succ_above) j)
theorem fin.insert_nth_zero {n : } {α : fin (n + 1)Type u} (x : α 0) (p : Π (j : fin n), α ((0.succ_above) j)) :
0.insert_nth x p = (λ (j : fin n), cast _ (p j))
@[simp]
theorem fin.insert_nth_zero' {n : } {β : Type v} (x : β) (p : fin n → β) :
0.insert_nth x p = p
theorem fin.insert_nth_last {n : } {α : fin (n + 1)Type u} (x : α (fin.last n)) (p : Π (j : fin n), α (((fin.last n).succ_above) j)) :
(fin.last n).insert_nth x p = fin.snoc (λ (j : fin n), cast _ (p j)) x
@[simp]
theorem fin.insert_nth_last' {n : } {β : Type v} (x : β) (p : fin n → β) :
theorem fin.insert_nth_le_iff {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α ((i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
i.insert_nth x p q x q i p λ (j : fin n), q ((i.succ_above) j)
theorem fin.le_insert_nth_iff {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α ((i.succ_above) j)} {q : Π (j : fin (n + 1)), α j} :
q i.insert_nth x p q i x (λ (j : fin n), q ((i.succ_above) j)) p
theorem fin.insert_nth_mem_Icc {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {p : Π (j : fin n), α ((i.succ_above) j)} {q₁ q₂ : Π (j : fin (n + 1)), α j} :
i.insert_nth x p set.Icc q₁ q₂ x set.Icc (q₁ i) (q₂ i) p set.Icc (λ (j : fin n), q₁ ((i.succ_above) j)) (λ (j : fin n), q₂ ((i.succ_above) j))
theorem fin.preimage_insert_nth_Icc_of_mem {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {q₁ q₂ : Π (j : fin (n + 1)), α j} (hx : x set.Icc (q₁ i) (q₂ i)) :
i.insert_nth x ⁻¹' set.Icc q₁ q₂ = set.Icc (λ (j : fin n), q₁ ((i.succ_above) j)) (λ (j : fin n), q₂ ((i.succ_above) j))
theorem fin.preimage_insert_nth_Icc_of_not_mem {n : } {α : fin (n + 1)Type u} [Π (i : fin (n + 1)), preorder (α i)] {i : fin (n + 1)} {x : α i} {q₁ q₂ : Π (j : fin (n + 1)), α j} (hx : x set.Icc (q₁ i) (q₂ i)) :
i.insert_nth x ⁻¹' set.Icc q₁ q₂ =
def fin.find {n : } (p : fin n → Prop)  :

find p returns the first index n where p n is satisfied, and none if it is never satisfied.

Equations
theorem fin.find_spec {n : } (p : fin n → Prop) {i : fin n} (hi : i ) :
p i

If find p = some i, then p i holds

theorem fin.is_some_find_iff {n : } {p : fin n → Prop}  :
((fin.find p).is_some) ∃ (i : fin n), p i

find p does not return none if and only if p i holds at some index i.

theorem fin.find_eq_none_iff {n : } {p : fin n → Prop}  :
∀ (i : fin n), ¬p i

find p returns none if and only if p i never holds.

theorem fin.find_min {n : } {p : fin n → Prop} {i : fin n} (hi : i ) {j : fin n} (hj : j < i) :
¬p j

If find p returns some i, then p j does not hold for j < i, i.e., i is minimal among the indices where p` holds.

theorem fin.find_min' {n : } {p : fin n → Prop} {i : fin n} (h : i ) {j : fin n} (hj : p j) :
i j
theorem fin.nat_find_mem_find {n : } {p : fin n → Prop} (h : ∃ (i : ) (hin : i < n), p i, hin⟩) :
, _⟩
theorem fin.mem_find_iff {n : } {p : fin n → Prop} {i : fin n} :
i p i ∀ (j : fin n), p ji j
theorem fin.find_eq_some_iff {n : } {p : fin n → Prop} {i : fin n} :
= some i p i ∀ (j : fin n), p ji j
theorem fin.mem_find_of_unique {n : } {p : fin n → Prop} (h : ∀ (i j : fin n), p ip ji = j) {i : fin n} (hi : p i) :
i
@[simp]
theorem fin.coe_of_nat_eq_mod (m n : ) :
n = n % m.succ
@[simp]
theorem fin.coe_of_nat_eq_mod' (m n : ) [I : fact (0 < m)] :

### mul #

theorem fin.val_mul {n : } (a b : fin n) :
(a * b).val = (a.val) * b.val % n
theorem fin.coe_mul {n : } (a b : fin n) :
a * b = (a) * b % n
@[protected, simp]
theorem fin.mul_one {n : } (k : fin (n + 1)) :
k * 1 = k
@[protected, simp]
theorem fin.one_mul {n : } (k : fin (n + 1)) :
1 * k = k
@[protected, simp]
theorem fin.mul_zero {n : } (k : fin (n + 1)) :
k * 0 = 0
@[protected, simp]
theorem fin.zero_mul {n : } (k : fin (n + 1)) :
0 * k = 0