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;

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 i h : embed i : fin (n+1) into fin n by ignoring p;
sub_nat i h : subtract m from i ≥ m, generalizes fin.pred;
add_nat i h : add m on i on the right, generalizes fin.succ;
nat_add i h 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.
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).

source

def fin_zero_elim {α : fin 0 → Sort u} (x : fin 0) :

α x

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

Equations

fin_zero_elim x = x.elim0

source

theorem fact.succ.pos {n : ℕ} :

fact (0 < n.succ)

source

theorem fact.bit0.pos {n : ℕ} [h : fact (0 < n)] :

fact (0 < bit0 n)

source

theorem fact.bit1.pos {n : ℕ} :

fact (0 < bit1 n)

source

theorem fact.pow.pos {p n : ℕ} [h : fact (0 < p)] :

fact (0 < p ^ n)

source

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

ℕ → fin n

convert a ℕ to fin n, provided n is positive

Equations

fin.of_nat' i = ⟨i % n, _⟩

source

@[simp]

theorem fin.eta {n : ℕ} (a : fin n) (h : a.val < n) :

⟨a.val, h⟩ = a

source

theorem fin.ext_iff {n : ℕ} (a b : fin n) :

a = b ↔ a.val = b.val

source

theorem fin.val_injective {n : ℕ} :

function.injective fin.val

source

theorem fin.eq_iff_veq {n : ℕ} (a b : fin n) :

a = b ↔ a.val = b.val

source

@[simp]

theorem fin.mk.inj_iff {n a b : ℕ} {ha : a < n} {hb : b < n} :

⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b

source

@[instance]

def fin.fin_to_nat (n : ℕ) :

has_coe (fin n) ℕ

Equations

fin.fin_to_nat n = {coe := fin.val n}

source

theorem fin.mk_val {m n : ℕ} (h : m < n) :

⟨m, h⟩.val = m

source

@[simp]

theorem fin.coe_mk {m n : ℕ} (h : m < n) :

↑⟨m, h⟩ = m

source

theorem fin.coe_eq_val {n : ℕ} (a : fin n) :

↑a = a.val

source

@[simp]

theorem fin.val_one {n : ℕ} :

1.val = 1

source

@[simp]

theorem fin.val_two {n : ℕ} :

2.val = 2

source

@[simp]

theorem fin.coe_zero {n : ℕ} :

↑0 = 0

source

@[simp]

theorem fin.coe_one {n : ℕ} :

↑1 = 1

source

@[simp]

theorem fin.coe_two {n : ℕ} :

↑2 = 2

source

@[simp]

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.

source

@[simp]

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.

source

theorem fin.val_add {n : ℕ} (a b : fin n) :

(a + b).val = (a.val + b.val) % n

source

theorem fin.val_mul {n : ℕ} (a b : fin n) :

(a * b).val = a.val * b.val % n

source

theorem fin.one_val {n : ℕ} :

1.val = 1 % (n + 1)

source

@[simp]

theorem fin.zero_val (n : ℕ) :

0.val = 0

source

@[simp]

theorem fin.of_nat_eq_coe (n a : ℕ) :

fin.of_nat a = ↑a

source

theorem fin.coe_val_of_lt {n a : ℕ} :

a < n + 1 → ↑a.val = a

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

source

@[simp]

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.

source

theorem fin.coe_coe_of_lt {n a : ℕ} :

a < n + 1 → ↑↑a = a

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

source

@[simp]

theorem fin.coe_coe_eq_self {n : ℕ} (a : fin (n + 1)) :

↑↑a = a

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

source

theorem fin.heq_fun_iff {α : Type u_1} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :

f == g ↔ ∀ (i : fin k), f i = g ⟨i.val, _⟩

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).

source

theorem fin.heq_ext_iff {k l : ℕ} (h : k = l) {i : fin k} {j : fin l} :

i == j ↔ i.val = j.val

source

@[instance]

def fin.linear_order {n : ℕ} :

linear_order (fin n)

Equations

fin.linear_order = {le := has_le.le fin.has_le, lt := has_lt.lt fin.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _}

source

@[instance]

def fin.decidable_linear_order {n : ℕ} :

decidable_linear_order (fin n)

Equations

fin.decidable_linear_order = {le := linear_order.le fin.linear_order, lt := linear_order.lt fin.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := fin.decidable_le n, decidable_eq := fin.decidable_eq n, decidable_lt := fin.decidable_lt n}

