Documentation

Std.Tactic.Congr

congr with tactic, rcongr tactic #

source
ink
def Std.Tactic.congrWith :
Lean.ParserDescr

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.
source
ink
partial def Std.Tactic.rcongrCore (g : Lean.MVarId) (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.

source
ink
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

⊢ (λ 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.