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

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
- 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). 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 (
`Iff`

s 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. - If the types are both propositions, they are plausibly equal (
- 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
- beqEq : Bool

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

## Equations

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

## Instances For

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

## Instances For

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

## Equations

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

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

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

Like `mkCongrSimp?`

but takes in a specific arity.

## Equations

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

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

## Equations

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

## Instances For

## Equations

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

## Instances For

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)

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

## Equations

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

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

## Equations

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

## Instances For

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.

## 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 `α = β`

.

## Equations

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

## Instances For

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))

## Instances For

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.

## Instances For

Conditionally runs a congruence strategy depending on the predicate `b`

applied to the config.

## Equations

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

## Instances For

- goals : Array Lean.MVarId
Accumulated goals that

`congr!`

could not handle. - patterns : List (Lean.TSyntax `rcasesPat)
Patterns to use when doing intro.

## Instances For

## Equations

## Instances For

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)

## 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 `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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

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

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

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.

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

- 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`

.

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.