Documentation

Mathlib.Data.Fin.Fin2

Inductive type variant of Fin #

Fin is defined as a subtype of . This file defines an equivalent type, Fin2, which is defined inductively. This is useful for its induction principle and different definitional equalities.

Main declarations #

inductive Fin2 :
Type

An alternate definition of Fin n defined as an inductive type instead of a subtype of .

Instances For
    def Fin2.cases' {n : } {C : Fin2 (Nat.succ n)Sort u} (H1 : C Fin2.fz) (H2 : (n : Fin2 n) → C (Fin2.fs n)) (i : Fin2 (Nat.succ n)) :
    C i

    Define a dependent function on Fin2 (succ n) by giving its value at zero (H1) and by giving a dependent function on the rest (H2).

    Equations
    def Fin2.elim0 {C : Fin2 0Sort u} (i : Fin2 0) :
    C i

    Ex falso. The dependent eliminator for the empty Fin2 0 type.

    Equations
    def Fin2.toNat {n : } :
    Fin2 n

    Converts a Fin2 into a natural.

    Equations
    def Fin2.optOfNat {n : } :
    Option (Fin2 n)

    Converts a natural into a Fin2 if it is in range

    Equations
    def Fin2.add {n : } (i : Fin2 n) (k : ) :
    Fin2 (n + k)

    i + k : Fin2 (n + k) when i : Fin2 n and k : ℕ

    Equations
    def Fin2.left (k : ) {n : } :
    Fin2 nFin2 (k + n)

    left k is the embedding Fin2 n → Fin2 (k + n)→ Fin2 (k + n)

    Equations
    def Fin2.insertPerm {n : } :
    Fin2 nFin2 nFin2 n

    insertPerm a is a permutation of Fin2 n with the following properties:

    • insertPerm a i = i+1 if i < a
    • insertPerm a a = 0
    • insertPerm a i = i if i > a
    Equations
    def Fin2.remapLeft {m : } {n : } (f : Fin2 mFin2 n) (k : ) :
    Fin2 (m + k)Fin2 (n + k)

    remapLeft f k : Fin2 (m + k) → Fin2 (n + k)→ Fin2 (n + k) applies the function f : Fin2 m → Fin2 n→ Fin2 n to inputs less than m, and leaves the right part on the right (that is, remapLeft f k (m + i) = n + i).

    Equations
    class Fin2.IsLT (m : ) (n : ) :
    • The unique field of Fin2.IsLT, a proof that m < n.

      h : m < n

    This is a simple type class inference prover for proof obligations of the form m < n where m n : ℕ.

    Instances
      instance Fin2.IsLT.zero (n : ) :
      Equations
      instance Fin2.IsLT.succ (m : ) (n : ) [l : Fin2.IsLT m n] :
      Equations
      def Fin2.ofNat' {n : } (m : ) [inst : Fin2.IsLT m n] :

      Use type class inference to infer the boundedness proof, so that we can directly convert a Nat into a Fin2 n. This supports notation like &1 : Fin 3.

      Equations