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.
 closePre : Bool
If
closePre := true
, then try to close goals before applying congruence lemmas using tactics such asrfl
andassumption. 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 theassumption
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 lefthand side and the righthand side. If
preferLHS
istrue
then we start with the lefthand 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 provingf a = g x y
.In this case, we might still consider
f = g x
if a pass generates a congruence lemma using the lefthand side. UsesameFun := true
to ensure both sides are applications of the same function (making it be similar to thecongr
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 iff
andg
are defeq (making it be similar to thecongr
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
, settingmaxArgs := some 2
means it will only consider eitherf a b = g w x y
andc = z
orf a = g w x
,b = y
, andc = z
. SettingmaxArgs := none
(the default) means no limit.When the functions are dependent,
maxArgs
can prevent congruence from working at all. InFintype.card α = Fintype.card β
, one needs to havemaxArgs
at2
or higher since there is aFintype
instance argument that depends on the first.When there aren't such dependency issues, setting
maxArgs := some 1
causescongr!
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ₘ
. Iff
is not definitionally equal tog
orm ≠ n
, thenα
andβ
are not plausibly equal.  If there is some
i
such thataᵢ
andbᵢ
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 asFin n = Fin m
orSubtype 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
intofun x y => x + y
.  useCongrSimp : Bool
The configuration for the congr!
tactic.
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
andty2
are inProp
, then yes.  If in whnf both
ty1
andty2
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.
Instances For
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
.
Instances For
Instances For
Like mkCongrSimp?
but takes in a specific arity.
Instances For
Try applying userprovided 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
Instances For
Try to apply pi_congr
. This is similar to Lean.MVar.congrImplies?
.
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
 goals : Array Lean.MVarId
Accumulated goals that
congr!
could not handle.  patterns : List (Lean.TSyntax `rcasesPat)
Patterns to use when doing intro.
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
, andx ↔ x
.  deleting Prop hypotheses that are already in the local context.
 converting
HEq x y
tox = y
if possible.  converting
x = y
tox ↔ y
if possible.
Instances For
Instances For
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
Instances For
A pass to clean up after Lean.MVarId.preCongr!
and Lean.MVarId.congrCore!
.
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.
Instances For
Instances For
Equations
 One or more equations did not get rendered due to their size.
Instances For
Equates pieces of the lefthand side of a goal to corresponding pieces of the righthand 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 lefthand sides
to righthand 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
andsimp
. If there is a subexpression that can be rewritten bysimp
, thencongr!
should be able to generate an equality for it. 
It can do congruences of pi types using lemmas like
implies_congr
andpi_congr
. 
Before applying congruences, it will run the
intros
tactic automatically. The introduced variables can be given names using awith
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
orFunction.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
orproof_irrel_heq
, and using theassumption
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.