Low-level coding recipes for Fin types

This module collects encoding/decoding bijections to represent basic type constructors of Fin types as Fin types. These functions implement the isomorphism Option (Fin n) ≃ Fin (n+1), Fin m ⊕ Fin n ≃ Fin (m + n), Fin m × Fin n ≃ Fin (m * n), ..., including, dependent sums, dependent products, decidable subtypes and decidable quotients.

Only a minimal API is provided. These utility functions are intended for use in other constructions. Such constructions should avoid exposing these functions as they are not meant for public use.

def Fin.encodeEmpty : Empty → Fin 0

Encode Empty into Fin 0.

def Fin.decodeEmpty : Fin 0 → Empty

Decode Empty from Fin 0.

@[simp]

theorem Fin.encodeEmpty_decodeEmpty (x : Fin 0) : encodeEmpty x.decodeEmpty = x

@[simp]

theorem Fin.decodeEmpty_encodeEmpty (x : Empty) : (encodeEmpty x).decodeEmpty = x

def Fin.encodePUnit : PUnit → Fin 1

Encode PUnit into Fin 1.

Equations

• Fin.encodePUnit x✝ = 0

def Fin.decodePUnit : Fin 1 → PUnit

Decode PUnit from Fin 1.

Equations

• Fin.decodePUnit 0 = PUnit.unit

@[reducible, inline]

abbrev Fin.encodeUnit : Unit → Fin 1

Encode Unit into Fin 1.

Equations

• Fin.encodeUnit = Fin.encodePUnit

@[reducible, inline]

abbrev Fin.decodeUnit : Fin 1 → Unit

Decode Unit from Fin 1.

Equations

• Fin.decodeUnit = Fin.decodePUnit

@[simp]

theorem Fin.encodePUnit_decodePUnit (x : Fin 1) : encodePUnit (decodePUnit x) = x

@[simp]

theorem Fin.decodePUnit_encodePUnit (x : PUnit) : decodePUnit (encodePUnit x) = x

def Fin.encodeBool : Bool → Fin 2

Encode Bool into Fin 2.

Equations

• Fin.encodeBool false = 0
• Fin.encodeBool true = 1

def Fin.decodeBool : Fin 2 → Bool

Decode Bool from Fin 2.

Equations

• Fin.decodeBool 0 = false
• Fin.decodeBool 1 = true

@[simp]

theorem Fin.encodeBool_decodeBool (x : Fin 2) : encodeBool (decodeBool x) = x

@[simp]

theorem Fin.decodeBool_encodeBool (x : Bool) : decodeBool (encodeBool x) = x

def Fin.encodeOrdering : Ordering → Fin 3

Encode Ordering into Fin 3.

Equations

• Fin.encodeOrdering Ordering.lt = 0
• Fin.encodeOrdering Ordering.eq = 1
• Fin.encodeOrdering Ordering.gt = 2

def Fin.decodeOrdering : Fin 3 → Ordering

Decode Ordering from Fin 3.

Equations

• Fin.decodeOrdering 0 = Ordering.lt
• Fin.decodeOrdering 1 = Ordering.eq
• Fin.decodeOrdering 2 = Ordering.gt

@[simp]

theorem Fin.encodeOrdering_decodeOrdering (x : Fin 3) : encodeOrdering (decodeOrdering x) = x

@[simp]

theorem Fin.decodeOrdering_encodeOrdering (x : Ordering) : decodeOrdering (encodeOrdering x) = x

def Fin.encodeChar (c : Char) : Fin Char.count

Encode Char into Fin Char.count.

Equations

• Fin.encodeChar c = if x : c.toNat < Char.minSurrogate then ⟨c.toNat, ⋯⟩ else ⟨c.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate), ⋯⟩

def Fin.decodeChar (i : Fin Char.count) : Char

Decode Char from Fin Char.count.

Equations