source

theorem fin.exists_iff {n : ℕ} {p : fin n → Prop} :

(∃ (i : fin n), p i) ↔ ∃ (i : ℕ) (h : i < n), p ⟨i, h⟩

source

theorem fin.forall_iff {n : ℕ} {p : fin n → Prop} :

(∀ (i : fin n), p i) ↔ ∀ (i : ℕ) (h : i < n), p ⟨i, h⟩

source

theorem fin.zero_le {n : ℕ} (a : fin (n + 1)) :

0 ≤ a

source

theorem fin.lt_iff_val_lt_val {n : ℕ} {a b : fin n} :

a < b ↔ a.val < b.val

source

theorem fin.le_iff_val_le_val {n : ℕ} {a b : fin n} :

a ≤ b ↔ a.val ≤ b.val

source

@[simp]

theorem fin.succ_val {n : ℕ} (j : fin n) :

j.succ.val = j.val.succ

source

theorem fin.succ.inj {n : ℕ} {a b : fin n} :

a.succ = b.succ → a = b

source

@[simp]

theorem fin.succ_inj {n : ℕ} {a b : fin n} :

a.succ = b.succ ↔ a = b

source

theorem fin.succ_injective (n : ℕ) :

function.injective fin.succ

source

theorem fin.succ_ne_zero {n : ℕ} (k : fin n) :

k.succ ≠ 0

source

@[simp]

theorem fin.pred_val {n : ℕ} (j : fin (n + 1)) (h : j ≠ 0) :

(j.pred h).val = j.val.pred

source

@[simp]

theorem fin.succ_pred {n : ℕ} (i : fin (n + 1)) (h : i ≠ 0) :

(i.pred h).succ = i

source

@[simp]

theorem fin.pred_succ {n : ℕ} (i : fin n) {h : i.succ ≠ 0} :

i.succ.pred h = i

source

