Documentation

Init.Data.Fin.Basic

instance Fin.coeToNat {n : Nat} :
Equations
  • Fin.coeToNat = { coe := fun (v : Fin n) => v }
def Fin.elim0 {α : Sort u} :
Fin 0α

From the empty type Fin 0, any desired result α can be derived. This is similar to Empty.elim.

Equations
Instances For
    def Fin.succ {n : Nat} :
    Fin nFin (n + 1)

    Returns the successor of the argument.

    The bound in the result type is increased:

    (2 : Fin 3).succ = (3 : Fin 4)
    

    This differs from addition, which wraps around:

    (2 : Fin 3) + 1 = (0 : Fin 3)
    
    Equations
    • i, h.succ = i + 1,
    Instances For
      def Fin.ofNat {n : Nat} (a : Nat) :
      Fin (n + 1)

      Returns a modulo n + 1 as a Fin n.succ.

      Equations
      Instances For
        def Fin.ofNat' (n : Nat) [NeZero n] (a : Nat) :
        Fin n

        Returns a modulo n as a Fin n.

        The assumption NeZero n ensures that Fin n is nonempty.

        Equations
        Instances For
          def Fin.add {n : Nat} :
          Fin nFin nFin n

          Addition modulo n

          Equations
          • a, h.add b, isLt = (a + b) % n,
          Instances For
            def Fin.mul {n : Nat} :
            Fin nFin nFin n

            Multiplication modulo n

            Equations
            • a, h.mul b, isLt = a * b % n,
            Instances For
              def Fin.sub {n : Nat} :
              Fin nFin nFin n

              Subtraction modulo n

              Equations
              • a, h.sub b, isLt = (n - b + a) % n,
              Instances For

                Remark: land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to bootstrap Lean.

                def Fin.mod {n : Nat} :
                Fin nFin nFin n
                Equations
                • a, h.mod b, isLt = a % b,
                Instances For
                  def Fin.div {n : Nat} :
                  Fin nFin nFin n
                  Equations
                  • a, h.div b, isLt = a / b,
                  Instances For
                    def Fin.modn {n : Nat} :
                    Fin nNatFin n
                    Equations
                    • a, h.modn x = a % x,
                    Instances For
                      def Fin.land {n : Nat} :
                      Fin nFin nFin n
                      Equations
                      • a, h.land b, isLt = a.land b % n,
                      Instances For
                        def Fin.lor {n : Nat} :
                        Fin nFin nFin n
                        Equations
                        • a, h.lor b, isLt = a.lor b % n,
                        Instances For
                          def Fin.xor {n : Nat} :
                          Fin nFin nFin n
                          Equations
                          • a, h.xor b, isLt = a.xor b % n,
                          Instances For
                            def Fin.shiftLeft {n : Nat} :
                            Fin nFin nFin n
                            Equations
                            • a, h.shiftLeft b, isLt = a <<< b % n,
                            Instances For
                              def Fin.shiftRight {n : Nat} :
                              Fin nFin nFin n
                              Equations
                              • a, h.shiftRight b, isLt = a >>> b % n,
                              Instances For
                                instance Fin.instAdd {n : Nat} :
                                Add (Fin n)
                                Equations
                                • Fin.instAdd = { add := Fin.add }
                                instance Fin.instSub {n : Nat} :
                                Sub (Fin n)
                                Equations
                                • Fin.instSub = { sub := Fin.sub }
                                instance Fin.instMul {n : Nat} :
                                Mul (Fin n)
                                Equations
                                • Fin.instMul = { mul := Fin.mul }
                                instance Fin.instMod {n : Nat} :
                                Mod (Fin n)
                                Equations
                                • Fin.instMod = { mod := Fin.mod }
                                instance Fin.instDiv {n : Nat} :
                                Div (Fin n)
                                Equations
                                • Fin.instDiv = { div := Fin.div }
                                instance Fin.instAndOp {n : Nat} :
                                Equations
                                • Fin.instAndOp = { and := Fin.land }
                                instance Fin.instOrOp {n : Nat} :
                                OrOp (Fin n)
                                Equations
                                • Fin.instOrOp = { or := Fin.lor }
                                instance Fin.instXor {n : Nat} :
                                Xor (Fin n)
                                Equations
                                • Fin.instXor = { xor := Fin.xor }
                                instance Fin.instShiftLeft {n : Nat} :
                                Equations
                                • Fin.instShiftLeft = { shiftLeft := Fin.shiftLeft }
                                instance Fin.instShiftRight {n : Nat} :
                                Equations
                                • Fin.instShiftRight = { shiftRight := Fin.shiftRight }
                                instance Fin.instOfNat {n : Nat} [NeZero n] {i : Nat} :
                                OfNat (Fin n) i
                                Equations
                                instance Fin.instInhabited {n : Nat} [NeZero n] :
                                Equations
                                • Fin.instInhabited = { default := 0 }
                                @[simp]
                                theorem Fin.zero_eta {n : Nat} :
                                0, = 0
                                theorem Fin.ne_of_val_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
                                i j
                                theorem Fin.val_ne_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i j) :
                                i j
                                theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) :
                                m > 0(i.modn m) < m
                                theorem Fin.val_lt_of_le {n : Nat} {b : Nat} (i : Fin b) (h : b n) :
                                i < n
                                theorem Fin.pos {n : Nat} (i : Fin n) :
                                0 < n
                                @[inline]
                                def Fin.last (n : Nat) :
                                Fin (n + 1)

                                The greatest value of Fin (n+1).

                                Equations
                                Instances For
                                  @[inline]
                                  def Fin.castLT {n : Nat} {m : Nat} (i : Fin m) (h : i < n) :
                                  Fin n

                                  castLT i h embeds i into a Fin where h proves it belongs into.

                                  Equations
                                  • i.castLT h = i, h
                                  Instances For
                                    @[inline]
                                    def Fin.castLE {n : Nat} {m : Nat} (h : n m) (i : Fin n) :
                                    Fin m

                                    castLE h i embeds i into a larger Fin type.

                                    Equations
                                    Instances For
                                      @[inline]
                                      def Fin.cast {n : Nat} {m : Nat} (eq : n = m) (i : Fin n) :
                                      Fin m

                                      cast eq i embeds i into an equal Fin type.

                                      Equations
                                      Instances For
                                        @[inline]
                                        def Fin.castAdd {n : Nat} (m : Nat) :
                                        Fin nFin (n + m)

                                        castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

                                        Equations
                                        Instances For
                                          @[inline]
                                          def Fin.castSucc {n : Nat} :
                                          Fin nFin (n + 1)

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

                                          Equations
                                          Instances For
                                            def Fin.addNat {n : Nat} (i : Fin n) (m : Nat) :
                                            Fin (n + m)

                                            addNat m i adds m to i, generalizes Fin.succ.

                                            Equations
                                            • i.addNat m = i + m,
                                            Instances For
                                              def Fin.natAdd {m : Nat} (n : Nat) (i : Fin m) :
                                              Fin (n + m)

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

                                              Equations
                                              Instances For
                                                @[inline]
                                                def Fin.rev {n : Nat} (i : Fin n) :
                                                Fin n

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

                                                Equations
                                                • i.rev = n - (i + 1),
                                                Instances For
                                                  @[inline]
                                                  def Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m i) :
                                                  Fin n

                                                  subNat i h subtracts m from i, generalizes Fin.pred.

                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i 0) :
                                                    Fin n

                                                    Predecessor of a nonzero element of Fin (n+1).

                                                    Equations
                                                    Instances For
                                                      theorem Fin.val_inj {n : Nat} {a : Fin n} {b : Fin n} :
                                                      a = b a = b
                                                      theorem Fin.val_congr {n : Nat} {a : Fin n} {b : Fin n} (h : a = b) :
                                                      a = b
                                                      theorem Fin.val_le_of_le {n : Nat} {a : Fin n} {b : Fin n} (h : a b) :
                                                      a b
                                                      theorem Fin.val_le_of_ge {n : Nat} {a : Fin n} {b : Fin n} (h : a b) :
                                                      b a
                                                      theorem Fin.val_add_one_le_of_lt {n : Nat} {a : Fin n} {b : Fin n} (h : a < b) :
                                                      a + 1 b
                                                      theorem Fin.val_add_one_le_of_gt {n : Nat} {a : Fin n} {b : Fin n} (h : a > b) :
                                                      b + 1 a
                                                      theorem Fin.exists_iff {n : Nat} {p : Fin nProp} :
                                                      (∃ (i : Fin n), p i) ∃ (i : Nat), ∃ (h : i < n), p i, h