Documentation

Mathlib.Data.Fin.Tuple.Reflection

Lemmas for tuples Fin m → α #

This file contains alternative definitions of common operators on vectors which expand definitionally to the expected expression when evaluated on ![] notation.

This allows "proof by reflection", where we prove f = ![f 0, f 1] by defining FinVec.etaExpand f to be equal to the RHS definitionally, and then prove that f = etaExpand f.

The definitions in this file should normally not be used directly; the intent is for the corresponding *_eq lemmas to be used in a place where they are definitionally unfolded.

Main definitions #

def FinVec.seq {α : Type u_1} {β : Type u_2} {m : } :
(Fin mαβ)(Fin mα)Fin mβ

Evaluate FinVec.seq f v = ![(f 0) (v 0), (f 1) (v 1), ...]

Equations
Instances For
    @[simp]
    theorem FinVec.seq_eq {α : Type u_1} {β : Type u_2} {m : } (f : Fin mαβ) (v : Fin mα) :
    FinVec.seq f v = fun (i : Fin m) => f i (v i)
    def FinVec.map {α : Type u_1} {β : Type u_2} (f : αβ) {m : } :
    (Fin mα)Fin mβ

    FinVec.map f v = ![f (v 0), f (v 1), ...]

    Equations
    Instances For
      @[simp]
      theorem FinVec.map_eq {α : Type u_1} {β : Type u_2} (f : αβ) {m : } (v : Fin mα) :
      FinVec.map f v = f v

      This can be use to prove

      example {f : α → β} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂] :=
        (map_eq _ _).symm
      
      def FinVec.etaExpand {α : Type u_1} {m : } (v : Fin mα) :
      Fin mα

      Expand v to ![v 0, v 1, ...]

      Equations
      Instances For
        @[simp]
        theorem FinVec.etaExpand_eq {α : Type u_1} {m : } (v : Fin mα) :

        This can be use to prove

        example (a : Fin 2 → α) : a = ![a 0, a 1] :=
          (etaExpand_eq _).symm
        
        def FinVec.Forall {α : Type u_1} {m : } :
        ((Fin mα)Prop)Prop

        with better defeq for ∀ x : Fin m → α, P x.

        Equations
        Instances For
          @[simp]
          theorem FinVec.forall_iff {α : Type u_1} {m : } (P : (Fin mα)Prop) :
          FinVec.Forall P ∀ (x : Fin mα), P x

          This can be use to prove

          example (P : (Fin 2 → α) → Prop) : (∀ f, P f) ↔ ∀ a₀ a₁, P ![a₀, a₁] :=
            (forall_iff _).symm
          
          def FinVec.Exists {α : Type u_1} {m : } :
          ((Fin mα)Prop)Prop

          with better defeq for ∃ x : Fin m → α, P x.

          Equations
          Instances For
            theorem FinVec.exists_iff {α : Type u_1} {m : } (P : (Fin mα)Prop) :
            FinVec.Exists P ∃ (x : Fin mα), P x

            This can be use to prove

            example (P : (Fin 2 → α) → Prop) : (∃ f, P f) ↔ ∃ a₀ a₁, P ![a₀, a₁] :=
              (exists_iff _).symm
            
            def FinVec.sum {α : Type u_1} [Add α] [Zero α] {m : } :
            (Fin mα)α

            Finset.univ.sum with better defeq for Fin.

            Equations
            Instances For
              @[simp]
              theorem FinVec.sum_eq {α : Type u_1} [AddCommMonoid α] {m : } (a : Fin mα) :
              FinVec.sum a = i : Fin m, a i

              This can be used to prove

              example [AddCommMonoid α] (a : Fin 3 → α) : ∑ i, a i = a 0 + a 1 + a 2 :=
                (sum_eq _).symm