@[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

source

def fin.last (n : ℕ) :

fin (n + 1)

The greatest value of fin (n+1)

Equations

fin.last n = ⟨n, _⟩

source

def fin.cast_lt {n m : ℕ} (i : fin m) :

i.val < n → fin n

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

Equations

i.cast_lt h = ⟨i.val, h⟩

source

def fin.cast_le {n m : ℕ} :

n ≤ m → fin n → fin m

cast_le h i embeds i into a larger fin type.

Equations

fin.cast_le h a = a.cast_lt _

source

def fin.cast {n m : ℕ} :

n = m → fin n → fin m

cast eq i embeds i into a equal fin type.

Equations

fin.cast eq = fin.cast_le _

source

def fin.cast_add {n : ℕ} (m : ℕ) :

fin n → fin (n + m)

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

Equations

fin.cast_add m = fin.cast_le _

source

def fin.cast_succ {n : ℕ} :

fin n → fin (n + 1)

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

Equations

fin.cast_succ = fin.cast_add 1

source

def fin.succ_above {n : ℕ} :

fin (n + 1) → fin n → fin (n + 1)

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

Equations

p.succ_above i = ite (i.val < p.val) i.cast_succ i.succ

source

def fin.pred_above {n : ℕ} (p i : fin (n + 1)) :

i ≠ p → fin n

pred_above p i h embeds i : fin (n+1) into fin n by ignoring p.

Equations

p.pred_above i hi = dite (i < p) (λ (h : i < p), i.cast_lt _) (λ (h : ¬i < p), i.pred _)

source

def fin.sub_nat {n : ℕ} (m : ℕ) (i : fin (n + m)) :

m ≤ i.val → fin n

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

Equations

fin.sub_nat m i h = ⟨i.val - m, _⟩

source

def fin.add_nat {n : ℕ} (m : ℕ) :

fin n → fin (n + m)

add_nat i h adds m on i, generalizes fin.succ.

Equations

fin.add_nat m i = ⟨i.val + m, _⟩

source

def fin.nat_add (n : ℕ) {m : ℕ} :

fin m → fin (n + m)

nat_add i h adds n on i

Equations

fin.nat_add n i = ⟨n + i.val, _⟩

source

theorem fin.le_last {n : ℕ} (i : fin (n + 1)) :

i ≤ fin.last n

source

@[simp]

theorem fin.cast_val {n m : ℕ} (k : fin n) (h : n = m) :

(fin.cast h k).val = k.val

source

@[simp]

theorem fin.cast_succ_val {n : ℕ} (k : fin n) :

k.cast_succ.val = k.val

source

@[simp]

theorem fin.cast_lt_val {n m : ℕ} (k : fin m) (h : k.val < n) :

(k.cast_lt h).val = k.val

source

@[simp]

theorem fin.cast_le_val {n m : ℕ} (k : fin m) (h : m ≤ n) :

(fin.cast_le h k).val = k.val

source

@[simp]

theorem fin.cast_add_val {n m : ℕ} (k : fin m) :

(fin.cast_add n k).val = k.val

source

@[simp]

theorem fin.last_val (n : ℕ) :

(fin.last n).val = n

source

@[simp]

theorem fin.coe_last {n : ℕ} :

↑(fin.last n) = n

source

@[simp]

theorem fin.succ_last (n : ℕ) :

(fin.last n).succ = fin.last n.succ

source

@[simp]

theorem fin.cast_succ_cast_lt {n : ℕ} (i : fin (n + 1)) (h : i.val < n) :

(i.cast_lt h).cast_succ = i

source

@[simp]

theorem fin.cast_lt_cast_succ {n : ℕ} (a : fin n) (h : a.val < n) :

a.cast_succ.cast_lt h = a

source

@[simp]

theorem fin.sub_nat_val {n m : ℕ} (i : fin (n + m)) (h : m ≤ i.val) :

(fin.sub_nat m i h).val = i.val - m

source

@[simp]

theorem fin.add_nat_val {n m : ℕ} (i : fin (n + m)) :

(fin.add_nat m i).val = i.val + m

source

@[simp]

theorem fin.cast_succ_inj {n : ℕ} {a b : fin n} :

a.cast_succ = b.cast_succ ↔ a = b

source

theorem fin.cast_succ_ne_last {n : ℕ} (a : fin n) :

a.cast_succ ≠ fin.last n

source

theorem fin.eq_last_of_not_lt {n : ℕ} {i : fin (n + 1)} :

¬i.val < n → i = fin.last n

source

theorem fin.cast_succ_fin_succ (n : ℕ) (j : fin n) :

j.succ.cast_succ = j.cast_succ.succ

source

def fin.clamp (n m : ℕ) :

fin (m + 1)

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

Equations

fin.clamp n m = fin.of_nat (min n m)

source

@[simp]

theorem fin.clamp_val (n m : ℕ) :

(fin.clamp n m).val = min n m

source

theorem fin.cast_le_injective {n₁ n₂ : ℕ} (h : n₁ ≤ n₂) :

function.injective (fin.cast_le h)

source

theorem fin.cast_succ_injective (n : ℕ) :

function.injective fin.cast_succ

source

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

p.succ_above i ≠ p

source

@[simp]

theorem fin.succ_above_descend {n : ℕ} (p i : fin (n + 1)) (h : i ≠ p) :

p.succ_above (p.pred_above i h) = i

source

@[simp]

theorem fin.pred_above_succ_above {n : ℕ} (p : fin (n + 1)) (i : fin n) (h : p.succ_above i ≠ p) :

p.pred_above (p.succ_above i) h = i

source

theorem fin.strict_mono_iff_lt_succ {n : ℕ} {α : Type u_1} [preorder α] {f : fin n → α} :

strict_mono f ↔ ∀ (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.

source

def fin.succ_rec {C : Π (n : ℕ), fin n → Sort u_1} (H0 : Π (n : ℕ), C n.succ 0) (Hs : Π (n : ℕ) (i : fin n), C n i → C 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

fin.succ_rec H0 Hs ⟨i.succ, h⟩ = Hs n ⟨i, _⟩ (fin.succ_rec H0 Hs ⟨i, _⟩)
fin.succ_rec H0 Hs ⟨0, _x⟩ = H0 n
fin.succ_rec H0 Hs i = i.elim0

source

def fin.succ_rec_on {n : ℕ} (i : fin n) {C : Π (n : ℕ), fin n → Sort u_1} :

(Π (n : ℕ), C n.succ 0) → (Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ) → C n i

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

Equations

i.succ_rec_on H0 Hs = fin.succ_rec H0 Hs i

source

@[simp]

theorem fin.succ_rec_on_zero {C : Π (n : ℕ), fin n → Sort u_1} {H0 : Π (n : ℕ), C n.succ 0} {Hs : Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ} (n : ℕ) :

0.succ_rec_on H0 Hs = H0 n

source

@[simp]

theorem fin.succ_rec_on_succ {C : Π (n : ℕ), fin n → Sort u_1} {H0 : Π (n : ℕ), C n.succ 0} {Hs : Π (n : ℕ) (i : fin n), C n i → C n.succ i.succ} {n : ℕ} (i : fin n) :

i.succ.succ_rec_on H0 Hs = Hs n i (i.succ_rec_on H0 Hs)

source

def fin.cases {n : ℕ} {C : fin n.succ → Sort 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

fin.cases H0 Hs ⟨i.succ, h⟩ = Hs ⟨i, _⟩
fin.cases H0 Hs ⟨0, h⟩ = H0

source

@[simp]

theorem fin.cases_zero {n : ℕ} {C : fin n.succ → Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} :

fin.cases H0 Hs 0 = H0

source

@[simp]

theorem fin.cases_succ {n : ℕ} {C : fin n.succ → Sort u_1} {H0 : C 0} {Hs : Π (i : fin n), C i.succ} (i : fin n) :

fin.cases H0 Hs i.succ = Hs i

source

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

source

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

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.

source

@[instance]

def fin.tuple0_unique (α : fin 0 → Type u) :

unique (Π (i : fin 0), α i)

There is exactly one tuple of size zero.

Equations

fin.tuple0_unique α = {to_inhabited := {default := fin_zero_elim (λ (i : fin 0), α i)}, uniq := _}

source

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

fin.tail q = λ (i : fin n), q i.succ

source

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

fin.cons x p = λ (j : fin (n + 1)), fin.cases x p j

source

@[simp]

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

fin.tail (fin.cons x p) = p

source

@[simp]

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

fin.cons x p i.succ = p i

source

@[simp]

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

fin.cons x p 0 = x

source

@[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) :

fin.cons x (function.update p i y) = function.update (fin.cons x p) i.succ y

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

source

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

function.update (fin.cons x p) 0 z = fin.cons z p

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

source

@[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

source

@[simp]

theorem fin.tail_update_zero {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (z : α 0) :

fin.tail (function.update q 0 z) = fin.tail q

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

source

@[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 (function.update q i.succ y) = function.update (fin.tail q) i y

Updating a nonzero element and taking the tail commute.

source

theorem fin.comp_cons {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (y : α) (q : fin n → α) :

g ∘ fin.cons y q = fin.cons (g y) (g ∘ q)

source

theorem fin.comp_tail {n : ℕ} {α : Type u_1} {β : Type u_2} (g : α → β) (q : fin n.succ → α) :

g ∘ fin.tail q = fin.tail (g ∘ q)

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.

source

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

α i.cast_succ

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

Equations

fin.init q i = q i.cast_succ

source

def fin.snoc {n : ℕ} {α : fin (n + 1) → Type u} (p : Π (i : fin n), α i.cast_succ) (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

fin.snoc p x i = dite (i.val < n) (λ (h : i.val < n), cast _ (p (i.cast_lt h))) (λ (h : ¬i.val < n), cast _ x)

source

@[simp]

theorem fin.init_snoc {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) :

fin.init (fin.snoc p x) = p

source

@[simp]

theorem fin.snoc_cast_succ {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) (i : fin n) :

fin.snoc p x i.cast_succ = p i

source

@[simp]

theorem fin.snoc_last {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) :

fin.snoc p x (fin.last n) = x

source

@[simp]

theorem fin.snoc_update {n : ℕ} {α : fin (n + 1) → Type u} (x : α (fin.last n)) (p : Π (i : fin n), α i.cast_succ) (i : fin n) (y : α i.cast_succ) :

fin.snoc (function.update p i y) x = function.update (fin.snoc p x) i.cast_succ y

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

source

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

function.update (fin.snoc p x) (fin.last n) z = fin.snoc p z

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

source

@[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

source

@[simp]

theorem fin.init_update_last {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (z : α (fin.last n)) :

fin.init (function.update q (fin.last n) z) = fin.init q

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

source

@[simp]

theorem fin.init_update_cast_succ {n : ℕ} {α : fin (n + 1) → Type u} (q : Π (i : fin (n + 1)), α i) (i : fin n) (y : α i.cast_succ) :

fin.init (function.update q i.cast_succ y) = function.update (fin.init q) i y

Updating an element and taking the beginning commute.

source

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

fin.tail (fin.init q) = fin.init (fin.tail q)

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.

source

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

fin.cons a (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.

source