The generalize_proofs tactic

Generalize any proofs occurring in the goal or in chosen hypotheses, replacing them by local hypotheses. When these hypotheses are named, this makes it easy to refer to these proofs later in a proof, commonly useful when dealing with functions like Classical.choose that produce data from proofs. It is also useful to eliminate proof terms to handle issues with dependent types.

For example:

def List.nthLe {α} (l : List α) (n : ℕ) (_h : n < l.length) : α := sorry
example : List.nthLe [1, 2] 1 (by simp) = 2 := by
  -- ⊢ [1, 2].nthLe 1 ⋯ = 2
  generalize_proofs h
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2

The tactic is similar in spirit to Lean.Meta.AbstractNestedProofs in core. One difference is that it the tactic tries to propagate expected types so that we get 1 < [1, 2].length in the above example rather than 1 < Nat.succ 1.

structure Mathlib.Tactic.GeneralizeProofs.Config : Type

Configuration for the generalize_proofs tactic.

• maxDepth : Nat

  The maximum recursion depth when generalizing proofs. When maxDepth > 0, then proofs are generalized from the types of the generalized proofs too.

• abstract : Bool

  When abstract is true, then the tactic will create universally quantified proofs to account for bound variables. When it is false then such proofs are left alone.

• debug : Bool

  (Debugging) When true, enables consistency checks.

def Mathlib.Tactic.GeneralizeProofs.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Elaborates a Parser.Tactic.config for generalize_proofs.

structure Mathlib.Tactic.GeneralizeProofs.GState : Type

State for the MGen monad.

• propToFVar : Lean.ExprMap Lean.Expr

  Mapping from propositions to an fvar in the local context with that type.

@[reducible, inline]

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

Monad used to generalize proofs. Carries Mathlib.Tactic.GeneralizeProofs.Config and Mathlib.Tactic.GeneralizeProofs.State.

def Mathlib.Tactic.GeneralizeProofs.MGen.insertFVar (prop fvar : Lean.Expr) : MGen Unit

Inserts a prop/fvar pair into the propToFVar map.

structure Mathlib.Tactic.GeneralizeProofs.AContext : Type

Context for the MAbs monad.

• fvars : Array Lean.Expr

  The local fvars corresponding to bound variables. Abstraction needs to be sure that these variables do not appear in abstracted terms.

• propToFVar : Lean.ExprMap Lean.Expr

  A copy of propToFVar from GState.

