Std.Tactic.Congr

# congr with tactic, rcongr tactic #

• closePre : Bool

If closePre := true, it will attempt to close new goals using Eq.refl, HEq.refl, and assumption with reducible transparency.

• closePost : Bool

If closePost := true, it will try again on goals on which congr failed to make progress with default transparency.

Configuration options for congr & rcongr

Instances For

Function elaborating Congr.Config

Instances For

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ HEq (f as) (f bs). 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.

Instances For

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ 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)), congr produces the goals ⊢ x = y and ⊢ y = x, while congr 2 produces the intended ⊢ 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 then congr with x generates the goal x : α ⊢ f x = g x.
Instances For
partial def Std.Tactic.rcongrCore (g : Lean.MVarId) (config : Std.Tactic.Congr.Config) (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

⊢ (fun x => f x + 3) '' s = (fun x => g x + 3) '' s


then rcongr x produces the goal

x : α ⊢ f x = g x


This gives the same result as congr; ext x; congr.

In contrast, congr would produce

⊢ (fun x => f x + 3) = (fun x => g x + 3)


and congr with x (or congr; ext x) would produce

x : α ⊢ f x + 3 = g x + 3
`
Instances For