congr with tactic, rcongr tactic

structure Batteries.Tactic.Congr.Config : Type

Configuration options for congr & rcongr

• 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.

def Batteries.Tactic.Congr.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Function elaborating Congr.Config

def Batteries.Tactic.congrConfig : Lean.ParserDescr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ 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 Batteries.Tactic.congrConfigWith : Lean.ParserDescr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ 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 Batteries.Tactic.rcongrCore (g : Lean.MVarId) (config : 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 Batteries.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