Documentation

Mathlib.Tactic.NormNum.BigOperators

norm_num plugin for big operators #

This file adds norm_num plugins for Finset.prod and Finset.sum.

The driving part of this plugin is Mathlib.Meta.NormNum.evalFinsetBigop. We repeatedly use Finset.proveEmptyOrCons to try to find a proof that the given set is empty, or that it consists of one element inserted into a strict subset, and evaluate the big operator on that subset until the set is completely exhausted.

See also #

Porting notes #

This plugin is noticeably less powerful than the equivalent version in Mathlib 3: the design of norm_num means plugins have to return numerals, rather than a generic expression. In particular, we can't use the plugin on sums containing variables. (See also the TODO note "To support variables".)

TODO #

This represents the result of trying to determine whether the given expression n : Q(ℕ) is either zero or succ.

Instances For

    Determine whether the expression n : Q(ℕ) unifies with 0 or Nat.succ n'.

    We do not use norm_num functionality because we want definitional equality, not propositional equality, for use in dependent types.

    Fails if neither of the options succeed.

    Equations
      Instances For
        inductive Mathlib.Meta.List.ProveNilOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(List «$α»)) :

        This represents the result of trying to determine whether the given expression s : Q(List $α) is either empty or consists of an element inserted into a strict subset.

        Instances For
          def Mathlib.Meta.List.ProveNilOrConsResult.uncheckedCast {u v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (s : Q(List «$α»)) (t : Q(List «$β»)) :

          If s unifies with t, convert a result for s to a result for t.

          If s does not unify with t, this results in a type-incorrect proof.

          Equations
            Instances For
              def Mathlib.Meta.List.ProveNilOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s t : Q(List «$α»)} (eq : Q(«$s» = «$t»)) :

              If s = t and we can get the result for t, then we can get the result for s.

              Equations
                Instances For
                  partial def Mathlib.Meta.List.proveNilOrCons {u : Lean.Level} {α : Q(Type u)} (s : Q(List «$α»)) :

                  Either show the expression s : Q(List α) is Nil, or remove one element from it.

                  Fails if we cannot determine which of the alternatives apply to the expression.

                  inductive Mathlib.Meta.Multiset.ProveZeroOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(Multiset «$α»)) :

                  This represents the result of trying to determine whether the given expression s : Q(Multiset $α) is either empty or consists of an element inserted into a strict subset.

                  Instances For

                    If s unifies with t, convert a result for s to a result for t.

                    If s does not unify with t, this results in a type-incorrect proof.

                    Equations
                      Instances For
                        def Mathlib.Meta.Multiset.ProveZeroOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s t : Q(Multiset «$α»)} (eq : Q(«$s» = «$t»)) :

                        If s = t and we can get the result for t, then we can get the result for s.

                        Equations
                          Instances For
                            theorem Mathlib.Meta.Multiset.insert_eq_cons {α : Type u_1} (a : α) (s : Multiset α) :
                            insert a s = a ::ₘ s
                            theorem Mathlib.Meta.Multiset.range_succ' {n nn n' : } (pn : NormNum.IsNat n nn) (pn' : nn = n'.succ) :

                            Either show the expression s : Q(Multiset α) is Zero, or remove one element from it.

                            Fails if we cannot determine which of the alternatives apply to the expression.

                            Equations
                              Instances For
                                inductive Mathlib.Meta.Finset.ProveEmptyOrConsResult {u : Lean.Level} {α : Q(Type u)} (s : Q(Finset «$α»)) :

                                This represents the result of trying to determine whether the given expression s : Q(Finset $α) is either empty or consists of an element inserted into a strict subset.

                                Instances For

                                  If s unifies with t, convert a result for s to a result for t.

                                  If s does not unify with t, this results in a type-incorrect proof.

                                  Equations
                                    Instances For
                                      def Mathlib.Meta.Finset.ProveEmptyOrConsResult.eq_trans {u : Lean.Level} {α : Q(Type u)} {s t : Q(Finset «$α»)} (eq : Q(«$s» = «$t»)) :

                                      If s = t and we can get the result for t, then we can get the result for s.

                                      Equations
                                        Instances For
                                          theorem Mathlib.Meta.Finset.insert_eq_cons {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) (h : as) :
                                          insert a s = Finset.cons a s h
                                          theorem Mathlib.Meta.Finset.range_succ' {n nn n' : } (pn : NormNum.IsNat n nn) (pn' : nn = n'.succ) :
                                          theorem Mathlib.Meta.Finset.univ_eq_elems {α : Type u_1} [Fintype α] (elems : Finset α) (complete : ∀ (x : α), x elems) :

                                          Either show the expression s : Q(Finset α) is empty, or remove one element from it.

                                          Fails if we cannot determine which of the alternatives apply to the expression.

                                          def Mathlib.Meta.NormNum.Result.eq_trans {u : Lean.Level} {α : Q(Type u)} {a b : Q(«$α»)} (eq : Q(«$a» = «$b»)) :
                                          Result bResult a

                                          If a = b and we can evaluate b, then we can evaluate a.

                                          Equations
                                            Instances For
                                              theorem Mathlib.Meta.NormNum.Finset.sum_empty {β : Type u_1} {α : Type u_2} [CommSemiring β] (f : αβ) :
                                              IsNat (.sum f) 0
                                              theorem Mathlib.Meta.NormNum.Finset.prod_empty {β : Type u_1} {α : Type u_2} [CommSemiring β] (f : αβ) :
                                              IsNat (.prod f) 1
                                              partial def Mathlib.Meta.NormNum.evalFinsetBigop {u v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (op : Q(Finset «$α»(«$α»«$β»)«$β»)) (f : Q(«$α»«$β»)) (res_empty : Result q(«$op» Finset.empty «$f»)) (res_cons : {a : Q(«$α»)} → {s' : Q(Finset «$α»)} → {h : Q(«$a»«$s'»)} → Result q(«$f» «$a»)Result q(«$op» «$s'» «$f»)Lean.MetaM (Result q(«$op» (Finset.cons «$a» «$s'» «$h») «$f»))) (s : Q(Finset «$α»)) :
                                              Lean.MetaM (Result q(«$op» «$s» «$f»))

                                              Evaluate a big operator applied to a finset by repeating proveEmptyOrCons until we exhaust all elements of the set.

                                              norm_num plugin for evaluating products of finsets.

                                              If your finset is not supported, you can add it to the match in Finset.proveEmptyOrCons.

                                              Equations
                                                Instances For

                                                  norm_num plugin for evaluating sums of finsets.

                                                  If your finset is not supported, you can add it to the match in Finset.proveEmptyOrCons.

                                                  Equations
                                                    Instances For