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 Batteries.Tactic.Congr.Config

Function elaborating Congr.Config

Equations

• One or more equations did not get rendered due to their size.

def Batteries.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.

Equations

• One or more equations did not get rendered due to their size.

def Batteries.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.

Equations

• One or more equations did not get rendered due to their size.

partial def Batteries.Tactic.rcongrCore (g : Lean.MVarId) (config : Batteries.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 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

Equations

• One or more equations did not get rendered due to their size.