19baa470e5
This PR gives the `specialize` tactic the ability to instantiate universal quantifiers other than the first using `specialize h (y := v)` syntax. It also fixes an issue where `MVarId.assertAfter` did not record variable alias information, and an issue where `MVarId.replace` and `MVarId.replaceLocalDecl` did not take metavariables into account when calculating dependencies. Additionally it fixes some uninstantiated metavariables bugs, including one in the Infoview tactic state hypothesis diff. The `specialize` tactic now uses `Lean.MVarId.replace` to simplify the implementation, and as a consequence it tries to keep the specialized hypothesis close to its original spot in the local context. Additional metaprogramming API: - `Lean.Expr.getLambdaBody` to accompany `Lean.Expr.getNumHeadLambdas` - `Lean.LocalContext.setType`, `Lean.MetavarContext.setFVarType`, `Lean.MVarId.setFVarType` - `Lean.MVarId.assertAfter'` to assert a new hypothesis as early as possibly in the context where it is well-formed, as a frontend to `Lean.MVarId.assertAfter`, which assumes the new hypothesis is well-formed Breaking change: metaprograms cannot assume that `MVarId`s change if metavariables are assigned. For example, the `change` tactic will no longer change `MVarId`s if the only effect is incidental metavariable assignments. Mathlib impact: this revealed many `dsimp`s that did nothing and could be deleted. Closes #9893
29 lines
678 B
Text
29 lines
678 B
Text
example (x y z : Prop) (f : x → y → z) (xp : x) (yp : y) : z := by
|
|
specialize f xp yp
|
|
assumption
|
|
|
|
example (B C : Prop) (f : forall (A : Prop), A → C) (x : B) : C := by
|
|
specialize f _ x
|
|
exact f
|
|
|
|
example (B C : Prop) (f : forall {A : Prop}, A → C) (x : B) : C := by
|
|
specialize f x
|
|
exact f
|
|
|
|
example (B C : Prop) (f : forall {A : Prop}, A → C) (x : B) : C := by
|
|
specialize @f _ x
|
|
exact f
|
|
|
|
example (X : Type) [Add X] (f : forall {A : Type} [Add A], A → A → A) (x : X) : X := by
|
|
specialize f x x
|
|
clear x
|
|
assumption
|
|
|
|
def ex (f : Nat → Nat → Nat) : Nat := by
|
|
specialize f _ _
|
|
exact 10
|
|
exact 2
|
|
exact f
|
|
|
|
example : ex (· - ·) = 8 :=
|
|
rfl
|