• Fin.decodeChar i = if x : ↑i < Char.minSurrogate then Char.ofNatAux ↑i ⋯ else Char.ofNatAux (↑i + (Char.maxSurrogate + 1 - Char.minSurrogate)) ⋯

@[simp]

theorem Fin.encodeChar_decodeChar (x : Fin Char.count) : encodeChar (decodeChar x) = x

@[simp]

theorem Fin.decodeChar_encodeChar (x : Char) : decodeChar (encodeChar x) = x

def Fin.encodeOption {n : Nat} : Option (Fin n) → Fin (n + 1)

Encode Option (Fin n) into Fin (n+1).

Equations

• Fin.encodeOption none = 0
• Fin.encodeOption (some ⟨i, h⟩) = ⟨i + 1, ⋯⟩

def Fin.decodeOption {n : Nat} : Fin (n + 1) → Option (Fin n)

Decode Option (Fin n) from Fin (n+1).

Equations

• Fin.decodeOption ⟨0, ⋯⟩ = none
• Fin.decodeOption ⟨i.succ, h⟩ = some ⟨i, ⋯⟩

@[simp]

theorem Fin.encodeOption_decodeOption {n : Nat} (x : Fin (n + 1)) : encodeOption (decodeOption x) = x

@[simp]

theorem Fin.decodeOption_encodeOption {n : Nat} (x : Option (Fin n)) : decodeOption (encodeOption x) = x

def Fin.encodeSum {n m : Nat} : Fin n ⊕ Fin m → Fin (n + m)

Encode Fin n ⊕ Fin m into Fin (n + m).

Equations

• Fin.encodeSum (Sum.inl x_1) = Fin.castAdd m x_1
• Fin.encodeSum (Sum.inr x_1) = Fin.natAdd n x_1

def Fin.decodeSum {n m : Nat} (x : Fin (n + m)) : Fin n ⊕ Fin m

Decode Fin n ⊕ Fin m from Fin (n + m).

Equations

• Fin.decodeSum x = Fin.addCases Sum.inl Sum.inr x

@[simp]

theorem Fin.encodeSum_decodeSum {n m : Nat} (x : Fin (n + m)) : encodeSum (decodeSum x) = x

@[simp]

theorem Fin.decodeSum_encodeSum {n m : Nat} (x : Fin n ⊕ Fin m) : decodeSum (encodeSum x) = x

def Fin.encodeProd {m n : Nat} : Fin m × Fin n → Fin (m * n)

Encode Fin m × Fin n into Fin (m * n).

Equations

• Fin.encodeProd (i, j) = i.mkDivMod j

def Fin.decodeProd {m n : Nat} (z : Fin (m * n)) : Fin m × Fin n

Decode Fin m × Fin n from Fin (m * n).

Equations

• Fin.decodeProd z = (z.divNat, z.modNat)

@[simp]

theorem Fin.encodeProd_decodeProd {m n : Nat} (x : Fin (m * n)) : encodeProd (decodeProd x) = x

@[simp]

theorem Fin.decodeProd_encodeProd {m n : Nat} (x : Fin m × Fin n) : decodeProd (encodeProd x) = x

