congr with tactic, rcongr tactic

structure Std.Tactic.Congr.Config : Type

• 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

def Std.Tactic.Congr.elabConfig : Lean.Syntax → Lean.Elab.TermElabM Std.Tactic.Congr.Config

Function elaborating Congr.Config

def Std.Tactic.congrConfig : Lean.ParserDescr

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.

def Std.Tactic.congrConfigWith : Lean.ParserDescr

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.

partial def Std.Tactic.rcongrCore (g : Lean.MVarId) (config : Std.Tactic.Congr.Config) (pats : List (Lean.TSyntax `rcasesPat)) (acc : Array Lean.MVarId) : Lean.Elab.TermElabM (Array Lean.MVarId)

Recursive core of rcongr. Calls ext pats <;> congr and then itself recursively, unless ext pats <;> congr made no progress.

def Std.Tactic.rcongr : Lean.ParserDescr

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