Apply congruence (recursively) to goals of the form ⊢ f as = f bs⊢ f as = f bs
and ⊢ HEq (f as) (f bs)⊢ HEq (f as) (f bs)
.
congr n
controls the depth of the recursive applications. This is useful whencongr
is too aggressive in breaking down the goal. For example, given⊢ f (g (x + y)) = f (g (y + x))⊢ f (g (x + y)) = f (g (y + x))
,congr
produces the goals⊢ x = y⊢ x = y
and⊢ y = x⊢ y = x
, whilecongr 2
produces the intended⊢ x + y = y + x⊢ x + y = y + x
.- If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
- You can use
congr with p (: n)?
to callext p (: n)?
to all subgoals generated bycongr
. For example, if the goal is⊢ f '' s = g '' s⊢ f '' s = g '' s
thencongr with x
generates the goalx : α ⊢ f x = g x⊢ f x = g x
.
Equations
- One or more equations did not get rendered due to their size.
partial def
Std.Tactic.rcongrCore
(g : Lean.MVarId)
(pats : List (Lean.TSyntax `rcasesPat))
(acc : Array Lean.MVarId)
:
Recursive core of rcongr
. Calls ext pats <;> congr
and then itself recursively,
unless ext pats <;> congr
made no progress.
Repeatedly apply congr
and ext
, using the given patterns as arguments for ext
.
There are two ways this tactic stops:
congr
fails (makes no progress), after having already appliedext
.congr
canceled out the last usage ofext
. In this case, the state is reverted to before thecongr
was applied.
For example, when the goal is
⊢ (λ x, f x + 3) '' s = (λ x, g x + 3) '' s
⊢ (λ x, f x + 3) '' s = (λ x, g x + 3) '' s
then rcongr x
produces the goal
x : α ⊢ f x = g x
⊢ f x = g x
This gives the same result as congr; ext x; congr
.
In contrast, congr
would produce
⊢ (λ x, f x + 3) = (λ x, g x + 3)
⊢ (λ x, f x + 3) = (λ x, g x + 3)
and congr with x
(or congr; ext x
) would produce
x : α ⊢ f x + 3 = g x + 3
⊢ f x + 3 = g x + 3
Equations
- One or more equations did not get rendered due to their size.