# 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`.

source
structure Batteries.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.

Instances For

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

Elaborates a `Parser.Tactic.config` for `generalize_proofs`.

Equations

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

Instances For

source
structure Batteries.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.

Instances For

source
@[reducible, inline]
abbrev Batteries.Tactic.GeneralizeProofs.MGen (α : Type) :
Type

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

Equations

- Batteries.Tactic.GeneralizeProofs.MGen = ReaderT Batteries.Tactic.GeneralizeProofs.Config (StateRefT' IO.RealWorld Batteries.Tactic.GeneralizeProofs.GState Lean.MetaM)

Instances For

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

Inserts a prop/fvar pair into the `propToFVar` map.

Equations

- Batteries.Tactic.GeneralizeProofs.MGen.insertFVar prop fvar = modify fun (s : Batteries.Tactic.GeneralizeProofs.GState) => { propToFVar := Std.HashMap.insert s.propToFVar prop fvar }

Instances For

source
structure Batteries.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.

Instances For

source
structure Batteries.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`.

Instances For

source
@[reducible, inline]
abbrev Batteries.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`.

Equations

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

Instances For

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

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

Generalize `prop`, where `proof` is its proof.

Equations

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

Instances For

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

Runs `x` with an additional local variable.

Equations

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

Instances For

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

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

source
partial def Batteries.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`.

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

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

- Batteries.Tactic.GeneralizeProofs.generalizeProofsCore g fvars rfvars target = Batteries.Tactic.GeneralizeProofs.generalizeProofsCore.go✝ fvars rfvars target g 0 #[]

Instances For

source
def Lean.MVarId.generalizeProofs (g : MVarId) (fvars : Array FVarId) (target : Bool) (config : Batteries.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.

Equations

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

Instances For

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

Equations

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

Instances For