def Fin.encodeSigma {n : Nat} (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : Fin (Fin.sum f)

Encode (i : Fin n) × Fin (f i) into Fin (Fin.sum f).

Equations

• Fin.encodeSigma f_2 ⟨⟨0, ⋯⟩, j⟩ = ⟨↑j, ⋯⟩
• Fin.encodeSigma f_2 ⟨⟨i.succ, hi⟩, j⟩ = match Fin.encodeSigma (fun (x : Fin n_2) => f_2 x.succ) ⟨⟨i, ⋯⟩, j⟩ with | ⟨k, hk⟩ => ⟨f_2 0 + k, ⋯⟩

def Fin.decodeSigma {n : Nat} (f : Fin n → Nat) (x : Fin (Fin.sum f)) : (i : Fin n) × Fin (f i)

Decode (i : Fin n) × Fin (f i) from Fin (Fin.sum f).

Equations

• One or more equations did not get rendered due to their size.
• Fin.decodeSigma x_2 ⟨val, h⟩ = ⋯.elim

@[simp]

theorem Fin.encodeSigma_decodeSigma {n : Nat} (f : Fin n → Nat) (x : Fin (Fin.sum f)) : encodeSigma f (decodeSigma f x) = x

@[simp]

theorem Fin.decodeSigma_encodeSigma {n : Nat} (f : Fin n → Nat) (x : (i : Fin n) × Fin (f i)) : decodeSigma f (encodeSigma f x) = x

def Fin.encodeFun {n m : Nat} : (Fin m → Fin n) → Fin (n ^ m)

Encode Fin m → Fin n into Fin (n ^ m).

Equations

• Fin.encodeFun x_2 = ⟨0, ⋯⟩
• Fin.encodeFun f = ⟨n * ↑(Fin.encodeFun fun (k : Fin m) => f k.succ) + ↑(f 0), ⋯⟩

def Fin.decodeFun {n m : Nat} : Fin (n ^ m) → Fin m → Fin n

Decode Fin m → Fin n from Fin (n ^ m).

Equations

• Fin.decodeFun x_2 = fun (x : Fin 0) => nomatch x
• Fin.decodeFun ⟨k, hk⟩ = fun (x : Fin (m + 1)) => match x with | ⟨0, ⋯⟩ => ⟨k % n, ⋯⟩ | ⟨i.succ, hi⟩ => have h := ⋯; Fin.decodeFun ⟨k / n, h⟩ ⟨i, ⋯⟩

@[simp]

theorem Fin.encodeFun_decodeFun {n m : Nat} (x : Fin (n ^ m)) : encodeFun (decodeFun x) = x

@[simp]

theorem Fin.decodeFun_encodeFun {m n : Nat} (x : Fin m → Fin n) : decodeFun (encodeFun x) = x

def Fin.encodePi {n : Nat} (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : Fin (Fin.prod f)

Encode (i : Fin n) → Fin (f i) into Fin (Fin.prod f).

Equations

• One or more equations did not get rendered due to their size.
• Fin.encodePi x_2 x_3 = ⟨0, ⋯⟩

def Fin.decodePi {n : Nat} (f : Fin n → Nat) (x : Fin (Fin.prod f)) (i : Fin n) : Fin (f i)

Decode (i : Fin n) → Fin (f i) from Fin (Fin.prod f).

Equations

• Fin.decodePi x_2 x_3 = fun (x : Fin 0) => nomatch x
• Fin.decodePi f_2 ⟨x_2, hx⟩ = fun (x : Fin (n_2 + 1)) => match x with | ⟨0, isLt⟩ => ⟨x_2 % f_2 0, ⋯⟩ | ⟨i.succ, hi⟩ => Fin.decodePi (fun (x : Fin n_2) => f_2 x.succ) ⟨x_2 / f_2 0, ⋯⟩ ⟨i, ⋯⟩

@[simp]

theorem Fin.encodePi_decodePi {n : Nat} (f : Fin n → Nat) (x : Fin (Fin.prod f)) : encodePi f (decodePi f x) = x

@[simp]

theorem Fin.decodePi_encodePi {n : Nat} (f : Fin n → Nat) (x : (i : Fin n) → Fin (f i)) : decodePi f (encodePi f x) = x

def Fin.encodeSubtype {n : Nat} (P : Fin n → Prop) [inst : DecidablePred P] (i : { i : Fin n // P i }) : Fin (Fin.countP fun (x : Fin n) => decide (P x))

Encode { i : Fin n // P i } into Fin (Fin.countP P) where P is a decidable predicate.

Equations

• One or more equations did not get rendered due to their size.
• Fin.encodeSubtype P_2 ⟨⟨0, ⋯⟩, hp⟩ = ⟨0, ⋯⟩

def Fin.decodeSubtype {n : Nat} (P : Fin n → Prop) [inst : DecidablePred P] (k : Fin (Fin.countP fun (x : Fin n) => decide (P x))) : { i : Fin n // P i }

Decode { i : Fin n // P i } from Fin (Fin.countP P) where P is a decidable predicate.

Equations

• One or more equations did not get rendered due to their size.
• Fin.decodeSubtype x ⟨val, h⟩ = ⋯.elim

theorem Fin.encodeSubtype_zero_pos {n : Nat} {P : Fin (n + 1) → Prop} [DecidablePred P] (h₀ : P 0) : encodeSubtype P ⟨0, h₀⟩ = ⟨0, ⋯⟩

theorem Fin.encodeSubtype_succ_pos {n : Nat} {P : Fin (n + 1) → Prop} [DecidablePred P] (h₀ : P 0) {i : Fin n} (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = Fin.cast ⋯ (encodeSubtype (fun (i : Fin n) => P i.succ) ⟨i, h⟩).succ

theorem Fin.encodeSubtype_succ_neg {n : Nat} {P : Fin (n + 1) → Prop} [DecidablePred P] (h₀ : ¬P 0) {i : Fin n} (h : P i.succ) : encodeSubtype P ⟨i.succ, h⟩ = Fin.cast ⋯ (encodeSubtype (fun (i : Fin n) => P i.succ) ⟨i, h⟩)

@[simp]

theorem Fin.encodeSubtype_decodeSubtype {n : Nat} (P : Fin n → Prop) [DecidablePred P] (x : Fin (Fin.countP fun (x : Fin n) => decide (P x))) : encodeSubtype P (decodeSubtype P x) = x

@[simp]

theorem Fin.decodeSubtype_encodeSubtype {n : Nat} (P : Fin n → Prop) [DecidablePred P] (x : { x : Fin n // P x }) : decodeSubtype P (encodeSubtype P x) = x

@[reducible, inline]

abbrev Fin.getRepr {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Fin n) : Fin n

Get representative for the equivalence class of x.

Equations

• Fin.getRepr s x = match h : Fin.find? fun (y : Fin n) => decide (Setoid.r x y) with | some y => y | none => ⋯.elim

@[simp]

theorem Fin.equiv_getRepr {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Fin n) : Setoid.r x (getRepr s x)

@[simp]

theorem Fin.getRepr_equiv {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Fin n) : Setoid.r (getRepr s x) x

theorem Fin.getRepr_eq_getRepr_of_equiv {n : Nat} {x y : Fin n} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (h : Setoid.r x y) : getRepr s x = getRepr s y

@[simp]

theorem Fin.getRepr_getRepr {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Fin n) : getRepr s (getRepr s x) = getRepr s x

def Fin.encodeQuotient {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Quotient s) : Fin (Fin.countP fun (i : Fin n) => decide (getRepr s i = i))

Encode Quotient s into Fin m where s is a decidable setoid on Fin n.

Equations

• Fin.encodeQuotient s x = Fin.encodeSubtype (fun (i : Fin n) => Fin.getRepr s i = i) (x.liftOn (fun (i : Fin n) => ⟨Fin.getRepr s i, ⋯⟩) ⋯)

def Fin.decodeQuotient {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (i : Fin (Fin.countP fun (i : Fin n) => decide (getRepr s i = i))) : Quotient s

Decode Quotient s from Fin m where s is a decidable setoid on Fin n.

Equations

• Fin.decodeQuotient s i = Quotient.mk s (Fin.decodeSubtype (fun (x : Fin n) => Fin.getRepr s x = x) i).val

@[simp]

theorem Fin.encodeQuotient_decodeQuotient {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Fin (Fin.countP fun (i : Fin n) => decide (getRepr s i = i))) : encodeQuotient s (decodeQuotient s x) = x

@[simp]

theorem Fin.decodeQuotient_encodeQuotient {n : Nat} (s : Setoid (Fin n)) [DecidableRel Setoid.r] (x : Quotient s) : decodeQuotient s (encodeQuotient s x) = x