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 n.succSort u} (H1 : C Fin2.fz) (H2 : (n_1 : Fin2 n) → C n_1.fs) (i : Fin2 n.succ) :
    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
    • Fin2.cases' H1 H2 x = match x with | Fin2.fz => H1 | n.fs => H2 n
    Instances For
      def Fin2.elim0 {C : Fin2 0Sort u} (i : Fin2 0) :
      C i

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

      Equations
      • a.elim0 = nomatch a
      Instances For
        def Fin2.toNat {n : } :
        Fin2 n

        Converts a Fin2 into a natural.

        Equations
        • Fin2.fz.toNat = 0
        • i.fs.toNat = i.toNat.succ
        Instances For
          def Fin2.optOfNat {n : } :
          Option (Fin2 n)

          Converts a natural into a Fin2 if it is in range

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

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

            Equations
            • i.add 0 = i
            • i.add k.succ = (i.add k).fs
            Instances For
              def Fin2.left (k : ) {n : } :
              Fin2 nFin2 (k + n)

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

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

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

                Equations
                • Fin2.fz.insertPerm Fin2.fz = Fin2.fz
                • Fin2.fz.insertPerm j.fs = j.fs
                • a_1.fs.insertPerm Fin2.fz = Fin2.fz.fs
                • i.fs.insertPerm j.fs = match i.insertPerm j with | Fin2.fz => Fin2.fz | k.fs => k.fs.fs
                Instances For
                  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) applies the function f : Fin2 m → 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
                  Instances For
                    class Fin2.IsLT (m : ) (n : ) :

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

                    • h : m < n

                      The unique field of Fin2.IsLT, a proof that m < n.

                    Instances
                      theorem Fin2.IsLT.h {m : } {n : } [self : Fin2.IsLT m n] :
                      m < n

                      The unique field of Fin2.IsLT, a proof that m < n.

                      instance Fin2.IsLT.zero (n : ) :
                      Fin2.IsLT 0 n.succ
                      Equations
                      • =
                      instance Fin2.IsLT.succ (m : ) (n : ) [l : Fin2.IsLT m n] :
                      Fin2.IsLT m.succ n.succ
                      Equations
                      • =
                      def Fin2.ofNat' {n : } (m : ) [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
                      Instances For
                        def Fin2.castSucc {n : } :
                        Fin2 nFin2 (n + 1)

                        castSucc i embeds i : Fin2 n in Fin2 (n+1).

                        Equations
                        • Fin2.fz.castSucc = Fin2.fz
                        • i.fs.castSucc = i.castSucc.fs
                        Instances For
                          def Fin2.last {n : } :
                          Fin2 (n + 1)

                          The greatest value of Fin2 (n+1).

                          Equations
                          • Fin2.last = Fin2.fz
                          • Fin2.last = Fin2.last.fs
                          Instances For
                            def Fin2.rev {n : } :
                            Fin2 nFin2 n

                            Maps 0 to n-1, 1 to n-2, ..., n-1 to 0.

                            Equations
                            • Fin2.fz.rev = Fin2.last
                            • i.fs.rev = i.rev.castSucc
                            Instances For
                              @[simp]
                              theorem Fin2.rev_last {n : } :
                              Fin2.last.rev = Fin2.fz
                              @[simp]
                              theorem Fin2.rev_castSucc {n : } (i : Fin2 n) :
                              i.castSucc.rev = i.rev.fs
                              @[simp]
                              theorem Fin2.rev_rev {n : } (i : Fin2 n) :
                              i.rev.rev = i
                              Equations
                              instance Fin2.instFintype (n : ) :
                              Equations