Documentation

Mathlib.Tactic.ProdAssoc

Associativity of products #

This file constructs a term elaborator for "obvious" equivalences between iterated products. For example,

(prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ)

gives the "obvious" equivalence between (α × β) × (γ × δ) and α × (β × γ) × δ.

A helper type to keep track of universe levels and types in iterated produts.

Instances For

    The iterated product corresponding to a ProdTree.

    Equations
    Instances For

      The number of types appearing in an iterated product encoded as a ProdTree.

      Equations
      Instances For

        The components of an iterated product, presented as a ProdTree.

        Equations
        Instances For

          Given P : ProdTree representing an iterated product and e : Expr which should correspond to a term of the iterated product, this will return a list, whose items correspond to the leaves of P (i.e. the types appearing in the product), where each item is the appropriate composition of Prod.fst and Prod.snd applied to e resulting in an element of the type corresponding to the leaf.

          For example, if P corresponds to (X × Y) × Z and t : (X × Y) × Z, then this should return [t.fst.fst, t.fst.snd, t.snd].

          Equations
          Instances For

            This function should act as the "reverse" of ProdTree.unpack, constructing a term of the iterated product out of a list of terms of the types appearing in the product.

            Equations
            Instances For

              Converts a term e in an iterated product P1 into a term of an iterated product P2. Here e is an Expr representing the term, and the iterated products are represented by terms of ProdTree.

              Equations
              Instances For

                Given two expressions corresponding to iterated products of the same types, associated in possibly different ways, this constructs the "obvious" function from one to the other.

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

                  Construct the equivalence between iterated products of the same type, associated in possibly different ways.

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

                    IMPLEMENTATION: Syntax used in the implementation of prod_assoc%. This elaborator postpones if there are metavariables in the expected type, and to propagate the fact that this elaborator produces an Equiv, the prod_assoc% macro sets things up with a type ascription. This enables using prod_assoc% with, for example Equiv.trans dot notation.

                    Equations
                    Instances For

                      Elaborator for prod_assoc%.

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

                        prod_assoc% elaborates to the "obvious" equivalence between iterated products of types, regardless of how the products are parenthesized. The prod_assoc% term uses the expected type when elaborating. For example, (prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ).

                        The elaborator can handle holes in the expected type, so long as they eventually get filled by unification.

                        example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ :=
                          (prod_assoc% : _ ≃ α × β × γ × δ).trans prod_assoc%
                        
                        Equations
                        Instances For