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 : Type

The configuration for the congr! tactic.

• 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.

• transparency : Lean.Meta.TransparencyMode

  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 ℕ

  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.

• beqEq : Bool

  Whether to use a special congruence lemma for BEq instances. This synthesizes LawfulBEq instances to discharge equalities of BEq instances.

def Congr!.Config.unfoldSameFun : Congr!.Config

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.

Equations

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

def Congr!.Config.numArgsOk (config : Congr!.Config) (numArgs : ℕ) : Bool

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

Equations

• config.numArgsOk numArgs = decide (numArgs ≤ config.maxArgs.getD numArgs)

def Congr!.Config.maxArgsFor (config : Congr!.Config) (numArgs : ℕ) : ℕ

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

Equations

• config.maxArgsFor numArgs = min numArgs (config.maxArgs.getD numArgs)

def Congr!.plausiblyEqualTypes (ty1 ty2 : Lean.Expr) (maxDepth : ℕ := 5) : Lean.MetaM Bool

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".

Equations

• One or more equations did not get rendered due to their size.
• Congr!.plausiblyEqualTypes ty1 ty2 0 = pure false

def Lean.MVarId.smartHCongr? (config : Congr!.Config) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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.

Equations

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

partial def Lean.MVarId.smartHCongr?.loop (config : Congr!.Config) (mvarId : Lean.MVarId) (numArgs : ℕ) (lhs rhs : Lean.Expr) (lhsArgs rhsArgs : List Lean.Expr) : Lean.MetaM (Option (List Lean.MVarId))

def Lean.MVarId.smartHCongr?.forSide (config : Congr!.Config) (mvarId : Lean.MVarId) (side : Lean.Expr) : Lean.MetaM (Option (List Lean.MVarId))

Equations

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

def Lean.MVarId.congrSimp? (config : Congr!.Config) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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.

Equations

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

def Lean.MVarId.congrSimp?.forSide (config : Congr!.Config) (mvarId : Lean.MVarId) (side : Lean.Expr) : Lean.MetaM (Option (List Lean.MVarId))

Equations

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

def Lean.MVarId.congrSimp?.mkCongrSimpNArgs (f : Lean.Expr) (nArgs : ℕ) : Lean.MetaM (Option Lean.Meta.CongrTheorem)

Like mkCongrSimp? but takes in a specific arity.

Equations

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

def Lean.MVarId.userCongr? (config : Congr!.Config) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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.

Equations

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

def Lean.MVarId.userCongr?.forSide (config : Congr!.Config) (mvarId : Lean.MVarId) (side : Lean.Expr) : Lean.MetaM (Option (List Lean.MVarId))

Equations

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

def Lean.MVarId.congrPi? (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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

Equations

• mvarId.congrPi? = Lean.observing? do let __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels `pi_congr Lean.Meta.withReducible (mvarId.apply __do_lift)

def Lean.MVarId.obviousFunext? (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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.

Equations

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

def Lean.MVarId.obviousHfunext? (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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.

Equations

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

def Lean.MVarId.congrImplies?' (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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

Equations

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

theorem FastSubsingleton.helim {α β : Sort u} [Lean.Meta.FastSubsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b

def Lean.MVarId.subsingletonHelim? (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

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 α = β.

Equations

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

def Lean.MVarId.beqInst? (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Tries to apply lawful_beq_subsingleton to prove that two BEq instances are equal by synthesizing LawfulBEq instances for both.

Equations

• mvarId.beqInst? = Lean.observing? (Lean.Meta.withReducible (mvarId.applyConst `lawful_beq_subsingleton))

def Lean.MVarId.congrPasses! : List (String × (Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))))

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

Equations

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

def Lean.MVarId.congrPasses!.when (b : Congr!.Config → Bool) (f : Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) (config : Congr!.Config) (mvar : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Conditionally runs a congruence strategy depending on the predicate b applied to the config.

Equations

• Lean.MVarId.congrPasses!.when b f config mvar = if b config = true then do let y ← pure PUnit.unit (fun (y : PUnit.{1}) => f config mvar) y else pure none

structure CongrState : Type

• goals : Array Lean.MVarId

  Accumulated goals that congr! could not handle.

• patterns : List (Lean.TSyntax `rcasesPat)

  Patterns to use when doing intro.

@[reducible, inline]

abbrev CongrMetaM (α : Type) : Type

Equations

• CongrMetaM = StateRefT' IO.RealWorld CongrState Lean.MetaM

def CongrMetaM.nextPattern : CongrMetaM (Option (Lean.TSyntax `rcasesPat))

Pop the next pattern from the current state.

Equations

• CongrMetaM.nextPattern = modifyGet fun (s : CongrState) => match s.patterns with | p :: ps => (some p, { goals := s.goals, patterns := ps }) | x => (none, s)

def Lean.MVarId.introsClean (mvarId : Lean.MVarId) : CongrMetaM (List Lean.MVarId)

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 Lean.Elab..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.

Equations

• mvarId.introsClean = Lean.MVarId.introsClean.loop mvarId

def Lean.MVarId.introsClean.heqImpOfEqImp (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

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

def Lean.MVarId.introsClean.eqImpOfIffImp (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

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

partial def Lean.MVarId.introsClean.loop (mvarId : Lean.MVarId) : CongrMetaM (List Lean.MVarId)

def Lean.MVarId.introsClean.isTrivialType (ty : Lean.Expr) : Lean.MetaM Bool

Equations

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

def Lean.MVarId.preCongr! (mvarId : Lean.MVarId) (tryClose : Bool) : Lean.MetaM (Option Lean.MVarId)

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.

Equations

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

def Lean.MVarId.congrCore! (config : Congr!.Config) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Equations

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

def Lean.MVarId.postCongr! (config : Congr!.Config) (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

A pass to clean up after Lean.MVarId.preCongr! and Lean.MVarId.congrCore!.

Equations

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

def Lean.MVarId.congrN! (mvarId : Lean.MVarId) (depth? : Option ℕ := none) (config : 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, beqEq := true }) (patterns : List (Lean.TSyntax `rcasesPat) := []) : Lean.MetaM (List Lean.MVarId)

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.

Equations

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

def Lean.MVarId.congrN!.post (config : 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, beqEq := true }) (mvarId : Lean.MVarId) : CongrMetaM Unit

Equations

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

def Lean.MVarId.congrN!.go (config : 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, beqEq := true }) (depth n : ℕ) (mvarId : Lean.MVarId) : CongrMetaM Unit

Equations

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

def Congr!.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Congr!.Config

Equations

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

def Congr!.congr! : Lean.ParserDescr

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.

Syntax:

congr!
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 ⊢ List.map f xs = List.map 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.

Equations

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