Std.Tactic.Congr

# congr with tactic, rcongr tactic #

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 when congr 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, while congr 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 call ext p (: n)? to all subgoals generated by congr. For example, if the goal is ⊢ f '' s = g '' s⊢ f '' s = g '' s then congr with x generates the goal x : α ⊢ 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 : ) :

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 applied ext.
• congr canceled out the last usage of ext. In this case, the state is reverted to before the congr 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.