The generalize_proofs tactic

Generalize any proofs occuring in the goal or in chosen hypotheses, replacing them by named hypotheses so that they can be referred to later in the proof easily. Commonly useful when dealing with functions like Classical.choose that produce data from proofs.

For example:

example : list.nth_le [1, 2] 1 dec_trivial = 2 := by
  -- ⊢ [1, 2].nth_le 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 h = 2

ink

structure Mathlib.Tactic.GeneralizeProofs.State : Type

• The user provided names, may be anonymous

  nextIdx : List (Lean.TSyntax `Lean.binderIdent)

• The generalizations made so far

  curIdx : Array Lean.Meta.GeneralizeArg

State for the generalize proofs tactic, contains the remaining names to be used and the list of generalizations so far

ink

@[inline]

abbrev Mathlib.Tactic.GeneralizeProofs.M (α : Type) : Type

Monad used by the generalizeProofs tactic, carries an expr cache and state with names to use and previous generalizations

Equations

• Mathlib.Tactic.GeneralizeProofs.M = Lean.MonadCacheT Lean.ExprStructEq Lean.Expr (StateRefT' IO.RealWorld Mathlib.Tactic.GeneralizeProofs.State Lean.MetaM)

ink

partial def Mathlib.Tactic.GeneralizeProofs.visit (e : Lean.Expr) : Mathlib.Tactic.GeneralizeProofs.M Lean.Expr

Recursively generalize proofs occuring in e

ink

def Mathlib.Tactic.GeneralizeProofs.generalizeProofs : Lean.ParserDescr

Generalize proofs in the goal, naming them with the provided list.

For example:

example : list.nth_le [1, 2] 1 dec_trivial = 2 := by
  -- ⊢ [1, 2].nth_le 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nth_le 1 h = 2
⊢ [1, 2].nth_le 1 h = 2

Equations

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