Documentation

Mathlib.Tactic.TermCongr

congr(...) congruence quotations #

This module defines a term elaborator for generating congruence lemmas from patterns written using quotation syntax. One can write congr($hf $hx) with hf : f = f' and hx : x = x' to get f x = f' x'. While in simple cases it might be possible to use congr_arg or congr_fun, congruence quotations are more general, since for example f could have implicit arguments, complicated dependent types, and subsingleton instance arguments such as Decidable or Fintype.

The implementation strategy is the following:

  1. The pattern is elaborated twice, once with each hole replaced by the LHS and again with each hole replaced by the RHS. We do not force the hole to have any particular type while elaborating, but if the hole has a type with an obvious LHS or RHS, then we propagate this information outward. We use Mathlib.Tactic.TermCongr.cHole with metadata for these replacements to hold onto the hole itself.
  2. Once the pattern has been elaborated twice, we unify them against the respective LHS and RHS of the target type if the target has a type with an obvious LHS and RHS. This can fill in some metavariables and help typeclass inference make progress.
  3. Then we simultaneously walk along the elaborated LHS and RHS expressions to generate a congruence. When we reach cHoles, we make sure they elaborated in a compatible way. Each Expr type has some logic to come up with a suitable congruence. For applications we use a version of Lean.Meta.mkHCongrWithArity that tries to fill in some of the equality proofs using subsingleton lemmas.

The point of elaborating the expression twice is that we let the elaborator handle activities like synthesizing instances, etc., specialized to LHS or RHS, without trying to derive one side from the other.

During development there was a version using simp transformations, but there was no way to inform simp about the expected RHS, which could cause simp to fail because it eagerly wants to solve for instance arguments. The current version is able to use the expected LHS and RHS to fill in arguments before solving for instance arguments.

congr(expr) generates an congruence from an expression containing congruence holes of the form $h or $(h). In these congruence holes, h : a = b indicates that, in the generated congruence, on the left-hand side a is substituted for $h and on the right-hand side b is substituted for $h.

For example, if h : a = b then congr(1 + $h) : 1 + a = 1 + b.

This is able to make use of the expected type, for example (congr(_ + $h) : 1 + _ = _) with h : x = y gives 1 + x = 1 + y. The expected type can be an Iff, Eq, or HEq. If there is no expected type, then it generates an equality.

Note: the process of generating a congruence lemma involves elaborating the pattern using terms with attached metadata and a reducible wrapper. We try to avoid doing so, but these terms can leak into the local context through unification. This can potentially break tactics that are sensitive to metadata or reducible functions. Please report anything that goes wrong with congr(...) lemmas on Zulip.

