The congr! tactic #

This is a more powerful version of the congr tactic that knows about more congruence lemmas and can apply to more situations. It is similar to the congr' tactic from Mathlib 3.

The congr! tactic is used by the convert and convert_to tactics.

See the syntax docstring for more details.

structure Congr!.Config :
  • closePre : Bool

    If closePre := true, then try to close goals before applying congruence lemmas using tactics such as rfl and assumption. These tactics are applied with the transparency level specified by preTransparency, which is .reducible` by default.

  • closePost : Bool

    If closePost := true, then try to close goals that remain after no more congruence lemmas can be applied, using the same tactics as closePre. These tactics are applied with current tactic transparency level.

  • The transparency level to use when applying a congruence theorem. By default this is .reducible, which prevents unfolding of most definitions.

  • preTransparency : Lean.Meta.TransparencyMode

    The transparency level to use when trying to close goals before applying congruence lemmas. This includes trying to prove the goal by rfl and using the assumption tactic. By default this is .reducible, which prevents unfolding of most definitions.

  • preferLHS : Bool

    For passes that synthesize a congruence lemma using one side of the equality, we run the pass both for the left-hand side and the right-hand side. If preferLHS is true then we start with the left-hand side.

    This can be used to control which side's definitions are expanded when applying the congruence lemma (if preferLHS = true then the RHS can be expanded).

  • partialApp : Bool

    Allow both sides to be partial applications. When false, given an equality f a b = g x y z this means we never consider proving f a = g x y.

    In this case, we might still consider f = g x if a pass generates a congruence lemma using the left-hand side. Use sameFun := true to ensure both sides are applications of the same function (making it be similar to the congr tactic).

  • sameFun : Bool

    Whether to require that both sides of an equality be applications of defeq functions. That is, if true, f a = g x is only considered if f and g are defeq (making it be similar to the congr tactic).

  • maxArgs : Option Nat

    The maximum number of arguments to consider when doing congruence of function applications. For example, with f a b c = g w x y z, setting maxArgs := some 2 means it will only consider either f a b = g w x y and c = z or f a = g w x, b = y, and c = z. Setting maxArgs := none (the default) means no limit.

    When the functions are dependent, maxArgs can prevent congruence from working at all. In Fintype.card α = Fintype.card β, one needs to have maxArgs at 2 or higher since there is a Fintype instance argument that depends on the first.

    When there aren't such dependency issues, setting maxArgs := some 1 causes congr! to do congruence on a single argument at a time. This can be used in conjunction with the iteration limit to control exactly how many arguments are to be processed by congruence.

  • typeEqs : Bool

    For type arguments that are implicit or have forward dependencies, whether or not congr! should generate equalities even if the types do not look plausibly equal.

    We have a heuristic in the main congruence generator that types α and β are plausibly equal according to the following algorithm:

    • If the types are both propositions, they are plausibly equal (Iffs are plausible).
    • If the types are from different universes, they are not plausibly equal.
    • Suppose in whnf we have α = f a₁ ... aₘ and β = g b₁ ... bₘ. If f is not definitionally equal to g or m ≠ n, then α and β are not plausibly equal.
    • If there is some i such that aᵢ and bᵢ are not plausibly equal, then α and β are not plausibly equal.
    • Otherwise, α and β are plausibly equal.

    The purpose of this is to prevent considering equalities like ℕ = ℤ while allowing equalities such as Fin n = Fin m or Subtype p = Subtype q (so long as these are subtypes of the same type).

    The way this is implemented is that when the congruence generator is comparing arguments when looking at an equality of function applications, it marks a function parameter as "fixed" if the provided arguments are types that are not plausibly equal. The effect of this is that congruence succeeds only if those arguments are defeq at transparency transparency.

  • etaExpand : Bool

    As a last pass, perform eta expansion of both sides of an equality. For example, this transforms a bare HAdd.hAdd into fun x y => x + y.

  • useCongrSimp : Bool

    Whether to use the congruence generator that is used by simp and congr. This generator is more strict, and it does not respect all configuration settings. It does respect preferLHS, partialApp and maxArgs and transparency settings. It acts as if sameFun := true and it ignores typeEqs.

The configuration for the congr! tactic.

Instances For

    A configuration option that makes congr! do the sorts of aggressive unfoldings that congr does while also similarly preventing congr! from considering partial applications or congruences between different functions being applied.

    Instances For
      def Congr!.Config.numArgsOk (config : Congr!.Config) (numArgs : Nat) :

      Whether the given number of arguments is allowed to be considered.

      Instances For
        def Congr!.Config.maxArgsFor (config : Congr!.Config) (numArgs : Nat) :

        According to the configuration, how many of the arguments in numArgs should be considered.

        Instances For

          Returns whether or not it's reasonable to consider an equality between types ty1 and ty2. The heuristic is the following:

          • If ty1 and ty2 are in Prop, then yes.
          • If in whnf both ty1 and ty2 have the same head and if (recursively) it's reasonable to consider an equality between corresponding type arguments, then yes.
          • Otherwise, no.

          This helps keep congr from going too far and generating hypotheses like ℝ = ℤ.

          To keep things from going out of control, there is a maxDepth. Additionally, if we do the check with maxDepth = 0 then the heuristic answers "no".

          Instances For

            This is like Lean.MVarId.hcongr? but (1) looks at both sides when generating the congruence lemma and (2) inserts additional hypotheses from equalities from previous arguments.

            It uses Lean.Meta.mkRichHCongr to generate the congruence lemmas.

            If the goal is an Eq, it uses eq_of_heq first.

            As a backup strategy, it uses the LHS/RHS method like in Lean.MVarId.congrSimp? (where Congr!.Config.preferLHS determines which side to try first). This uses a particular side of the target, generates the congruence lemma, then tries applying it. This can make progress with higher transparency settings. To help the unifier, in this mode it assumes both sides have the exact same function.

            Instances For
              partial def Lean.MVarId.smartHCongr?.loop (config : Congr!.Config) (mvarId : Lean.MVarId) (numArgs : Nat) (lhs : Lean.Expr) (rhs : Lean.Expr) (lhsArgs : List Lean.Expr) (rhsArgs : List Lean.Expr) :

              Like Lean.MVarId.congr? but instead of using only the congruence lemma associated to the LHS, it tries the RHS too, in the order specified by config.preferLHS.

              It uses Lean.Meta.mkCongrSimp? to generate a congruence lemma, like in the congr tactic.

              Applies the congruence generated congruence lemmas according to config.

              Instances For

                Like mkCongrSimp? but takes in a specific arity.

                Instances For

                  Try applying user-provided congruence lemmas. If any are applicable, returns a list of new goals.

                  Tries a congruence lemma associated to the LHS and then, if that failed, the RHS.

                  Instances For

                    Try to apply pi_congr. This is similar to Lean.MVar.congrImplies?.

                    Instances For

                      Try to apply funext, but only if it is an equality of two functions where at least one is a lambda expression.

                      One thing this check prevents is accidentally applying funext to a set equality, but also when doing congruence we don't want to apply funext unnecessarily.

                      Instances For

                        Try to apply Function.hfunext, returning the new goals if it succeeds. Like Lean.MVarId.obviousFunext?, we only do so if at least one side of the HEq is a lambda. This prevents unfolding of things like Set.

                        Need to have Mathlib.Logic.Function.Basic imported for this to succeed.

                        Instances For

                          A version of Lean.MVarId.congrImplies? that uses implies_congr' instead of implies_congr.

                          Instances For

                            Try to apply Subsingleton.helim if the goal is a HEq. Tries synthesizing a Subsingleton instance for both the LHS and the RHS.

                            If successful, this reduces proving @HEq α x β y to proving α = β.

                            Instances For

                              A list of all the congruence strategies used by Lean.MVarId.congrCore!.

                              Instances For
                                structure CongrState :
                                Instances For
                                  @[inline, reducible]
                                  abbrev CongrMetaM (α : Type) :
                                  Instances For

                                    Pop the next pattern from the current state.

                                    Instances For

                                      Does Lean.MVarId.intros but then cleans up the introduced hypotheses, removing anything that is trivial. If there are any patterns in the current CongrMetaM state then instead of Lean.MVarId.intros it does Std.Tactic.RCases.rintro.

                                      Cleaning up includes:

                                      • deleting hypotheses of the form HEq x x, x = x, and x ↔ x.
                                      • deleting Prop hypotheses that are already in the local context.
                                      • converting HEq x y to x = y if possible.
                                      • converting x = y to x ↔ y if possible.
                                      Instances For

                                        Convert a goal into an Eq goal if possible (since we have a better shot at those). Also, if tryClose := true, then try to close the goal using an assumption, Subsingleton.Elim, or definitional equality.

                                        Instances For
                                          def Lean.MVarId.congrN! (mvarId : Lean.MVarId) (depth? : optParam (Option Nat) none) (config : optParam Congr!.Config { closePre := true, closePost := true, transparency := Lean.Meta.TransparencyMode.reducible, preTransparency := Lean.Meta.TransparencyMode.reducible, preferLHS := true, partialApp := true, sameFun := false, maxArgs := none, typeEqs := false, etaExpand := false, useCongrSimp := false }) (patterns : optParam (List (Lean.TSyntax `rcasesPat)) []) :

                                          A more insistent version of Lean.MVarId.congrN. See the documentation on the congr! syntax.

                                          The depth? argument controls the depth of the recursion. If none, then it uses a reasonably large bound that is linear in the expression depth.

                                          Instances For
                                            def Lean.MVarId.congrN!.post (config : optParam Congr!.Config { closePre := true, closePost := true, transparency := Lean.Meta.TransparencyMode.reducible, preTransparency := Lean.Meta.TransparencyMode.reducible, preferLHS := true, partialApp := true, sameFun := false, maxArgs := none, typeEqs := false, etaExpand := false, useCongrSimp := false }) (mvarId : Lean.MVarId) :
                                            Instances For
                                              def Lean.MVarId.congrN!.go (config : optParam Congr!.Config { closePre := true, closePost := true, transparency := Lean.Meta.TransparencyMode.reducible, preTransparency := Lean.Meta.TransparencyMode.reducible, preferLHS := true, partialApp := true, sameFun := false, maxArgs := none, typeEqs := false, etaExpand := false, useCongrSimp := false }) (depth : Nat) (n : Nat) (mvarId : Lean.MVarId) :
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Equates pieces of the left-hand side of a goal to corresponding pieces of the right-hand side by recursively applying congruence lemmas. For example, with ⊢ f as = g bs we could get two goals ⊢ f = g and ⊢ as = bs.


                                                congr! n
                                                congr! with x y z
                                                congr! n with x y z

                                                Here, n is a natural number and x, y, z are rintro patterns (like h, rfl, ⟨x, y⟩, _, -, (h | h), etc.).

                                                The congr! tactic is similar to congr but is more insistent in trying to equate left-hand sides to right-hand sides of goals. Here is a list of things it can try:

                                                • If R in ⊢ R x y is a reflexive relation, it will convert the goal to ⊢ x = y if possible. The list of reflexive relations is maintained using the @[refl] attribute. As a special case, ⊢ p ↔ q is converted to ⊢ p = q during congruence processing and then returned to ⊢ p ↔ q form at the end.

                                                • If there is a user congruence lemma associated to the goal (for instance, a @[congr]-tagged lemma applying to f xs = g ys), then it will use that.

                                                • It uses a congruence lemma generator at least as capable as the one used by congr and simp. If there is a subexpression that can be rewritten by simp, then congr! should be able to generate an equality for it.

                                                • It can do congruences of pi types using lemmas like implies_congr and pi_congr.

                                                • Before applying congruences, it will run the intros tactic automatically. The introduced variables can be given names using a with clause. This helps when congruence lemmas provide additional assumptions in hypotheses.

                                                • When there is an equality between functions, so long as at least one is obviously a lambda, we apply funext or Function.hfunext, which allows for congruence of lambda bodies.

                                                • It can try to close goals using a few strategies, including checking definitional equality, trying to apply Subsingleton.elim or proof_irrel_heq, and using the assumption tactic.

                                                The optional parameter is the depth of the recursive applications. This is useful when congr! is too aggressive in breaking down the goal. For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr! produces the goals ⊢ x = y and ⊢ y = x, while congr! 2 produces the intended ⊢ x + y = y + x.

                                                The congr! tactic also takes a configuration option, for example

                                                congr! (config := {transparency := .default}) 2

                                                This overrides the default, which is to apply congruence lemmas at reducible transparency.

                                                The congr! tactic is aggressive with equating two sides of everything. There is a predefined configuration that uses a different strategy: Try

                                                congr! (config := .unfoldSameFun)

                                                This only allows congruences between functions applications of definitionally equal functions, and it applies congruence lemmas at default transparency (rather than just reducible). This is somewhat like congr.

                                                See Congr!.Config for all options.

                                                Instances For