Documentation

Mathlib.Tactic.NormNum.Core

norm_num core functionality #

This file sets up the norm_num tactic and the @[norm_num] attribute, which allow for plugging in new normalization functionality around a simp-based driver. The actual behavior is in @[norm_num]-tagged definitions in Tactic.NormNum.Basic and elsewhere.

Attribute for identifying norm_num extensions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    An extension for norm_num.

    Instances For

      Read a norm_num extension from a declaration of the right type.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]

        Each norm_num extension is labelled with a collection of patterns which determine the expressions to which it should be applied.

        Equations
        Instances For

          The state of the norm_num extension environment

          Instances For

            Configuration for DiscrTree.

            Equations
            Instances For

              Run each registered norm_num extension on an expression, returning a NormNum.Result.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Mathlib.Meta.NormNum.deriveNat {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (_inst : autoParam Q(AddMonoidWithOne «$α») _auto✝) :
                Lean.MetaM ((lit : Q()) × Q(Mathlib.Meta.NormNum.IsNat «$e» «$lit»))

                Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℕ, and a proof of isNat e lit.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Mathlib.Meta.NormNum.deriveInt {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (_inst : autoParam Q(Ring «$α») _auto✝) :
                  Lean.MetaM ((lit : Q()) × Q(Mathlib.Meta.NormNum.IsInt «$e» «$lit»))

                  Run each registered norm_num extension on a typed expression e : α, returning a typed expression lit : ℤ, and a proof of IsInt e lit in expression form.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Mathlib.Meta.NormNum.deriveRat {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (_inst : autoParam Q(DivisionRing «$α») _auto✝) :
                    Lean.MetaM ( × (n : Q()) × (d : Q()) × Q(Mathlib.Meta.NormNum.IsRat «$e» «$n» «$d»))

                    Run each registered norm_num extension on a typed expression e : α, returning a rational number, typed expressions n : ℤ and d : ℕ for the numerator and denominator, and a proof of IsRat e n d in expression form.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Run each registered norm_num extension on a typed expression p : Prop, and returning the truth or falsity of p' : Prop from an equivalence p ↔ p'.

                      Equations
                      Instances For
                        def Mathlib.Meta.NormNum.deriveBoolOfIff (p : Q(Prop)) (p' : Q(Prop)) (hp : Q(«$p» «$p'»)) :

                        Run each registered norm_num extension on a typed expression p : Prop, and returning the truth or falsity of p' : Prop from an equivalence p ↔ p'.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Run each registered norm_num extension on an expression, returning a Simp.Result.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Erases a name marked norm_num by adding it to the state's erased field and removing it from the state's list of Entrys.

                            Equations
                            Instances For

                              Erase a name marked as a norm_num attribute.

                              Check that it does in fact have the norm_num attribute by making sure it names a NormNumExt found somewhere in the state's tree, and is not erased.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                A simp plugin which calls NormNum.eval.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  A Methods implementation which calls norm_num.

                                  Traverses the given expression using simp and normalises any numbers it finds.

                                  The core of norm_num as a tactic in MetaM.

                                  • g: The goal to simplify
                                  • ctx: The simp context, constructed by mkSimpContext and containing any additional simp rules we want to use
                                  • fvarIdsToSimp: The selected set of hypotheses used in the location argument
                                  • simplifyTarget: true if the target is selected in the location argument
                                  • useSimp: true if we used norm_num instead of norm_num1
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Constructs a simp context from the simp argument syntax.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Elaborates a call to norm_num only? [args] or norm_num1.

                                      • args: the (simpArgs)? syntax for simp arguments
                                      • loc: the (location)? syntax for the optional location argument
                                      • simpOnly: true if only was used in norm_num
                                      • useSimp: false if norm_num1 was used, in which case only the structural parts of simp will be used, not any of the post-processing that simp only does without lemmas
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as , , , , and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Basic version of norm_num that does not call simp.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Basic version of norm_num that does not call simp.

                                            Equations
                                            Instances For

                                              Elaborator for norm_num1 conv tactic.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as , , , , and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Elaborator for norm_num conv tactic.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    The basic usage is #norm_num e, where e is an expression, which will print the norm_num form of e.

                                                    Syntax: #norm_num (only)? ([ simp lemma list ])? :? expression

                                                    This accepts the same options as the #simp command. You can specify additional simp lemmas as usual, for example using #norm_num [f, g] : e. (The colon is optional but helpful for the parser.) The only restricts norm_num to using only the provided lemmas, and so #norm_num only : e behaves similarly to norm_num1.

                                                    Unlike norm_num, this command does not fail when no simplifications are made.

                                                    #norm_num understands local variables, so you can use them to introduce parameters.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For