For debugging, you can set set_option trace.Elab.congr true.

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

    Congruence holes #

    This section sets up the way congruence holes are elaborated for congr(...) quotations. The basic problem is that if we have $h with h : x = y, we need to elaborate it once as x and once as y, and in both cases the term needs to remember that it's associated to h.

    @[reducible]
    def Mathlib.Tactic.TermCongr.cHole {α : Sort u} (val : α) {p : Prop} (_pf : p) :
    α

    For holding onto the hole's value along with the value of either the LHS or RHS of the hole. These occur wrapped in metadata so that they always appear as function application with exactly four arguments.

    Note that there is no relation between val and the proof. We need to decouple these to support letting the proof's elaboration be deferred until we know whether we want an iff, eq, or heq, while also allowing it to choose to elaborate as an iff, eq, or heq. Later, the congruence generator handles any discrepancies. See Mathlib.Tactic.TermCongr.CongrResult.

    Equations
    • val = val
    Instances For

      For error reporting purposes, make the hole pretty print as its value. We can still see that it is a hole in the info view on mouseover.

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

        Create the congruence hole. Used by elabCHole.

        Saves the current mvarCounter as a proxy for age. We use this to avoid reprocessing old congruence holes that happened to leak into the local context.

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

          If the expression is a congruence hole, returns (forLhs, sideVal, pf). If mvarCounterSaved? is not none, then only returns the hole if it is at least as recent.

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

            Returns any subexpression that is a recent congruence hole.

            Equations
            Instances For

              Eliminate all congruence holes from an expression by replacing them with their values.

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

                Elaborates a congruence hole and returns either the left-hand side or the right-hand side, annotated with information necessary to generate a congruence lemma.

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

                  (Internal for congr(...)) Elaborates to an expression satisfying cHole? that equals the LHS or RHS of h, if the LHS or RHS is available after elaborating h. Uses the expected type as a hint.

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

                    (Internal for congr(...)) Elaborates to an expression satisfying cHole? that equals the LHS or RHS of h, if the LHS or RHS is available after elaborating h. Uses the expected type as a hint.

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

                      Replace all term antiquotations in a term using the given expand function.

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

                        Given the pattern t in congr(t), elaborate it for the given side by replacing antiquotations with cHole% terms, and ensure the elaborated term is of the expected type.

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

                          Congruence generation #

                          Ensures the expected type is an equality. Returns the equality. The returned expression satisfies Lean.Expr.eq?.

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

                            Ensures the expected type is a HEq. Returns the HEq. This expression satisfies Lean.Expr.heq?.

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

                              Ensures the expected type is an iff. Returns the iff. This expression satisfies Lean.Expr.iff?.

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

                                Make sure that the expected type of pf is an iff by unification.

                                Equations
                                Instances For

                                  A request for a type of congruence lemma from a CongrResult.

                                  Instances For

                                    A congruence lemma between two expressions. The proof is generated dynamically, depending on whether the resulting lemma should be an Eq or a HEq. If generating a proof impossible, then the generator can throw an error. This can be due to either an Eq proof being impossible or due to the lhs/rhs not being defeq to the lhs/rhs of the generated proof, which can happen for user-supplied congruence holes.

                                    This complexity is to support two features:

                                    1. The user is free to supply Iff, Eq, and HEq lemmas in congurence holes, and we're able to transform them into whatever is appropriate for a given congruence lemma.
                                    2. If the congrence hole is a metavariable, then we can specialize that hole to an Iff, Eq, or HEq depending on what's necessary at that site.
                                    Instances For

                                      Returns whether the proof is by reflexivity. Such congruence proofs are trivial.

                                      Equations
                                      • res.isRfl = res.pf?.isNone
                                      Instances For

                                        Returns the proof that lhs = rhs. Fails if the CongrResult is inapplicable. Throws an error if the lhs and rhs have non-defeq types. If pf? = none, this returns the rfl proof.

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

                                          Returns the proof that HEq lhs rhs. Fails if the CongrResult is inapplicable. If pf? = none, this returns the rfl proof.

                                          Equations
                                          Instances For

                                            Returns a proof of lhsrhs. Uses CongrResult.eq.

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

                                              Combine two congruence proofs using transitivity. Does not check that res1.rhs is defeq to res2.lhs. If both res1 and res2 are trivial then the result is trivial.

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

                                                Make a CongrResult from a LHS, a RHS, and a proof of an Iff, Eq, or HEq. The proof is allowed to have a metavariable for its type. Validates the inputs and throws errors in the pf? function.

                                                The pf? function is responsible for finally unifying the type of pf with lhs and rhs.

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

                                                  Given a pf of an Iff, Eq, or HEq, return a proof of Eq. If pf is not obviously any of these, weakly try inserting propext to make an Iff and otherwise unify the type with Eq.

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

                                                    Given a pf of an Iff, Eq, or HEq, return a proof of HEq. If pf is not obviously any of these, weakly try making it be an Eq or an Iff, and otherwise make it be a HEq.

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

                                                      Get the sides of the type of pf and unify them with the respective lhs and rhs.

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

                                                        Force the lhs and rhs to be defeq. For when dsimp-like congruence is necessary. Clears the proof.

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

                                                          Tries to make a congruence between lhs and rhs automatically.

                                                          1. If they are defeq, returns a trivial congruence.
                                                          2. Tries using Subsingleton.elim.
                                                          3. Tries proof_irrel_heq as another effort to avoid doing congruence on proofs.
                                                          4. Otherwise throws an error.

                                                          Note: mkAppM uses withNewMCtxDepth, which prevents typeclass inference from accidentally specializing Sort _ to Prop, which could otherwise happen because there is a Subsingleton Prop instance.

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

                                                            Does CongrResult.mkDefault but makes sure there are no lingering congruence holes.

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

                                                              Throw an internal error.

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

                                                                If lhs or rhs is a congruence hole, then process it. Only process ones that are at least as new as mvarCounterSaved since nothing prevents congruence holes from leaking into the local context.

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

                                                                  Walks along both lhs and rhs simultaneously to create a congruence lemma between them.

                                                                  Where they are desynchronized, we fall back to the base case (using CongrResult.mkDefault') since it's likely due to unification with the expected type, from _ placeholders or implicit arguments being filled in.

                                                                  Elaborating congruence quotations #

                                                                  congr(expr) generates an congruence from an expression containing congruence holes of the form $h or $(h). In these congruence holes, h : a = b indicates that, in the generated congruence, on the left-hand side a is substituted for $h and on the right-hand side b is substituted for $h.

                                                                  For example, if h : a = b then congr(1 + $h) : 1 + a = 1 + b.

                                                                  This is able to make use of the expected type, for example (congr(_ + $h) : 1 + _ = _) with h : x = y gives 1 + x = 1 + y. The expected type can be an Iff, Eq, or HEq. If there is no expected type, then it generates an equality.

                                                                  Note: the process of generating a congruence lemma involves elaborating the pattern using terms with attached metadata and a reducible wrapper. We try to avoid doing so, but these terms can leak into the local context through unification. This can potentially break tactics that are sensitive to metadata or reducible functions. Please report anything that goes wrong with congr(...) lemmas on Zulip.

                                                                  For debugging, you can set set_option trace.Elab.congr true.

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