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α) :
      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α) :
          map f v = f v

          This can be used 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 used 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) :
                  Forall P ∀ (x : Fin mα), P x

                  This can be used 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) :
                      Exists P ∃ (x : Fin mα), P x

                      This can be used 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
                          def FinVec.prod {α : Type u_1} [Mul α] [One α] {m : } :
                          (Fin mα)α

                          Finset.univ.prod with better defeq for Fin.

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

                              This can be used to prove

                              example [CommMonoid α] (a : Fin 3 → α) : ∏ i, a i = a 0 * a 1 * a 2 :=
                                (prod_eq _).symm
                              
                              @[simp]
                              theorem FinVec.sum_eq {α : Type u_1} [AddCommMonoid α] {m : } (a : Fin mα) :
                              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
                              
                              def FinVec.mkProdEqQ {u : Lean.Level} {α : Q(Type u)} (inst : Q(CommMonoid «$α»)) (n : ) (f : Q(Fin «$n»«$α»)) :
                              Lean.MetaM ((val : Q(«$α»)) × Q(i : Fin «$n», «$f» i = «$val»))

                              Produce a term of the form f 0 * f 1 * ... * f (n - 1) and an application of FinVec.prod_eq that shows it is equal to ∏ i, f i.

                              Equations
                                Instances For
                                  def FinVec.mkProdEqQ.makeRHS {u : Lean.Level} {α : Q(Type u)} (inst : Q(CommMonoid «$α»)) (n : ) (f : Q(Fin «$n»«$α»)) (nezero : Q(NeZero «$n»)) (k : ) :
                                  Lean.MetaM Q(«$α»)

                                  Creates the expression f 0 * f 1 * ... * f (n - 1).

                                  Equations
                                    Instances For
                                      def FinVec.mkSumEqQ {u : Lean.Level} {α : Q(Type u)} (inst : Q(AddCommMonoid «$α»)) (n : ) (f : Q(Fin «$n»«$α»)) :
                                      Lean.MetaM ((val : Q(«$α»)) × Q(i : Fin «$n», «$f» i = «$val»))

                                      Produce a term of the form f 0 + f 1 + ... + f (n - 1) and an application of FinVec.sum_eq that shows it is equal to ∑ i, f i.

                                      Equations
                                        Instances For
                                          def FinVec.mkSumEqQ.makeRHS {u : Lean.Level} {α : Q(Type u)} (inst : Q(AddCommMonoid «$α»)) (n : ) (f : Q(Fin «$n»«$α»)) (nezero : Q(NeZero «$n»)) (k : ) :
                                          Lean.MetaM Q(«$α»)

                                          Creates the expression f 0 + f 1 + ... + f (n - 1).

                                          Equations
                                            Instances For

                                              Rewrites ∏ i : Fin n, f i as f 0 * f 1 * ... * f (n - 1) when n is a numeral.

                                              Equations
                                                Instances For

                                                  Rewrites ∑ i : Fin n, f i as f 0 + f 1 + ... + f (n - 1) when n is a numeral.

                                                  Equations
                                                    Instances For