Documentation

Mathlib.Tactic.Attr.Register

Attributes used in Mathlib #

In this file we define all simp-like and label-like attributes used in Mathlib. We declare all of them in one file for two reasons:

Simplification procedure

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

    Simp set for functor_norm

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

      Simp set for functor_norm

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

        Simplification procedure

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

          Simplification procedure

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

            The simpset field_simps is used by the tactic field_simp to reduce an expression in a field to an expression of the form n / d where n and d are division-free.

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

              Simplification procedure

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

                Simp attribute for lemmas about Even

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

                  Simplification procedure

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

                    "Simp attribute for lemmas about RCLike"

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

                      Simplification procedure

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

                        The simpset rify_simps is used by the tactic rify to move expressions from , , or to .

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

                          The simpset qify_simps is used by the tactic qify to move expressions from or to which gives a well-behaved division.

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

                            Simplification procedure

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

                              The simpset zify_simps is used by the tactic zify to move expressions from to which gives a well-behaved subtraction.

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

                                Simplification procedure

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

                                  Simplification procedure

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

                                    The simpset mfld_simps records several simp lemmas that are especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it possible to have quicker proofs (when used with squeeze_simp or simp only) while retaining readability.

                                    The typical use case is the following, in a file on manifolds: If simp [foo, bar] is slow, replace it with squeeze_simp [foo, bar, mfld_simps] and paste its output. The list of lemmas should be reasonable (contrary to the output of squeeze_simp [foo, bar] which might contain tens of lemmas), and the outcome should be quick enough.

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

                                      Simp set for integral rules.

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

                                        Simplification procedure

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

                                          Simplification procedure

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

                                            simp set for the manipulation of typevec and arrow expressions

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

                                              Simplification rules for ghost equations.

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

                                                Simplification procedure

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

                                                  Simplification procedure

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

                                                    The @[nontriviality] simp set is used by the nontriviality tactic to automatically discharge theorems about the trivial case (where we know Subsingleton α and many theorems in e.g. groups are trivially true).

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

                                                      A stub attribute for is_poly.

                                                      Equations
                                                      Instances For

                                                        A simp set for the fin_omega wrapper around omega.

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

                                                          Simplification procedure

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

                                                            Simplification procedure

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

                                                              A simp set for simplifying expressions involving in enat_to_nat.

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

                                                                A simp set for pushing coercions from to ℕ∞ in enat_to_nat.

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

                                                                  Simplification procedure

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

                                                                    A simp set for the pnat_to_nat tactic.

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

                                                                      Simplification procedure

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

                                                                        Simplification procedure

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

                                                                          mon_tauto is a simp set to prove tautologies about morphisms from some (tensor) power of M to M, where M is a (commutative) monoid object in a (braided) monoidal category.

                                                                          This simp set is incompatible with the standard simp set. If you want to use it, make sure to add the following to your simp call to disable the problematic default simp lemmas:

                                                                          -MonoidalCategory.whiskerLeft_id, -MonoidalCategory.id_whiskerRight,
                                                                          -MonoidalCategory.tensor_comp, -MonoidalCategory.tensor_comp_assoc,
                                                                          -MonObj.mul_assoc, -MonObj.mul_assoc_assoc
                                                                          

                                                                          The general algorithm it follows is to push the associators α_ and commutators β_ inwards until they cancel against the right sequence of multiplications.

                                                                          This approach is justified by the fact that a tautology in the language of (commutative) monoid objects "remembers" how it was proved: Every use of a (commutative) monoid object axiom inserts a unitor, associator or commutator, and proving a tautology simply amounts to undoing those moves as prescribed by the presence of unitors, associators and commutators in its expression.

                                                                          This simp set is opiniated about its normal form, which is why it cannot be used concurrently with some of the simp lemmas in the standard simp set:

                                                                          • It eliminates all mentions of whiskers by rewriting them to tensored homs, which goes against whiskerLeft_id and id_whiskerRight: X ◁ f = 𝟙 X ⊗ₘ f, f ▷ X = 𝟙 X ⊗ₘ f. This goes against whiskerLeft_id and id_whiskerRight in the standard simp set.
                                                                          • It collapses compositions of tensored homs to the tensored hom of the compositions, which goes against tensor_comp: (f₁ ⊗ₘ g₁) ≫ (f₂ ⊗ₘ g₂) = (f₁ ≫ f₂) ⊗ₘ (g₁ ≫ g₂). TODO: Isn't this direction Just Better?
                                                                          • It cancels the associators against multiplications, which goes against mul_assoc: (α_ M M M).hom ≫ (𝟙 M ⊗ₘ μ) ≫ μ = (μ ⊗ₘ 𝟙 M) ≫ μ, (α_ M M M).inv ≫ (μ ⊗ₘ 𝟙 M) ≫ μ = (𝟙 M ⊗ₘ μ) ≫ μ
                                                                          • It unfolds non-primitive coherence isomorphisms, like the tensor strengths tensorμ, tensorδ.
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For