• depth : Nat

  The recursion depth, for how many times visit is called from within `visitProof.

• initLCtx : Lean.LocalContext

  The initial local context, for resetting when recursing.

• config : Config

  The tactic configuration.

structure Mathlib.Tactic.GeneralizeProofs.AState : Type

State for the MAbs monad.

• generalizations : Array (Lean.Expr × Lean.Expr)

  The prop/proof triples to add to the local context. The proofs must not refer to fvars in fvars.

• propToProof : Lean.ExprMap Lean.Expr

  Map version of generalizations. Use MAbs.findProof? and MAbs.insertProof.

@[reducible, inline]

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

Monad used to abstract proofs, to prepare for generalization. Has a cache (of expr/type? pairs), and it also has a reader context Mathlib/Tactic/GeneralizeProofs/AContext.lean and a state Mathlib/Tactic/GeneralizeProofs/AState.lean.

def Mathlib.Tactic.GeneralizeProofs.MGen.runMAbs {α : Type} (mx : MAbs α) : MGen (α × Array (Lean.Expr × Lean.Expr))

Runs MAbs in MGen. Returns the value and the generalizations.

def Mathlib.Tactic.GeneralizeProofs.MAbs.findProof? (prop : Lean.Expr) : MAbs (Option Lean.Expr)

Finds a proof of prop by looking at propToFVar and propToProof.

def Mathlib.Tactic.GeneralizeProofs.MAbs.insertProof (prop pf : Lean.Expr) : MAbs Unit

Generalize prop, where proof is its proof.

def Mathlib.Tactic.GeneralizeProofs.MAbs.withLocal {α : Type} (fvar : Lean.Expr) (x : MAbs α) : MAbs α

Runs x with an additional local variable.

def Mathlib.Tactic.GeneralizeProofs.MAbs.withRecurse {α : Type} (x : MAbs α) : MAbs α

Runs x with an increased recursion depth and the initial local context, clearing fvars.

def Mathlib.Tactic.GeneralizeProofs.appArgExpectedTypes (f : Lean.Expr) (args : Array Lean.Expr) (ty? : Option Lean.Expr) : Lean.MetaM (Array (Option Lean.Expr))

Computes expected types for each argument to f, given that the type of mkAppN f args is supposed to be ty? (where if ty? is none, there's no type to propagate inwards).

def Mathlib.Tactic.GeneralizeProofs.appArgExpectedTypes.go (f : Lean.Expr) (args : Array Lean.Expr) (ty? : Option Lean.Expr) : Lean.MetaM (Array (Option Lean.Expr))

Core implementation for appArgExpectedTypes.

def Mathlib.Tactic.GeneralizeProofs.mkLambdaFVarsUsedOnly (fvars : Array Lean.Expr) (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr × Lean.Expr)

Does mkLambdaFVars fvars e but

1. zeta reduces let bindings
2. only includes used fvars
3. returns the list of fvars that were actually abstracted

partial def Mathlib.Tactic.GeneralizeProofs.abstractProofs (e : Lean.Expr) (ty? : Option Lean.Expr) : MAbs Lean.Expr

Abstract proofs occurring in the expression. A proof is abstracted if it is of the form f a b ... where a b ... are bound variables (that is, they are variables that are not present in the initial local context) and where f contains no bound variables. In this form, f can be immediately lifted to be a local variable and generalized. The abstracted proofs are recorded in the state.

This function is careful to track the type of e based on where it's used, since the inferred type might be different. For example, (by simp : 1 < [1, 2].length) has 1 < Nat.succ 1 as the inferred type, but from knowing it's an argument to List.nthLe we can deduce 1 < [1, 2].length.

partial def Mathlib.Tactic.GeneralizeProofs.abstractProofs.visit (e : Lean.Expr) (ty? : Option Lean.Expr) : MAbs Lean.Expr

Core implementation of abstractProofs.

partial def Mathlib.Tactic.GeneralizeProofs.abstractProofs.visitProof (e : Lean.Expr) (ty? : Option Lean.Expr) : MAbs Lean.Expr

Core implementation of abstracting a proof.

def Mathlib.Tactic.GeneralizeProofs.initialPropToFVar : Lean.MetaM (Lean.ExprMap Lean.Expr)

Create a mapping of all propositions in the local context to their fvars.

def Mathlib.Tactic.GeneralizeProofs.withGeneralizedProofs {α : Type} [Nonempty α] (e : Lean.Expr) (ty? : Option Lean.Expr) (k : Array Lean.Expr → Array Lean.Expr → Lean.Expr → MGen α) : MGen α

Generalizes the proofs in the type e and runs k in a local context with these propositions. This continuation k is passed

1. an array of fvars for the propositions
2. an array of proof terms (extracted from e) that prove these propositions
3. the generalized e, which refers to these fvars

The propToFVar map is updated with the new proposition fvars.

partial def Mathlib.Tactic.GeneralizeProofs.withGeneralizedProofs.go {α : Type} (k : Array Lean.Expr → Array Lean.Expr → Lean.Expr → MGen α) (e : Lean.Expr) (generalizations : Array (Lean.Expr × Lean.Expr)) [Nonempty α] (i : Nat) (fvars pfs : Array Lean.Expr) (proofToFVar propToFVar : Lean.ExprMap Lean.Expr) : MGen α

Core loop for withGeneralizedProofs, adds generalizations one at a time.

def Mathlib.Tactic.GeneralizeProofs.generalizeProofsCore (g : Lean.MVarId) (fvars rfvars : Array Lean.FVarId) (target : Bool) : MGen (Array Lean.Expr × Lean.MVarId)

Main loop for Lean.MVarId.generalizeProofs. The fvars array is the array of fvars to generalize proofs for, and rfvars is the array of fvars that have been reverted. The g metavariable has all of these fvars reverted.

partial def Mathlib.Tactic.GeneralizeProofs.generalizeProofsCore.go (fvars rfvars : Array Lean.FVarId) (target : Bool) (g : Lean.MVarId) (i : Nat) (hs : Array Lean.Expr) : MGen (Array Lean.Expr × Lean.MVarId)

Loop for generalizeProofsCore.

def Lean.MVarId.generalizeProofs (g : MVarId) (fvars : Array FVarId) (target : Bool) (config : Mathlib.Tactic.GeneralizeProofs.Config := { }) : MetaM (Array Expr × MVarId)

Generalize proofs in the hypotheses fvars and, if target is true, the target. Returns the fvars for the generalized proofs and the new goal.

If a hypothesis is a proposition and a let binding, this will clear the value of the let binding.

If a hypothesis is a proposition that already appears in the local context, it will be eliminated.

Only nontrivial proofs are generalized. These are proofs that aren't of the form f a b ... where f is atomic and a b ... are bound variables. These sorts of proofs cannot be meaningfully generalized, and also these are the sorts of proofs that are left in a term after generalization.

def Mathlib.Tactic.generalizeProofsElab : Lean.ParserDescr

generalize_proofs ids* [at locs]? generalizes proofs in the current goal, turning them into new local hypotheses.

• generalize_proofs generalizes proofs in the target.
• generalize_proofs at h₁ h₂ generalized proofs in hypotheses h₁ and h₂.
• generalize_proofs at * generalizes proofs in the entire local context.
• generalize_proofs pf₁ pf₂ pf₃ uses names pf₁, pf₂, and pf₃ for the generalized proofs. These can be _ to not name proofs.

If a proof is already present in the local context, it will use that rather than create a new local hypothesis.

When doing generalize_proofs at h, if h is a let binding, its value is cleared, and furthermore if h duplicates a preceding local hypothesis then it is eliminated.

The tactic is able to abstract proofs from under binders, creating universally quantified proofs in the local context. To disable this, use generalize_proofs -abstract. The tactic is also set to recursively abstract proofs from the types of the generalized proofs. This can be controlled with the maxDepth configuration option, with generalize_proofs (config := { maxDepth := 0 }) turning this feature off.

For example:

def List.nthLe {α} (l : List α) (n : ℕ) (_h : n < l.length) : α := sorry
example : List.nthLe [1, 2] 1 (by simp) = 2 := by
  -- ⊢ [1, 2].nthLe 1 ⋯ = 2
  generalize_proofs h
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2