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
    • One or more equations did not get rendered due to their size.
    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

        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
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Mathlib.Meta.List.range_succ_eq_map' {n : } {nn : } {n' : } (pn : Mathlib.Meta.NormNum.IsNat n nn) (pn' : nn = n'.succ) :

            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
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                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 : Mathlib.Meta.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
                  • One or more equations did not get rendered due to their size.
                  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
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        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 : Mathlib.Meta.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) :
                          Finset.univ = 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 : Q(«$α»)} {b : Q(«$α»)} (eq : Q(«$a» = «$b»)) :

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem Mathlib.Meta.NormNum.Finset.sum_empty {β : Type u_1} {α : Type u_2} [CommSemiring β] (f : αβ) :
                            theorem Mathlib.Meta.NormNum.Finset.prod_empty {β : Type u_1} {α : Type u_2} [CommSemiring β] (f : αβ) :
                            partial def Mathlib.Meta.NormNum.evalFinsetBigop {u : Lean.Level} {v : Lean.Level} {α : Q(Type u)} {β : Q(Type v)} (op : Q(Finset «$α»(«$α»«$β»)«$β»)) (f : Q(«$α»«$β»)) (res_empty : Mathlib.Meta.NormNum.Result q(«$op» Finset.empty «$f»)) (res_cons : {a : Q(«$α»)} → {s' : Q(Finset «$α»)} → {h : Q(«$a»«$s'»)} → Mathlib.Meta.NormNum.Result q(«$f» «$a»)Mathlib.Meta.NormNum.Result q(«$op» «$s'» «$f»)Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$op» (Finset.cons «$a» «$s'» «$h») «$f»))) (s : Q(Finset «$α»)) :
                            Lean.MetaM (Mathlib.Meta.NormNum.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
                            • One or more equations did not get rendered due to their size.
                            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
                              • One or more equations did not get rendered due to their size.
                              Instances For