-
Notifications
You must be signed in to change notification settings - Fork 350
/
Apply.lean
328 lines (298 loc) · 13.1 KB
/
Apply.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Siddhartha Gadgil
-/
prelude
import Lean.Util.FindMVar
import Lean.Meta.SynthInstance
import Lean.Meta.CollectMVars
import Lean.Meta.Tactic.Util
namespace Lean.Meta
/-- Controls which new mvars are turned in to goals by the `apply` tactic.
- `nonDependentFirst` mvars that don't depend on other goals appear first in the goal list.
- `nonDependentOnly` only mvars that don't depend on other goals are added to goal list.
- `all` all unassigned mvars are added to the goal list.
-/
inductive ApplyNewGoals where
| nonDependentFirst | nonDependentOnly | all
/-- Configures the behaviour of the `apply` tactic. -/
structure ApplyConfig where
newGoals := ApplyNewGoals.nonDependentFirst
/--
If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
one inferred. The `congr` tactic sets this flag to false.
-/
synthAssignedInstances := true
/--
If `allowSynthFailures` is `true`, then `apply` will return instance implicit arguments
for which typeclass search failed as new goals.
-/
allowSynthFailures := false
/--
If `approx := true`, then we turn on `isDefEq` approximations. That is, we use
the `approxDefEq` combinator.
-/
approx : Bool := true
/--
Compute the number of expected arguments and whether the result type is of the form
(?m ...) where ?m is an unassigned metavariable.
-/
def getExpectedNumArgsAux (e : Expr) : MetaM (Nat × Bool) :=
withDefault <| forallTelescopeReducing e fun xs body =>
pure (xs.size, body.getAppFn.isMVar)
def getExpectedNumArgs (e : Expr) : MetaM Nat := do
let (numArgs, _) ← getExpectedNumArgsAux e
pure numArgs
private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α :=
throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}"
def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
(synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit :=
newMVars.size.forM fun i => do
if binderInfos[i]!.isInstImplicit then
let mvar := newMVars[i]!
if synthAssignedInstances || !(← mvar.mvarId!.isAssigned) then
let mvarType ← inferType mvar
try
let mvarVal ← synthInstance mvarType
unless (← isDefEq mvar mvarVal) do
throwTacticEx tacticName mvarId "failed to assign synthesized instance"
catch e => unless allowSynthFailures do throw e
def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do
let parentTag ← mvarId.getTag
if newMVars.size == 1 then
-- if there is only one subgoal, we inherit the parent tag
newMVars[0]!.mvarId!.setTag parentTag
else
unless parentTag.isAnonymous do
newMVars.size.forM fun i => do
let mvarIdNew := newMVars[i]!.mvarId!
unless (← mvarIdNew.isAssigned) do
unless binderInfos[i]!.isInstImplicit do
let currTag ← mvarIdNew.getTag
mvarIdNew.setTag (appendTag parentTag currTag)
/--
If `synthAssignedInstances` is `true`, then `apply` will synthesize instance implicit arguments
even if they have assigned by `isDefEq`, and then check whether the synthesized value matches the
one inferred. The `congr` tactic sets this flag to false.
-/
def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
(synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
-- TODO: default and auto params
appendParentTag mvarId newMVars binderInfos
private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
otherMVars.anyM fun otherMVar => do
if mvar == otherMVar then
return false
else
let otherMVarType ← inferType otherMVar
return (otherMVarType.findMVar? fun mvarId => mvarId == mvar.mvarId!).isSome
/-- Partitions the given mvars in to two arrays (non-deps, deps)
according to whether the given mvar depends on other mvars in the array.-/
private def partitionDependentMVars (mvars : Array Expr) : MetaM (Array MVarId × Array MVarId) :=
mvars.foldlM (init := (#[], #[])) fun (nonDeps, deps) mvar => do
let currMVarId := mvar.mvarId!
if (← dependsOnOthers mvar mvars) then
return (nonDeps, deps.push currMVarId)
else
return (nonDeps.push currMVarId, deps)
private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MVarId)
| ApplyNewGoals.nonDependentFirst => do
let (nonDeps, deps) ← partitionDependentMVars mvars
return nonDeps.toList ++ deps.toList
| ApplyNewGoals.nonDependentOnly => do
let (nonDeps, _) ← partitionDependentMVars mvars
return nonDeps.toList
| ApplyNewGoals.all => return mvars.toList.map Lean.Expr.mvarId!
/-- Custom `isDefEq` for the `apply` tactic -/
private def isDefEqApply (cfg : ApplyConfig) (a b : Expr) : MetaM Bool := do
if cfg.approx then
approxDefEq <| isDefEqGuarded a b
else
isDefEqGuarded a b
/--
Close the given goal using `apply e`.
-/
def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
mvarId.withContext do
mvarId.checkNotAssigned `apply
let targetType ← mvarId.getType
let eType ← inferType e
let (numArgs, hasMVarHead) ← getExpectedNumArgsAux eType
/-
The `apply` tactic adds `_`s to `e`, and some of these `_`s become new goals.
When `hasMVarHead` is `false` we try different numbers, until we find a type compatible with `targetType`.
We used to try only `numArgs-targetTypeNumArgs` when `hasMVarHead = false`, but this is not always correct.
For example, consider the following example
```
example {α β} [LE_trans β] (x y z : α → β) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z := by
apply le_trans
assumption
assumption
```
In this example, `targetTypeNumArgs = 1` because `LE` for functions is defined as
```
instance {α : Type u} {β : Type v} [LE β] : LE (α → β) where
le f g := ∀ i, f i ≤ g i
```
-/
let rangeNumArgs ← if hasMVarHead then
pure [numArgs : numArgs+1]
else
let targetTypeNumArgs ← getExpectedNumArgs targetType
pure [numArgs - targetTypeNumArgs : numArgs+1]
/-
Auxiliary function for trying to add `n` underscores where `n ∈ [i: rangeNumArgs.stop)`
See comment above
-/
let rec go (i : Nat) : MetaM (Array Expr × Array BinderInfo) := do
if i < rangeNumArgs.stop then
let s ← saveState
let (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType i
if (← isDefEqApply cfg eType targetType) then
return (newMVars, binderInfos)
else
s.restore
go (i+1)
else
let (_, _, eType) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start)
throwApplyError mvarId eType targetType
termination_by rangeNumArgs.stop - i
let (newMVars, binderInfos) ← go rangeNumArgs.start
postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures
let e ← instantiateMVars e
mvarId.assign (mkAppN e newMVars)
let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
let otherMVarIds ← getMVarsNoDelayed e
let newMVarIds ← reorderGoals newMVars cfg.newGoals
let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId
let result := newMVarIds ++ otherMVarIds.toList
result.forM (·.headBetaType)
return result
@[deprecated MVarId.apply]
def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
mvarId.apply e cfg
/-- Short-hand for applying a constant to the goal. -/
def _root_.Lean.MVarId.applyConst (mvar : MVarId) (c : Name) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
mvar.apply (← mkConstWithFreshMVarLevels c) cfg
end Meta
open Meta
namespace MVarId
partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) :=
mvarId.withContext do
mvarId.checkNotAssigned `splitAnd
let type ← mvarId.getType'
if !type.isAppOfArity ``And 2 then
return [mvarId]
else
let tag ← mvarId.getTag
let rec go (type : Expr) : StateRefT (Array MVarId) MetaM Expr := do
let type ← whnf type
if type.isAppOfArity ``And 2 then
let p₁ := type.appFn!.appArg!
let p₂ := type.appArg!
return mkApp4 (mkConst ``And.intro) p₁ p₂ (← go p₁) (← go p₂)
else
let idx := (← get).size + 1
let mvar ← mkFreshExprSyntheticOpaqueMVar type (tag ++ (`h).appendIndexAfter idx)
modify fun s => s.push mvar.mvarId!
return mvar
let (val, s) ← go type |>.run #[]
mvarId.assign val
return s.toList
/--
Apply `And.intro` as much as possible to goal `mvarId`.
-/
abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
splitAndCore mvarId
@[deprecated splitAnd]
def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
mvarId.splitAnd
def exfalso (mvarId : MVarId) : MetaM MVarId :=
mvarId.withContext do
mvarId.checkNotAssigned `exfalso
let target ← instantiateMVars (← mvarId.getType)
let u ← getLevel target
let mvarIdNew ← mkFreshExprSyntheticOpaqueMVar (mkConst ``False) (tag := (← mvarId.getTag))
mvarId.assign (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew)
return mvarIdNew.mvarId!
/--
Apply the `n`-th constructor of the target type,
checking that it is an inductive type,
and that there are the expected number of constructors.
-/
def nthConstructor
(name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
MetaM (List MVarId) := do
goal.withContext do
goal.checkNotAssigned name
matchConstInduct (← goal.getType').getAppFn
(fun _ => throwTacticEx name goal "target is not an inductive datatype")
fun ival us => do
if let some e := expected? then unless ival.ctors.length == e do
throwTacticEx name goal
s!"{name} tactic works for inductive types with exactly {e} constructors"
if h : idx < ival.ctors.length then
goal.apply <| mkConst ival.ctors[idx] us
else
throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
/--
Try to convert an `Iff` into an `Eq` by applying `iff_of_eq`.
If successful, returns the new goal, and otherwise returns the original `MVarId`.
This may be regarded as being a special case of `Lean.MVarId.liftReflToEq`, specifically for `Iff`.
-/
def iffOfEq (mvarId : MVarId) : MetaM MVarId := do
let res ← observing? do
let [mvarId] ← mvarId.apply (mkConst ``iff_of_eq []) | failure
return mvarId
return res.getD mvarId
/--
Try to convert an `Eq` into an `Iff` by applying `propext`.
If successful, then returns then new goal, otherwise returns the original `MVarId`.
-/
def propext (mvarId : MVarId) : MetaM MVarId := do
let res ← observing? do
-- Avoid applying `propext` if the target is not an equality of `Prop`s.
-- We don't want a unification specializing `Sort*` to `Prop`.
let tgt ← withReducible mvarId.getType'
let some (_, x, _) := tgt.eq? | failure
guard <| ← Meta.isProp x
let [mvarId] ← mvarId.apply (mkConst ``propext []) | failure
return mvarId
return res.getD mvarId
/--
Try to close the goal using `proof_irrel_heq`. Returns whether or not it succeeds.
We need to be somewhat careful not to assign metavariables while doing this, otherwise we might
specialize `Sort _` to `Prop`.
-/
def proofIrrelHeq (mvarId : MVarId) : MetaM Bool :=
mvarId.withContext do
let res ← observing? do
mvarId.checkNotAssigned `proofIrrelHeq
let tgt ← withReducible mvarId.getType'
let some (_, lhs, _, rhs) := tgt.heq? | failure
-- Note: `mkAppM` uses `withNewMCtxDepth`, which prevents `Sort _` from specializing to `Prop`
let pf ← mkAppM ``proof_irrel_heq #[lhs, rhs]
mvarId.assign pf
return true
return res.getD false
/--
Try to close the goal using `Subsingleton.elim`. Returns whether or not it succeeds.
We are careful to apply `Subsingleton.elim` in a way that does not assign any metavariables.
This is to prevent the `Subsingleton Prop` instance from being used as justification to specialize
`Sort _` to `Prop`.
-/
def subsingletonElim (mvarId : MVarId) : MetaM Bool :=
mvarId.withContext do
let res ← observing? do
mvarId.checkNotAssigned `subsingletonElim
let tgt ← withReducible mvarId.getType'
let some (_, lhs, rhs) := tgt.eq? | failure
-- Note: `mkAppM` uses `withNewMCtxDepth`, which prevents `Sort _` from specializing to `Prop`
let pf ← mkAppM ``Subsingleton.elim #[lhs, rhs]
mvarId.assign pf
return true
return res.getD false
end Lean.MVarId