# 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:

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

.

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

Elaborates a `Parser.Tactic.config`

for `generalize_proofs`

.

## Equations

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

## Instances For

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

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

and `Mathlib.Tactic.GeneralizeProofs.State`

.

## Equations

## Instances For

Inserts a prop/fvar pair into the `propToFVar`

map.

## Equations

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

## Instances For

Context for the `MAbs`

monad.

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.

The tactic configuration.

## Instances For

State for the `MAbs`

monad.

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

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`

and a state `Mathlib.Tactic.GeneralizeProofs.AState`

.

## Equations

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

## Instances For

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

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

Generalize `prop`

, where `proof`

is its proof.

## Equations

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

## Instances For

Runs `x`

with an additional local variable.

## Equations

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

## Instances For

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

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

Core implementation for `appArgExpectedTypes`

.

## Equations

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

## Instances For

Does `mkLambdaFVars fvars e`

but

- zeta reduces let bindings
- only includes used fvars
- returns the list of fvars that were actually abstracted

## Equations

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

## Instances For

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`

.

Core implementation of `abstractProofs`

.

Core implementation of abstracting a proof.

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

Generalizes the proofs in the type `e`

and runs `k`

in a local context with these propositions.
This continuation `k`

is passed

- an array of fvars for the propositions
- an array of proof terms (extracted from
`e`

) that prove these propositions - 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

Core loop for `withGeneralizedProofs`

, adds generalizations one at a time.

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

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

## Instances For

Loop for `generalizeProofsCore`

.

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

`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 (config := { abstract := false })`

.
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:

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