This module defines the
tactic.generalizes' tactic and its interactive version
tactic.interactive.generalizes. These work like
generalize, but they can
generalize over multiple expressions at once. This is particularly handy when
there are dependencies between the expressions, in which case
usually fail but
generalizes may succeed.
To generalize the target
T over expressions
j₁ : J₁, ..., jₙ : Jₙ, we first
create the new target type
T' = ∀ (k₁ : J₁) ... (kₙ : Jₙ) (k₁_eq : k₁ = j₁) ... (kₙ_eq : kₙ == jₙ), U
T with any occurrences of the
jᵢ replaced by the corresponding
kᵢ. Note that some of the
kᵢ_eq may be heterogeneous; this happens when
there are dependencies between the
jᵢ. The construction of
T' is performed
T', we can
assert it and use it to construct a proof of
the original target by instantiating the binders with
This leaves us with a generalized goal. This construction is performed by
- Target expression
- List of expressions
jᵢto be generalised, along with a name for the local const that will replace them. The
jᵢmust be in dependency order:
[n, fin n]is okay but
[fin n, n]is not.
- List of new local constants
kᵢ, one for each
jᵢreplaced by the
e[jᵢ := kᵢ]...[j₀ := k₀].
Note that the substitution also affects the types of the
jᵢ : Jᵢ then
kᵢ : Jᵢ[jᵢ₋₁ := kᵢ₋₁]...[j₀ := k₀].
md and the boolean
unify are passed to
kabstract when we
abstract over occurrences of the
Input: for each equation that should be generated: the equation name, the
jᵢ and the corresponding local constant
kᵢ from step 1.
Output: for each element of the input list a new local constant of type
jᵢ = kᵢ or
jᵢ == kᵢ and a proof of
jᵢ = jᵢ or
jᵢ == jᵢ.
md is used when determining whether the type of
jᵢ is defeq
to the type of
kᵢ (and thus whether to generate a homogeneous or heterogeneous
jᵢ; the local constants
kᵢ from step 1; the equations and their
proofs from step 2.
This step is the first one that changes the goal (and also the last one overall). It asserts the generalized goal, then derives the current goal from it. This leaves us with the generalized goal.
Generalizes the target over each of the expressions in
args = [(a₁, h₁, arg₁), ...], this changes the target to
∀ (a₁ : T₁) ... (h₁ : a₁ = arg₁) ..., U
U is the current target with every occurrence of
argᵢ replaced by
aᵢ. A similar effect can be achieved by using
generalize once for each of
args, but if there are dependencies between the
args, this may fail to
perform some generalizations.
The replacement is performed using keyed matching/unification with transparency
unify determines whether matching or unification is used. See
After generalizing the
args, the target type may no longer type check.
generalizes' will then raise an error.
Generalizes the target over multiple expressions. For example, given the goal
P : ∀ n, fin n → Prop n : ℕ f : fin n n' : ℕ n'_eq : n' = nat.succ n f' : fin n' f'_eq : f' == fin.succ f ⊢ P n' f'
After generalization, the target type may no longer type check.
will then raise an error.